Changes between Version 18 and Version 19 of NewAxioms/Nonlinearity
 Timestamp:
 May 30, 2013 3:14:12 PM (22 months ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms/Nonlinearity
v18 v19 27 27 28 28 We need to consider the two instances of {{{F}}} to be overlapping and inadmissible. There are a handful of ways to do this, but the best seems to be this: 29 * '''when performing the overlap check between two instances, check a version of the instances where all variables are distinct'''29 * (A) '''when performing the overlap check between two instances, check a version of the instances where all variables are distinct''' 30 30 We call the "version of the instance where all variables are distinct" the "linearized form" of the instance. 31 31 Using such a check, the two instances for {{{F}}} above indeed conflict, because we would compare `(F a b)` against `(F [c] d)`, where a,b,c,d are the fresh distinct variables. … … 36 36 37 37 Conor's alternative general idea: 38 * '''when performing the overlap check, during unification succeed (instead of failing) if the occurs check happens''' 39 38 * (B) '''when performing the overlap check, during unification succeed (instead of failing) if the occurs check happens''' 39 This is a bit more permissive than (A). For example 40 {{{ 41 type instance F x x = blah 42 type instance F Int Bool = boo 43 }}} 44 These would be considered overlapping by (A), but accepted as nonoverlapping (ie unification fails) by (B). 40 45 41 46 == Problem: coincident overlap ==