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 [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.) |
| 31 | |
| 32 | == Branched instances == |
| 33 | |
| 34 | But, 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. |
| 35 | |
| 36 | Here are some examples, leaving off the {{{type family}}} headers: |
| 37 | |
| 38 | {{{ |
| 39 | type instance Equals x y where |
| 40 | Equals x x = True |
| 41 | Equals x y = False |
| 42 | }}} |
| 43 | |
| 44 | {{{ |
| 45 | type instance F Int x where |
| 46 | F Int Bool = Double |
| 47 | F Int Int = Char |
| 48 | F Int a = Bool |
| 49 | }}} |
| 50 | |
| 51 | And thiswill be disallowed: |
| 52 | |
| 53 | {{{ |
| 54 | type instance G [x] y where |
| 55 | G [Int] Int = Bool -- OK |
| 56 | G a b = () -- not OK: outside the type space (G [x] y) |
| 57 | }}} |
| 58 | |
| 59 | The declared type space will be checked for overlap with other instances using the same linearization check that unbranched instances use. |
| 60 | |
| 61 | == Concrete Proposal == |
| 62 | |
| 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. |
| 64 | |
| 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.) |
| 66 | |
| 67 | * Add type space declarations to the {{{type instance where}}} syntax, checking to make sure that branches fit within the declared space. |
| 68 | |
| 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. |
| 70 | |
| 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. |
| 72 | |
| 73 | == Alternative (Non-)Solution == |
| 74 | |
| 75 | One way we (Simon, Dimitrios, and Richard) considered proceeding was to prohibit non-linear unbranched instances entirely. Unfortunately, that doesn't work. Consider this: |
| 76 | |
| 77 | {{{ |
| 78 | type family H (x :: [k]) :: * |
| 79 | type instance H '[] = Bool |
| 80 | }}} |
| 81 | |
| 82 | 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. |