View source for 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.

* {{GHCUsersGuide|exts/poly_kinds||a section on Kind Polymorphism}}. {{GHCUsersGuide|exts/data_kinds||another section on data-type promotion.}} 
* [http://gallium.inria.fr/~jcretin/papers/fc-kind-poly.pdf Giving Haskell a promotion], the paper about it.

== Syntactic ambiguity for lists ==

Suppose <hask>Proxy :: forall k. k -> *</hask>, and consider
<haskell>
Proxy [Int]
Proxy [Int,Bool]
</haskell>
The former must mean what it always means in Haskell, namely 
<haskell>
Proxy * (List Int)
</haskell>
where I'm writing the kind argument explicitly. To be fully clear, I'm writing <hask>List</hask> for the type constructor for lists (written <hask>[]</hask> in Haskell), so <hask>(List Int)</hask> is a type of kind *.

But <hask>Proxy [Int,Bool]</hask> can only mean <hask>Proxy</hask> applied to a list of types, thus:
<haskell>
Proxy [*] (Cons * Int (Cont * Bool (Nil *)))
</haskell>
Now we can see that <hask>Proxy [Int]</hask> is ambiguous. It could also mean
<haskell>
Proxy [*] (Cons * Int (Nil *))
</haskell>
but we choose the normal meaning to avoid screwing up Haskell programs.  To get the above form we have to quote the "[", thus
<haskell>
	Proxy '[ Int ]
</haskell>
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.