Difference between revisions of "GHC/Type system/PolyKinds"
(fix link to ghc user guide) |
(→Kind polymorphism: fix link to promotion section in ghc user 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 [ | + | * 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] |
* [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 19:40, 3 February 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.
- User manual sections about kind polymorphism and 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.