Changes between Version 4 and Version 5 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 1:12:31 PM (2 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v4 v5  
    7373 * 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. 
    7474 
     75== Discussion about coincident overlap == 
     76 
     77This proposal has the net effect of forcing all uses of coincident overlap to appear in one module, instead of spread across modules. That's admittedly not great, but it's possible that no one will be negatively affected. The only alternative we've (Simon, Dimitrios, Richard) thought of is to disallow coincident overlap when the left-hand sides are non-linear, but that seems very ugly and ad-hoc. 
     78 
     79To see why disallowing coincident overlap checking for unbranched axioms is vitally necessary, consider this example: 
     80 
     81{{{ 
     82type instance F a a Int = a 
     83type instance F c d d   = Int 
     84}}} 
     85 
     86No, they most certainly are not OK (think about {{{F G G G}}}, where this is the malignant {{{G}}} from the beginning of this page), but they do coincide in the region of overlap. Yuck Yuck! So, we give up and just say "no" to coincident overlap in this case. 
     87 
    7588== Alternative (Non-)Solution == 
    7689