Changes between Version 26 and Version 27 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
Jun 16, 2013 3:47:26 PM (10 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v26 v27  
    7272However, the above proposal of linearizing the LHS before checking overlap (plan (A)) makes a nonsense of exploiting coincident overlap, because when we freshen the LHS we no longer bind the variables in the RHS. '''So the proposal abandons support for coincident overlap between standalone type instances'''.  (It's worth noting, though, that there is already no support for coincident overlap between branched type instances, or between a singleton type instance and a branched one; it is currently only supported between singleton type instances.) 
    7373 
    74 Plan (B) above has a better relationship with coincident overlap, but not quite a rosy one: in the event that an infinite type is needed to show the overlap, we don't have a well-defined substitution to apply to the RHS. It is conceivable to allow coincident overlap only when the unification algorithm produces a bona fide substitution. But, there may be no need for this. 
    75  
    76 However, we can recover coincident overlap with in a branched instance: see [wiki:NewAxioms/CoincidentOverlap here].  
     74Plan (B) above has a better relationship with coincident overlap, but not quite a rosy one: in the event that an infinite type is needed to show the overlap, we don't have a well-defined substitution to apply to the RHS. It is conceivable to allow coincident overlap only when the unification algorithm produces a bona fide substitution. 
    7775 
    7876== Concrete Proposal == 
     
    8078 * Use plan (B) to check for overlap. Thus, our two problematic instances of {{{F}}}, at the top, will conflict. 
    8179 
    82  * The current coincidence check (see [wiki:NewAxioms/CoincidentOverlap here] for more information) is no longer straightforward and will be removed. (Don't yell yet. Keep reading.) 
     80 * Continue to allow coincident overlap in standalone instances. 
    8381 
    84  * Allow coincident overlap within branched instances. This recovers the lost coincident overlap check on unbranched instances. See [wiki:NewAxioms/CoincidentOverlap here] for more information. 
     82 * Allow coincident overlap within branched instances. See [wiki:NewAxioms/CoincidentOverlap here] for more information. 
    8583 
    8684 * Optional: Change the syntax for branched family instances, as described [wiki:NewAxioms/ClosedTypeFamilies here].