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