Changes between Version 28 and Version 29 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
Jul 23, 2017 5:48:40 AM (2 years ago)
Author:
takenobu
Comment:

Fix broken link

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v28 v29  
    3535This can break existing code. But, a medium-intensity search did not find ''any'' uses of nonlinear (i.e. with a repeated variable) family instances in existing code, so I think we should be OK. However, a change needs to be made to be confident that nonlinear axioms and undecidable instances do not introduce a type-soundness hole into GHC.
    3636
    37 (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  incorrect, but they  don't allow both undecidable instances and nonlinear family instances.)
     37(Interestingly, proofs of the soundness of the existing system have been published. For example, see [https://www.microsoft.com/en-us/research/wp-content/uploads/2007/01/tldi22-sulzmann-with-appendix.pdf here] and [http://www.cis.upenn.edu/~stevez/papers/WVPJZ11.pdf here]. These proofs are not  incorrect, but they  don't allow both undecidable instances and nonlinear family instances.)
    3838
    3939Conor's alternative general idea: