GHC/Type system/PolyKinds

Kind polymorphism

GHC 7.6 introduced kind polymorphism and data kinds for the first time. This page contains notes (currently rather random) about how to use these features.

• The GHC Users Guide has a section on Kind Polymorphism.. The GHC Users Guide has another section on data-type promotion..
• Giving Haskell a promotion, the paper about it.

Syntactic ambiguity for lists

Suppose Proxy :: forall k. k -> *, and consider

Proxy [Int]
Proxy [Int,Bool]

The former must mean what it always means in Haskell, namely

Proxy * (List Int)

where I'm writing the kind argument explicitly. To be fully clear, I'm writing List for the type constructor for lists (written [] in Haskell), so (List Int) is a type of kind *.

But Proxy [Int,Bool] can only mean Proxy applied to a list of types, thus:

Proxy [*] (Cons * Int (Cont * Bool (Nil *)))

Now we can see that Proxy [Int] is ambiguous. It could also mean

Proxy [*] (Cons * Int (Nil *))

but we choose the normal meaning to avoid screwing up Haskell programs. To get the above form we have to quote the "[", thus

	Proxy '[ Int ]

In short, singleton lists (and indeed the empty list) must be explicitly promoted with a quote, whereas for type-level lists of two or more elements you don't need an explicit promotion quote.