| | 24 | |
| | 25 | This section deals with a proposal to collapse kinds and sorts into a single system |
| | 26 | so as to allow Generalised Algebraic DataKinds (GADKs). The sort `BOX` should |
| | 27 | become a kind, whose ''kind'' is again `BOX`. Kinds would no longer be classified by sorts; |
| | 28 | they 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 |
| | 32 | concern for Haskell.) |
| | 33 | |
| | 34 | Collapsing kinds and sorts would allow some form of indexing on kinds. Consider the |
| | 35 | following two types, currently not promotable in FC-pro: |
| | 36 | {{{ |
| | 37 | data Proxy a = Proxy |
| | 38 | |
| | 39 | data Ind (n :: Nat) :: * where ... |
| | 40 | }}} |
| | 41 | In `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 |
| | 43 | polymorphism) is getting on the way of another new feature (promoting |
| | 44 | datatypes). As for `Ind`, it takes an argument of kind (promoted) `Nat`, |
| | 45 | which renders it non-promotable. Why is this? Well, promoted `Proxy` and `Ind` |
| | 46 | would have sorts: |
| | 47 | {{{ |
| | 48 | Proxy :: forall s. s -> BOX |
| | 49 | |
| | 50 | Ind :: 'Nat -> BOX |
| | 51 | }}} |
| | 52 | But `s` is a sort variable, and `'Nat` is the sort arising from promoting |
| | 53 | the kind `Nat` (which itself arose from promoting a datatype). FC-pro has |
| | 54 | neither 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` |
| | 56 | and `Ind` become: |
| | 57 | {{{ |
| | 58 | Proxy :: forall k. k -> BOX |
| | 59 | |
| | 60 | Ind :: Nat -> BOX |
| | 61 | }}} |
| | 62 | Now instead of sort variables we have kind variables, and we do not need to promote |
| | 63 | `Nat` again. |
| | 64 | |
| | 65 | Kind indexing alone should not require kind equality constraints; we always |
| | 66 | require 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] |
| | 68 | can be used to type check generalised algebraic kinds, avoiding the need for |
| | 69 | coercions. While this would still require some implementation effort, it |
| | 70 | should be "doable". |
