Changes between Version 16 and Version 17 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 2:28:18 PM (11 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v16 v17  
    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:  
    2929 * '''when performing the overlap check between two instances, check a version of the instances where all variables are distinct''' 
    30 We call the "version of the instance where all variables are distinct" the "linearised form" of the instance. 
     30We 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. 
    3232 
     
    4747These instances surely overlap, but in the case when they do, the right-hand sides coincide. We call this '''coincident overlap'''. 
    4848 
    49 However, the above proposal of linearising the LHS before checking overlap 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 singelton type instance and a branched one; it is currently only supported between singleton type instances.) 
     49However, the above proposal of linearizing the LHS before checking overlap 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.) 
    5050 
    5151However, we can recover coincident overlap with in a branched instance: see [wiki:NewAxioms/CoincidentOverlap here].  
     
    107107 * After linearizing a left-hand side, the right-hand side of the instance is ill-defined. Thus, the current coincidence check (see [wiki:NewAxioms/CoincidentOverlap here] for more information) is no longer possible and will be removed. (Don't yell yet. Keep reading.) 
    108108 
    109  * Add type space declarations to the {{{type instance where}}} syntax, checking to make sure that branches fit within the declared space. 
     109 * Allow coincident overlap within branched instances. This recovers the lost coincident overlap check on unbranched instances. See [wiki:NewAxioms/CoincidentOverlap here] for more information. 
    110110 
    111  * Allow coincident overlap within branched instances. This recovers the lost coincident overlap check on unbranched instances. See [wiki:NewAxioms/CoincidentOverlap here] for more information. 
     111 * Optional: Add type space declarations to the {{{type instance where}}} syntax, checking to make sure that branches fit within the declared space. [wiki:NewAxioms/TypeSpaces This page] has the details. 
    112112 
    113113 * Optional: Add new syntax {{{type family Foo a b where { Foo ... = ... ; Foo ... = ... } }}} to declare a type family with one branched instance covering the entire type space. This would be a ''closed'' type family.