Changes between Version 19 and Version 20 of GhcKinds/KindInference


Ignore:
Timestamp:
Jun 19, 2014 9:53:25 PM (5 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindInference

    v19 v20  
    4242
    4343A somewhat simpler, but more permissive definition, and one that covers classes, is this:
    44  * A class or datatype is said to have a CUSK if and only if all of its type variables are annotated.
     44 * A class or datatype is said to have a CUSK if and only if all of its type variables are annotated. 
    4545
    4646See comment:19:ticket:9200 for more exposition.
    4747
    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
     50We 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}}}
     55That 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}}}
     59The kind variables mentioned in the partial kind signature scope over the "rhs".
     60
     61Then we have two typing rules, one for CUSK, and one for non-CUSK.
     62We give the rule for data types but modulo keyword it works for classes, closed
     63type families, etc.  We ignore arity/saturation issues for type families.
     64{{{
     65k has at least one missing bit (non-CUSK)
     66k2 = k[k'1 .. k'n/_]     -- k'1 .. k'n are magically known
     67kvs2 = fkv(k2)
     68G, kvs, T : k2 |- (data T tvs = rhs) ok    -- Monomorphic recursion
    5769----------------------------------------------------- NoCUSK
    58 G |- type family F :: k1 where { F ps_i = t_i } : forall kvs. k2
    59 
    60 k has no missing bits
    61 kvs = fkv(k)
    62 G, F : forall kvs. k |- (F ps_i = t_i) ok
     70G |- (T :: forall kvs. k; data T tvs = rhs) :: {T :: forall kvs2. k2}
     71
     72k has no missing bits (CUSK)
     73G, T : forall kvs. k |- (T tvs = rhs) ok  -- Polymorphic recursion
    6374----------------------------------------------------- CUSK
    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.
     75G |- (T :: forall kvs. k; data T tvs = rhs) :: {T :: forall kvs. k}
     76}}}
     77
     78We need two rules, depending on whether or not a CUSK is detected.
     79
     80The 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
     82For 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.
    6883
    6984----------------------------------