Changes between Version 23 and Version 24 of TypeFunctionsSolving
 Timestamp:
 Aug 3, 2008 6:37:05 AM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v23 v24 1 1 = Normalising and Solving Type Equalities = 2 2 3 The following is based on ideas for the new, postICFP'08 solving algorithm. Technical details are in CVS `papers/typesynonym/newsingle.tex`. Most of the code is in the module `TcTyFuns`. 3 The following is based on ideas for the new, postICFP'08 solving algorithm described in CVS `papers/typesynonym/newsingle.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 4 17 5 18 == Overall algorithm == 6 19 7 20 The overall algorithm is as in `newsingle.tex`, namely 8 * Normalise all constraints (both locals and wanteds)9 * Solve the wanteds10 * Finalise21 1. normalise all constraints (both locals and wanteds), 22 2. solve the wanteds, and 23 3. finalise. 11 24 12 25 == Normal equalities == … … 19 32 20 33 The types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families. Moreover, in Forms (2) & (3), the left and righthand side need to be different, and the lefthand side may not occur in the righthand side. 21 22 '''SLPJ''': Terminology: I think "flexible type variable" = "unification variable" = "HM variable".23 34 24 35 '''SLPJ''': I think that you intend a "normal equality" to embody the Orientation Invariant and the Flattening Invariant from newsingle.tex. But they don't line up exactly. For example, what about `F [x] ~ G x`? That satisfies both invariants.