Hacker News new | past | comments | ask | show | jobs | submit login

Types can be seen both as collections of values and as collections of expressions. (I'm defining a “value” as “something the operational semantics of the language lets you substitute a variable with”.) In a call-by-value language, the former is embeddable in the latter. In a call-by-name or call-by-need language, the two coincide.



I disagree that it's a good idea to think of types as a "collection" (loosely) of values. It may be the case that you do not distinguish computation and value (here, I'm thinking of CBPV) but types only classify values as interpreted via their embedding into expressions.


If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound. Of course, induction on datatypes is unsound in Haskell, but it's sound in Standard ML.


> If a type couldn't be regarded as a collection of values in a strict language, then induction on datatypes would simply be unsound.

Just because induction on some types is sound, does not entail that induction on all types is sound. Indeed it's not in general, even though it may be in specific languages.


(0) I didn't say all types. I said datatypes.

(1) Induction on datatypes is a powerful tool for reasoning about programs in strict languages, and it's only possible when you regard datatypes as collections of values.


Then data types are a restricted notion of types for which induction applies, so we agree that types in general are not a collection of values.


All types in a call-by-value language are two collections: one of values and another of expressions, the former embeddable in the latter. This is plain obvious when you see its operational semantics.


Not all types need to have induction principles. The ones that do are nicer, of course, precisely because they correspond to values.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: