Changes between Version 18 and Version 19 of GhcKinds


Ignore:
Timestamp:
Dec 15, 2011 11:31:08 AM (2 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".