3 ms·
(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 pos
by 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.