Changes between Version 3 and Version 4 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 29, 2013 12:44:25 PM (11 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v3 v4  
    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: when performing the overlap check, check a version of the instance where all variables are distinct. Using such a check, the two instances for {{{F}}} above indeed conflict. 
    2929 
    30 This can break existing code. But, a medium-intensity search did not find ''any'' uses of non-linear (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 -- the current system is subtly broken and has been so for years. 
     30This 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 -- the current system is subtly broken and has been so for years. 
    3131 
    32 (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 non-linear family instances.) 
     32(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.) 
    3333 
    3434== Branched instances == 
     
    7575== Alternative (Non-)Solution == 
    7676 
    77 One way we (Simon, Dimitrios, and Richard) considered proceeding was to prohibit non-linear unbranched instances entirely. Unfortunately, that doesn't work. Consider this: 
     77One way we (Simon, Dimitrios, and Richard) considered proceeding was to prohibit nonlinear unbranched instances entirely. Unfortunately, that doesn't work. Consider this: 
    7878 
    7979{{{ 
     
    8282}}} 
    8383 
    84 Innocent enough, it seems. However, that instance expands to {{{type instance H k ('[] k) = Bool}}} internally. And that expansion contains a repeated variable! Yuck. We Thought Hard about this and came up with various proposals to fix it, but we weren't convinced that any of them were any good. So, we concluded to allow non-linear unbranched instances, but we linearize them when checking overlap. This may surprise some users, but we will put in a helpful error message in this case. 
     84Innocent enough, it seems. However, that instance expands to {{{type instance H k ('[] k) = Bool}}} internally. And that expansion contains a repeated variable! Yuck. We Thought Hard about this and came up with various proposals to fix it, but we weren't convinced that any of them were any good. So, we concluded to allow nonlinear unbranched instances, but we linearize them when checking overlap. This may surprise some users, but we will put in a helpful error message in this case.