Changes between Version 7 and Version 8 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 1:46:12 PM (21 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v7 v8  
    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''' 
     30We call the "version of the instance where all variables are distinct" the "linearised form" of the instance. 
    3031Using 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. 
    3132 
     
    3334 
    3435(Interestingly, proofs of the soundness of the existing system have been published. For example, see [http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/fc-tldi.pdf here] and [http://www.cis.upenn.edu/~stevez/papers/WVPJZ11.pdf here]. These proofs are not necessarily incorrect, but they implicitly don't allow nonlinear family instances.) 
     36 
     37This new overlap check only looks at the ''left hand side'' of the instance. The alert reader will know that GHC currently also looks at the ''right hand side'', which we return to in "coincident overlap" below. 
    3538 
    3639== Branched instances ==