Why names form a kind and not just a type?

Question

Some time ago in one of Haskell extensions (can't find the link), and recently in Ur I've found that names (e.g., of record fields) form a Kind. Can somebody explain why Type abstraction is not enough for them?

Wynne

Answer 1

The answer is simple: because they can appear in types. Consequently, they have to live on the type level (otherwise you would need dependent types). And because they live on the type level, they are classified by a kind.

Kesterson

This answer has put everything into place in my head. Thanks! – Wynne

Answer 2

Record systems define rules for values, types and (maybe) kinds. What rules are used depends on the type system being designed, and what the designer wishes to achieve.

E.g. in Haskell, record labels are:

• values (the accessor functions)
• those values have types (e.g. Record -> Int)
• those types have kinds (*)

Other record systems can use the type or kind system for different purposes.

By putting labels in a separate kind, the type checker can treat them specially, with special rules for e.g. automatic lenses, or proofs to do with record construction (totality perhaps) not true of general purpose functions.

An example of using the kind system in Haskell is the use of "unboxed types". These are types that have:

• different runtime representations to regular values
• different binding forms (e.g. can't be allocated on the heap)

To keep unboxed types from mixing in with regular types, they are given a different kind, which allows the compiler to track their separation.

So, there is nothing magic about record label names that means you have to use a different kind to represent them -- it is just a choice a language designer can make - and in a dependently-typed language such as Ur or Twelf, that can be a useful distinction.

Elvaelvah

Thanks, the example about unboxed types is enlightening – Wynne