Changes between Version 24 and Version 25 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 3, 2008 7:26:56 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v24 v25  
    22
    33The following is based on ideas for the new, post-ICFP'08 solving algorithm described in CVS `papers/type-synonym/new-single.tex`.  Most of the code is in the module `TcTyFuns`.
     4
    45
    56== Terminology ==
     
    1516
    1617
    17 
    1818== Overall algorithm ==
    1919
     
    2323 3. finalise.
    2424
     25
    2526== Normal equalities ==
    2627
     
    3132 3. `co :: a ~ t`, where `a` is a rigid type variable (skolem) and `t` is ''not'' a flexible type variable.
    3233
    33 The types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families.  Moreover, in Forms (2) & (3), the left- and right-hand side need to be different, and the left-hand side may not occur in the right-hand side.
    34 
    35 '''SLPJ''': I think that you intend a "normal equality" to embody the Orientation Invariant and the Flattening Invariant from new-single.tex.  But they don't line up exactly.  For example, what about `F [x] ~ G x`?  That satisfies both invariants.
    36 
    37 NB: We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.
    38 
    39 Coercions `co` are either wanteds (represented by a flexible type variable) or givens ''aka'' locals (represented by a type term of kind CO).  In GHC, they are represented by `TcRnTypes.EqInstCo`.   Moreover, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules.  '''SLPJ''' but I hope the difference between wanted and given is explicit (different constructor) not implicit (look at the form of the coercion).
     34where
     35
     36 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, and
     37 * we call the Forms (2) & (3) '''variable equalities''', and require that the left- and right-hand side need to be different, and that the left-hand side does not occur in the right-hand side.
     38
     39=== Observations ===
     40
     41The following is interesting to note:
     42
     43 * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.
     44 * Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of new-single, but they are not the same.
     45 * Normal equalities are '''never''' recursive.  They can be mutually recursive.  A mutually recursive group will exclusively contain variable equalities.
     46
     47=== Coercions ===
     48
     49Coercions `co` are either wanteds (represented by a flexible type variable) or givens ''aka'' locals (represented by a type term of kind CO).  In GHC, they are represented by `TcRnTypes.EqInstCo`, which is defined as
     50{{{
     51type EqInstCo = Either
     52                  TcTyVar    -- case for wanteds (variable to be filled with a witness)
     53                  Coercion   -- case for locals
     54}}}
     55Moreover, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules.
    4056
    4157