Changes between Version 18 and Version 19 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 30, 2013 3:14:12 PM (11 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v18 v19  
    2727 
    2828We 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''' 
    3030We call the "version of the instance where all variables are distinct" the "linearized form" of the instance. 
    3131Using 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. 
     
    3636 
    3737Conor'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''' 
     39This 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}}} 
     44These would be considered overlapping by (A), but accepted as non-overlapping (ie unification fails) by (B). 
    4045 
    4146== Problem: coincident overlap ==