48 | | === Typing rule for closed type families === |
49 | | |
50 | | Here are the declarative typing rules for closed type families. In these rules, we ignore arity/saturation issues and pretend that the kind is given with underscores instead of using the tyvarbndr syntax. |
51 | | |
52 | | {{{ |
53 | | k1 has at least one missing bit |
54 | | k2 = k1[k'1 .. k'n/_] -- k'1 .. k'n are magically known |
55 | | kvs = fkv(k2) |
56 | | G, kvs, F : k2 |- (F ps_i = t_i) ok -- but kvs aren't in scope for ps_i and t_i |
| 48 | === Typing rule for (BASELINE/NEWCUSK) === |
| 49 | |
| 50 | We will pretend that data, type, type family, class declarations look something like this: |
| 51 | {{{ |
| 52 | T :: forall k1 k2. (k1 -> *) -> k1 -> _ -> * |
| 53 | data/type/class T a b c = rhs |
| 54 | }}} |
| 55 | That is, there is a possibly-partial kind signature, with holes denoted by "_", and a definition "rhs" (eg the consructors of a dat type, or equations of a closed type family). In reality there isn't a separate kind signature; instead, it is integrated in the definition; e.g. |
| 56 | {{{ |
| 57 | data T (a::k1 -> *) (b::k1) c = MkT (a b) c |
| 58 | }}} |
| 59 | The kind variables mentioned in the partial kind signature scope over the "rhs". |
| 60 | |
| 61 | Then we have two typing rules, one for CUSK, and one for non-CUSK. |
| 62 | We give the rule for data types but modulo keyword it works for classes, closed |
| 63 | type families, etc. We ignore arity/saturation issues for type families. |
| 64 | {{{ |
| 65 | k has at least one missing bit (non-CUSK) |
| 66 | k2 = k[k'1 .. k'n/_] -- k'1 .. k'n are magically known |
| 67 | kvs2 = fkv(k2) |
| 68 | G, kvs, T : k2 |- (data T tvs = rhs) ok -- Monomorphic recursion |
64 | | G |- type family F :: k where { F ps_i = t_i } : forall kvs. k |
65 | | }}} |
66 | | |
67 | | We need two rules, depending on whether or not a CUSK is detected. The first rule requires the equations to be fully parametric in its kinds, whereas the second allows non-parametric equations and polymorphic recursion. These rules are ''different'' than the implementation today, because kind inference for closed type families today is ill-specified. See comment:18:ticket:9200. |
| 75 | G |- (T :: forall kvs. k; data T tvs = rhs) :: {T :: forall kvs. k} |
| 76 | }}} |
| 77 | |
| 78 | We need two rules, depending on whether or not a CUSK is detected. |
| 79 | |
| 80 | The first rule requires the equations to be fully parametric in its kinds, whereas the second allows non-parametric equations and polymorphic recursion. '''Simon:''' I don't know what this means. |
| 81 | |
| 82 | For closed type families, these rules are ''different'' than the implementation today, because kind inference for closed type families today is ill-specified. See comment:18:ticket:9200. |