Changes between Version 18 and Version 19 of GhcKinds

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