Changes between Version 20 and Version 21 of GhcKinds/KindInference


Ignore:
Timestamp:
Jul 24, 2014 9:59:40 PM (5 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • GhcKinds/KindInference

    v20 v21  
    11= Kind inference for types and classes =
    22
    3 This page summarises several alternative designs, which are debated on #9200.  (See also #9201.)
    4 
    5 ==  Baseline strategy (BASELINE) ==
    6 
    7 This plan, originally due to Mark Jones, is the strategy that GHC 7.8 follows for ordinary, recursive term-level functions, and for recursive data types.  I'll describe it for data types, with this example:
     3This page summarises several alternative designs for doing kind inference for
     4types and classes, under `-XPolyKinds`.  See the extensive discussion on #9200.  (See also #9201.)
     5
     6== Current strategy (GHC 7.8) ==
     7
     8Running example:
     9{{{
     10  data T a f = T1 Int (T a f) | T2 (f a)
     11
     12  data S a f = S1 (S Maybe (S Int))
     13}}}
     14
     15Here is GHC 7.8's strategy:
     16
     17 1. Sort data/type/class declarations into strongly connected components.  In our example, there are two recursive SCCs, one for `T` and one for `S`.
     18 
     19 2. Then, for each SCC in turn:
     20
     21    * Bind the type constructor to a fresh meta-kind variable:
     22{{{
     23        T :: kappa0
     24}}}
     25    * Kind-check all the declarations of the SCC in this environment.  This will generate some unifications, so in the end we get
     26{{{
     27        kappa0 ~ kappa1 -> (kappa1 -> *) -> *
     28}}}
     29    * Generalise.  So we get
     30{{{
     31        T :: forall k. k -> (k -> *) -> *
     32}}}
     33Following the same three steps for `S` fails, because we need polymorphic recursion.  Srarting with `S :: kappa0`, we get
     34{{{
     35  kappa0 ~ kappa1 -> kappa2 -> *    -- S has two arguments
     36  kappa1 ~ *->*                     -- From (S Maybe)
     37  kappa1 ~ *                        -- From (S Int)
     38  ...and some more...
     39}}}
     40So in GHC 7.8 you can supply a "complete user kind signature" (CUSK) for `S`, thus:
     41{{{
     42  data S (a :: k) (f :: k -> *) where
     43     S1 :: S Maybe (S Int) -> S a f
     44}}}
     45The real step 2 works thus:
     46    * Bind the each non-CUSK type constructor to a fresh meta-kind variable, and each CUSK type constructor to its polymorphic kind.
     47{{{
     48        S :: forall k. k -> (k->*) -> *
     49}}}
     50    * Kind-check all the declarations of the SCC in this environment.  With this new kind for `S`, kind checking succeeds.
     51
     52    * Generalise any non-CUSK type constructors.
     53
     54== Proposed new strategy ==
     55
     56The main proposed change is to the definition of a "complete user kind signature" (CUSK).  The current story is in [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind-polymorphism.html#complete-kind-signatures Section 7.8.3 of the user manual].  Alas, it does not allow CUSKs for class declarations.
     57The new proposal is this:
     58 * A class or datatype is said to have a CUSK if and only if all of its type variables are annotated.
     59This is somewhat simpler, it covers classes. See comment:19:ticket:9200 for more exposition.
     60This change alone is enough to satisfy #9200.
     61
     62'''Simon''' What about type synonym declarations. Don't we need a kind signature on the RHS?
     63
     64==  A possible variation ==
     65
     66This algorithm is not quite as expressive as it could be.  Consider
    867{{{
    968   data SS f a b = MkSS (TT a f) (SS f a b)
     
    1170      MkTT :: f a -> SS f a Maybe -> SS f a Int -> TT a f
    1271}}}
    13  1. Identify which type constructors have Complete User Type Signatures (CUSK).  In this example, `TT` does. Extend the environment with these, fixed, kinds:
     72Here `TT` has a CUSK, but `SS` does not.  Hence in step 1 we'd bind `SS :: kappa0`. But in the RHS of `TT` we use `SS` at two different kinds, so infernece will fail.  We could solve this by giving a CUSK to `SS` as well.
     73
     74However, we can ''also'' solve it using a plan due to Mark Jones, and one that GHC 7.8 already follows for ordinary, recursive term-level functions.  As usual, divide the declarations into SCCs, and then for each SCC do the following:
     75
     76 * Identify which type constructors have Complete User Type Signatures (CUSK).  In this example, `TT` does. Extend the environment with these, fixed, kinds:
    1477{{{
    1578       TT :: forall k. k -> (k->*) -> *
    1679}}}
    17  2. Perform strongly-connected component (SCC) analysis on the non-CUSK decls, ''ignoring'' dependencies on a type constructor with a CUSK.  In our example, we get a single recursive SCC, containing `SS`.
    18 
    19  3. For each SCC in turn:
     80 * Perform a new strongly-connected component (SCC) analysis on the non-CUSK decls in the SCC, ''ignoring dependencies on a type constructor with a CUSK''.  In our example, we get a single recursive SCC, containing `SS`.
     81
     82 * For each SCC in turn:
    2083    * Bind the type constructor to a fresh meta-kind variable:
    2184{{{
     
    3194        SS :: forall k1 k2. (k1->*) -> k1 -> k2 -> *
    3295}}}
    33  4. Extend the environment with these generalised kind bindings, and kind-check the CUSK declarations.
     96 * Extend the environment with these generalised kind bindings, and kind-check the CUSK declarations.
    3497
    3598The Key Point is that we can kind-check `SS` ''without looking at `TT`'s definition at all'', because we completely know `TT`'s kind.  That in turn means that we can exploit ''inferred'' polymorphism for `SS` when kind-checking `TT`.  As we do here: `TT` uses `SS` in two different ways `(SS f a Maybe)` and `(SS f a Int)`.
    3699
    37 Note that for a ''non-recursive'' type or class declaration, (BASELINE) always works fine.
    38 
    39 === Refine the definition of CUSK (BASELINE/NEWCUSK) ===
    40 
    41 GHC's current definition of a complete user-supplied kind signature is [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind-polymorphism.html#complete-kind-signatures here in the user manual].  A big disadvantage is that classes can't have a CUSK under that definition.
    42 
    43 A 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.
    45 
    46 See comment:19:ticket:9200 for more exposition.
    47 
    48 === Typing rule for (BASELINE/NEWCUSK) ===
    49 
     100This strategy is more complicated than the initial proposal, but allows fewer annotations.  It's not clear whether it is wroth the bother.
     101
     102=== Typing rule for the new proposal ===
     103
     104An algorithm is all very well, but what about the typing judgements?
    50105We will pretend that data, type, type family, class declarations look something like this:
    51106{{{
     
    53108  data/type/class T a b c = rhs
    54109}}}
    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.
     110That is, there is a possibly-partial kind signature, with holes denoted by "_", and a definition "rhs" (eg the consructors of a data 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.
    56111{{{
    57112  data T (a::k1 -> *) (b::k1) c = MkT (a b) c
     
    66121k2 = k[k'1 .. k'n/_]     -- k'1 .. k'n are magically known
    67122kvs2 = fkv(k2)
    68 G, kvs, T : k2 |- (data T tvs = rhs) ok    -- Monomorphic recursion
     123G, kvs2, T : k2 |- (data T tvs = rhs) ok    -- Monomorphic recursion
    69124----------------------------------------------------- NoCUSK
    70125G |- (T :: forall kvs. k; data T tvs = rhs) :: {T :: forall kvs2. k2}