3 ms·
What's the question? For uninhabited types there's a universe (empty), ways to construct (no ways), ways to work with (any way), and you can (tautologically) p
by tel 5y ago
What's the question?
For uninhabited types there's a universe (empty), ways to construct (no ways), ways to work with (any way), and you can (tautologically) pick out values and put them in sets.
Constructors aren't first order meaningful (except in higher-kinded calculi) but for any concrete types `A` and `B`, `MyType A B` is a type with a universe of values (isomorphic to `A`'s universe), ways to construct and use (again, isomorphic to `A`s), and we can place them in sets.
- piinbinary 5y agoI think I see now. So the author wasn't saying that construction of values is what defines the type. Rather it is a necessary step before you can start talking about sets of values. (And you can talk about a type without knowing how to construct it, so that makes types different from sets?)
- tel 5y agoI think I see what the question is now. A type is defined by picking how its values are introduced and/or used. It doesn’t mean that those rules have to be actually productive. In fact there are many kinds of uninhabited types (the empty type being the simplest, but in languages with rich type systems there are many others).