Type theory: type kinds

Question

I've read a lot of interesting things about type kinds, higher-kinded types and so on. By default Haskell supports two sorts of kind:

• Simple type: *
• Type constructor: * → *

Latest GHC's language extensions ConstraintKinds adds a new kind:

• Type parameter constraint: Constraint

Also after reading this mailing list it becomes clear that another type of kind may exists, but it is not supported by GHC (but such support is implemented in .NET):

• Unboxed type: #

I've learned about polymorphic kinds and I think I understand the idea. Also Haskell supports explicitly-kinded quantification.

So my questions are:

• Do any other types of kinds exists?
• Are there any other kind-releated language features?
• What does subkinding mean? Where is it implemented/useful?
• Is there a type system on top of kinds, like kinds are a type system on top of types? (just interested)

Answer 1

Yes, other kinds exist. The page Intermediate Types describes other kinds used in GHC (including both unboxed types and some more complicated kinds as well). The Ωmega language takes higher-kinded types to the maximum logical extension, allowing for user-definable kinds (and sorts, and higher). This page proposes a kind system extension for GHC which would allow for user-definable kinds in Haskell, as well as a good example of why they would be useful.

As a short excerpt, suppose you wanted a list type which had a type-level annotation of the length of the list, like this:

data Zero data Succ n  data List :: * -> * -> * where   Nil   :: List a Zero   Cons  :: a -> List a n -> List a (Succ n) 

The intention is that the last type argument should only be Zero or Succ n, where n is again only Zero or Succ n. In short, you need to introduce a new kind, called Nat which contains only the two types Zero and Succ n. Then the List datatype could express that the last argument is not a *, but a Nat, like

data List :: * -> Nat -> * where   Nil   :: List a Zero   Cons  :: a -> List a n -> List a (Succ n) 

This would allow the type checker to be much more discriminative in what it accepts, as well as making type-level programming much more expressive.