|Version 32 (modified by simonpj, 23 months ago) (diff)|
Kind polymorphism and datatype promotion
This page gives additional implementation details for the -XPolyKinds flag. The grand design is described in the paper Giving Haskell a Promotion. Most of the work has been done and merged into GHC 7.4.1. The relevant user documentation is in [the user's guide (add link when it's up)] and on the Haskell wiki page. What still doesn't work, or doesn't work correctly, is described here.
- GhcKinds/PolyTypeable A kind-polymorphic version of the Typeable class.
- ExplicitTypeApplication proposes a syntax for explicit kind application
Kind defaulting in type families
At the moment, when you define a type family without -XPolyKinds like this:
type family F a
it gets kind * -> *. There are no constraints on the kind of a, so we default it to *. We also default the return kind of F to *. The same happens for data families, and also for plain datatypes with phantom types.
When you turn -XPolyKinds on, however, we currently give F the kind forall (k :: BOX). k -> *. This is unsatisfactory for two reasons:
- The behaviour of kind generalisation changes when we turn -XPolyKinds on, even though it doesn't really have to. We could still default to * unless you give a kind signature. So if you want F to be kind polymorphic, you should write type family F (a :: k). This, of course, requires supporting explicit kind variables.
- Unlike the parameters, however, the return kind of F is defaulted to *.
This seems rather arbitrary. We should either generalise both arguments and
return kind, or default both. In case we choose to default, the more
general kind can be obtained by giving a signature:
type family F (a :: k1) :: k2
Future work: do more consistent kind defaulting.
#5682 (proper handling of infix promoted constructors)
Bug report #5682 shows a problem in parsing promoted infix datatypes.
Future work: handle kind operators properly in the parser.
Kind synonyms (from type synonym promotion)
At the moment we are not promoting type synonyms, i.e. the following is invalid:
data Nat = Ze | Su Nat type Nat2 = Nat type family Add (m :: Nat2) (n :: Nat2) :: Nat2
Future work: promote type synonyms to kind synonyms.
Generalized Algebraic Data Kinds (GADKs)
Future work: this section deals with a proposal to collapse kinds and sorts into a single system so as to allow Generalised Algebraic DataKinds (GADKs). The sort BOX should become a kind, whose kind is again BOX. Kinds would no longer be classified by sorts; they would be classified by kinds.
(As an aside, sets containing themselves result in an inconsistent system; see, for instance, this example. This is not of practical concern for Haskell.)
Collapsing kinds and sorts would allow some form of indexing on kinds. Consider the following two types, currently not promotable in FC-pro:
data Proxy a = Proxy data Ind (n :: Nat) :: * where ...
In Proxy, a has kind forall k. k. This type is not promotable because a does not have kind *. This is unfortunate, since a new feature (kind polymorphism) is getting on the way of another new feature (promoting datatypes). As for Ind, it takes an argument of kind (promoted) Nat, which renders it non-promotable. Why is this? Well, promoted Proxy and Ind would have sorts:
Proxy :: forall s. s -> BOX Ind :: 'Nat -> BOX
But s is a sort variable, and 'Nat is the sort arising from promoting the kind Nat (which itself arose from promoting a datatype). FC-pro has neither sort variables nor promoted sorts. However, if there are no sorts, and BOX is the kind of all kinds, the "sorts" ("kinds", now) of promoted Proxy and Ind become:
Proxy :: forall k. k -> BOX Ind :: Nat -> BOX
Now instead of sort variables we have kind variables, and we do not need to promote Nat again.
Kind indexing alone should not require kind equality constraints; we always require type/kind signatures for kind polymorphic stuff, so then wobbly types can be used to type check generalised algebraic kinds, avoiding the need for coercions. While this would still require some implementation effort, it should be "doable".