Changes between Version 7 and Version 8 of NewAxioms/Nonlinearity
 Timestamp:
 May 29, 2013 1:46:12 PM (3 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

NewAxioms/Nonlinearity
v7 v8 28 28 We 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 29 * '''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. 30 31 Using 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. 31 32 … … 33 34 34 35 (Interestingly, proofs of the soundness of the existing system have been published. For example, see [http://research.microsoft.com/enus/um/people/simonpj/papers/extf/fctldi.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 37 This 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. 35 38 36 39 == Branched instances ==