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