Changes between Version 53 and Version 54 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 17, 2008 9:02:36 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v53 v54  
    1 = Normalising and Solving Type Equalities = 
     1= Entailment of Type Equalities = 
     2 
     3Our aims is to derive the entailment judgement 
     4{{{ 
     5  g1, .., gn  |-  w1, .., wm 
     6}}} 
     7i.e., whether we can derive the wanted equalities `w1` to `wm` from the given equalities `g1`, .., `gn` under a given set of toplevel equality schemas (i.e., equalities involving universally quantified variables).  We permit unification variables in the wanted equalities, and a derivation may include the instantiation of these variables; i.e., may compute a unifier.  However, that unifer must be most general. 
     8 
     9The derivation algorithm is complicated by the pragmatic requirement that, even if there is no derivation for the judgement, we would like to compute a unifier.  This unifier should be as specific as possible under some not yet specified (strongest) weakening of the judgement so that it is derivable.  (Whatever that means...) 
    210 
    311The following is based on ideas for the new, post-ICFP'08 solving algorithm described in CVS `papers/type-synonym/new-single.tex`.  A revised version of `new-single.tex` that integrates the core ideas from this wiki page is in `papers/type-synonym/normalised_equations_algorithm.tex`.  Most of the code is in the module `TcTyFuns`.