[Haskell-cafe] question about "singletons"

[wren ng thornton]

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