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

> 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.

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