Changes between Version 23 and Version 24 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
08/02/08 23:37:05 (5 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • TypeFunctionsSolving

    v23 v24  
    11= Normalising and Solving Type Equalities = 
    22 
    3 The following is based on ideas for the new, post-ICFP'08 solving algorithm.  Technical details are in CVS `papers/type-synonym/new-single.tex`.  Most of the code is in the module `TcTyFuns`. 
     3The 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 
     5== Terminology == 
     6 
     7 ''Wanted equality'':: 
     8  An equality constraint that we need to derive during type checking.  Failure to derive it leads to rejection of the checked program. 
     9 ''Local equality'', ''given equality'':: 
     10  An equality constraint that -in a certain scope- may be used to derive wanted equalities. 
     11 ''Flexible type variable'',  ''unification variable'', ''HM variable''::  
     12  Type variables that may be '''globally''' instantiated by unification. 
     13 ''Rigid type variable'', ''skolem type variable'':: 
     14  Type variable that cannot be globally instantiated, but it may be '''locally''' refined by a local equality constraint. 
     15 
     16 
    417 
    518== Overall algorithm == 
    619 
    720The overall algorithm is as in `new-single.tex`, namely 
    8  * Normalise all constraints (both locals and wanteds) 
    9  * Solve the wanteds 
    10  * Finalise 
     21 1. normalise all constraints (both locals and wanteds), 
     22 2. solve the wanteds, and 
     23 3. finalise. 
    1124 
    1225== Normal equalities == 
    … …  
    1932 
    2033The 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. 
    21  
    22 '''SLPJ''': Terminology: I think "flexible type variable" = "unification variable" = "HM variable". 
    2334 
    2435'''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.