Difference between revisions of "GHC/Type system/PolyKinds"

From HaskellWiki
Jump to: navigation, search
(Kind polymorphism: fix link to promotion section in ghc user guide)
(Kind polymorphism: fix links to ghc users guide)
Line 3: Line 3:
 
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.
 
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.
   
* User manual sections about [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#kind-polymorphism kind polymorphism] and [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#datatype-promotion data type promotion]
 
  +
* {{GHCUsersGuide|exts/poly_kinds||a section on Kind Polymorphism}}. {{GHCUsersGuide|exts/data_kinds||another section on data-type promotion.}}
 
* [http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf Giving Haskell a promotion], the paper about it.
 
* [http://research.microsoft.com/en-us/people/dimitris/fc-kind-poly.pdf Giving Haskell a promotion], the paper about it.
   

Revision as of 23:31, 24 July 2021

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.