3 ms·
It's also simple enough to direct readers to note that types refer to expressions, not values. It's only through later evaluation relations do those expressions
by tel 10y ago
It's also simple enough to direct readers to note that types refer to expressions, not values. It's only through later evaluation relations do those expressions and their values end up sharing types.
- catnaroek 10y agoTypes 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.
- tel 10y agoI 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.
- catnaroek 10y agoIf 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.
- naasking 10y ago> 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.
- catnaroek 10y ago(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.
- naasking 10y agoThen 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.
- catnaroek 10y agoAll 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.
- tel 10y agoNot all types need to have induction principles. The ones that do are nicer, of course, precisely because they correspond to values.