Changes between Version 23 and Version 24 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 3, 2008 6:37:05 AM (7 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.