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.

Answer 2

Just as types are classified with kinds, kinds are classified with sorts.

Ωmega programming language has a kind system with user definable kinds at any level. (So says its wiki. I think it refers to the sorts and the levels above, but I am not sure.)

Answer 3

There has been a proposal to lift types into the kind level and values into the type level. But I don't know if that is already implemented (or if it ever will reach "prime time")

Consider the following code:

data Z
data S a 

data Vec (a :: *) (b :: *) where
  VNil  :: Vec Z a 
  VCons :: a -> Vec l a -> Vec (S l) a 

This is a Vector that has it's dimension encoded in the type. We are using Z and S to generate the natural number. That's kind of nice but we cannot "type check" if we are using the right types when generating a Vec (we could accidently switch length an content type) and we also need to generate a type S and Z, which is inconvenient if we already defined the natural numbers like so:

data Nat = Z | S Nat

With the proposal you could write something like this:

data Nat = Z | S Nat

data Vec (a :: Nat) (b :: *) where                                              
  VNil  :: Vec Z a
  VCons :: a -> Vec l a -> Vec (S l) a

This would lift Nat into the kind level and S and Z into the type level if needed. So Nat is another kind and lives on the same level as *.

Here is the presentation by Brent Yorgey

Typed type-level functional programming in GHC