3 ms·
> So types are prior to sets: types provide a universe of values, constructed in orderly ways, that we can work with; only then can we start picking out certain
by piinbinary 5y ago
> So types are prior to sets: types provide a universe of values, constructed in orderly ways, that we can work with; only then can we start picking out certain values to place them in a set.
What about uninhabited types?
Or types where the constructor is not enough to determine the entire type?
e.g.
data MyType a b = MyConstructor { myField :: a }
- tel 5y agoWhat'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).