On 6/1/13 3:18 PM, TP wrote:
In other words, bottom can be an inhabitant of a concrete type, not a type constructor, which I can understand. But a type of kind Nat is a concrete type, so why bottom cannot be an inhabitant of this type?
The technical term is "proper type". That is, types are used as a way of characterizing collections of values; but, all sorts of things can exist at the type level. For lack of a better name, we call everything at the type level a "type", in order to distinguish them from things at the value level or kind level, etc. But in order to be a *proper* type, a type-level expression must serve to characterize a collection of values. Types of kind * are proper types, because they serve to characterize collections of values. Types of other kinds are not proper, since they do not characterize collections of values. Thus, we can't say: undefined :: (->) nor: undefined :: Maybe because (->) and Maybe are not proper types. It doesn't make sense to say that some value (like undefined) belongs to the collection of values characterized by them, since there is no such collection to belong to! The same sort of thing holds for datakinds. Types of kind 'Nat are not proper, in exactly the same way that types of kind *->* or *->*->* are not proper. -- Live well, ~wren