GHC/Type system/PolyKinds

From HaskellWiki
< GHC‎ | Type system
Revision as of 19:40, 3 February 2021 by Ysangkok (talk | contribs) (fix link to ghc user guide)
Jump to: navigation, search

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.

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.