Changes between Version 1 and Version 2 of NewAxioms/Nonlinearity

May 29, 2013 12:42:21 PM (4 years ago)



  • NewAxioms/Nonlinearity

    v1 v2  
    2828This 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.
    30 (Interestingly, proofs of the soundness of the existing system have been published. For example, see here and here.
     30(Interestingly, proofs of the soundness of the existing system have been published. For example, see [ here] and [ here]. These proofs are not necessarily incorrect, but they implicitly don't allow non-linear family instances.)
     32== Branched instances ==
     34But, how does this interact with branched instances (those new instance forms that allow for ordered overlapping)? We still need nonlinear branched instances, as the canonical example of a nonlinear instance is an equality test. The solution is to declare a ''type space'' that all branches fit within.
     36Here are some examples, leaving off the {{{type family}}} headers:
     39type instance Equals x y where
     40  Equals x x = True
     41  Equals x y = False
     45type instance F Int x where
     46  F Int Bool = Double
     47  F Int Int  = Char
     48  F Int a    = Bool
     51And thiswill be disallowed:
     54type instance G [x] y where
     55  G [Int] Int = Bool -- OK
     56  G a     b   = ()   -- not OK: outside the type space (G [x] y)
     59The declared type space will be checked for overlap with other instances using the same linearization check that unbranched instances use.
     61== Concrete Proposal ==
     63 * Among unbranched instances, check linearized forms of the instances when doing overlap checking. Thus, our two problematic instances of {{{F}}}, at the top, will conflict.
     65 * After linearizing a left-hand side, the right-hand side of the instance is ill-defined. Thus, the current coincidence check (see [wiki:NewAxioms/CoincidentOverlap here] for more information) is no longer possible and will be removed. (Don't yell yet. Keep reading.)
     67 * Add type space declarations to the {{{type instance where}}} syntax, checking to make sure that branches fit within the declared space.
     69 * Allow coincident overlap within branched instances. This recovers the lost coincident overlap check on unbranched instances. See [wiki:NewAxioms/CoincidentOverlap here] for more information.
     71 * Add new syntax {{{type family Foo a b where { Foo ... = ... ; Foo ... = ... } }}} to declare a type family with one branched instance covering the entire type space. This would be a ''closed'' type family.
     73== Alternative (Non-)Solution ==
     75One way we (Simon, Dimitrios, and Richard) considered proceeding was to prohibit non-linear unbranched instances entirely. Unfortunately, that doesn't work. Consider this:
     78type family H (x :: [k]) :: *
     79type instance H '[] = Bool
     82Innocent 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.