Changes between Version 18 and Version 19 of GhcKinds


Ignore:
Timestamp:
Dec 15, 2011 11:31:08 AM (4 years ago)
Author:
dreixel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds

    v18 v19  
    2222
    2323= Generalized Algebraic Data Kinds (GADKs) =
     24
     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.
     29
     30(As an aside, sets containing themselves result in an inconsistent system; see, for instance,
     31[http://www.cs.nott.ac.uk/~txa/g53cfr/l20.agda this example]. This is not of practical
     32concern for Haskell.)
     33
     34Collapsing kinds and sorts would allow some form of indexing on kinds. Consider the
     35following two types, currently not promotable in FC-pro:
     36{{{
     37data Proxy a = Proxy
     38
     39data Ind (n :: Nat) :: * where ...
     40}}}
     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:
     47{{{
     48Proxy  :: forall s. s -> BOX
     49
     50Ind    :: 'Nat -> BOX
     51}}}
     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:
     57{{{
     58Proxy  :: forall k. k  -> BOX
     59
     60Ind    :: Nat          -> BOX
     61}}}
     62Now instead of sort variables we have kind variables, and we do not need to promote
     63`Nat` again.
     64
     65Kind indexing alone should not require kind equality constraints; we always
     66require type/kind signatures for kind polymorphic stuff, so then
     67[http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/gadt-rigid-contexts.pdf 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".