Changes between Version 18 and Version 19 of GhcKinds

Dec 15, 2011 11:31:08 AM (6 years ago)



  • GhcKinds

    v18 v19  
    2323= Generalized Algebraic Data Kinds (GADKs) =
     25This section deals with a proposal to collapse kinds and sorts into a single system
     26so as to allow Generalised Algebraic DataKinds (GADKs). The sort `BOX` should
     27become a kind, whose ''kind'' is again `BOX`. Kinds would no longer be classified by sorts;
     28they would be classified by kinds.
     30(As an aside, sets containing themselves result in an inconsistent system; see, for instance,
     31[ this example]. This is not of practical
     32concern for Haskell.)
     34Collapsing kinds and sorts would allow some form of indexing on kinds. Consider the
     35following two types, currently not promotable in FC-pro:
     37data Proxy a = Proxy
     39data Ind (n :: Nat) :: * where ...
     41In `Proxy`, `a` has kind `forall k. k`. This type is not promotable because
     42`a` does not have kind `*`. This is unfortunate, since a new feature (kind
     43polymorphism) is getting on the way of another new feature (promoting
     44datatypes). As for `Ind`, it takes an argument of kind (promoted) `Nat`,
     45which renders it non-promotable. Why is this? Well, promoted `Proxy` and `Ind`
     46would have sorts:
     48Proxy  :: forall s. s -> BOX
     50Ind    :: 'Nat -> BOX
     52But `s` is a sort variable, and `'Nat` is the sort arising from promoting
     53the kind `Nat` (which itself arose from promoting a datatype). FC-pro has
     54neither sort variables nor promoted sorts. However, if there are no sorts, and
     55`BOX` is the '''kind''' of all kinds, the "sorts" ("kinds", now) of promoted `Proxy`
     56and `Ind` become:
     58Proxy  :: forall k. k  -> BOX
     60Ind    :: Nat          -> BOX
     62Now instead of sort variables we have kind variables, and we do not need to promote
     63`Nat` again.
     65Kind indexing alone should not require kind equality constraints; we always
     66require type/kind signatures for kind polymorphic stuff, so then
     67[ wobbly types]
     68can be used to type check generalised algebraic kinds, avoiding the need for
     69coercions. While this would still require some implementation effort, it
     70should be "doable".