Changes between Version 12 and Version 13 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 1:58:08 PM (11 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v12 v13  
    3535(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.) 
    3636 
    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. 
     37 
    3838 
    3939== Coincident overlap ==  
     
    4848These instances surely overlap, but in the case when they do, the right-hand sides coincide. We call this '''coincident overlap'''. 
    4949 
    50 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.  However, we can recover coincident overlap with in a branched instance: see [wiki:NewAxioms/CoincidentOverlap here].  
     50However, 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'''.  However, we can recover coincident overlap with in a branched instance: see [wiki:NewAxioms/CoincidentOverlap here].  
    5151 
    5252