On 6/18/19 1:25 PM, Stephen J. Turnbull wrote:
Dan Sommers writes:
How would I "think of types as collections of their instances"?
The canonical example of a type as a collection of instances is an enumeration, the simplest (useful) example of which is bool = {False, True}.
And now the light goes on. :-) [...]
In my mind, a type is a description/container/shortand for a collection of properties or behaviors of instances of that type.
That's one way to think about it, of course. But the strong intuitions about the numeric tower (a natural number *is* an integer, an integer *is* a real number, and so on) as well as some useful but (intuitively) more artificial ideas such as a bool *is* a natural number are just as well expressed as set inclusions. This is useful in type theory, but explaining "how" is way beyond the scope of this post (and this whole list, in fact).
Thanks, Stephen; you've done just enough to give me a good shove in the right direction.