Instance Chains selection by class membership [was: [ghc-proposals/cafe] Partially applied type families]
[starting a new thread for this topic]
On Fri Jun 2 17:35:35 UTC 2017, J. Garrett Morris wrote:
On Fri, Jun 2, 2017 at 2:34 PM, Anthony Clayden wrote:
else f :<: g fails if f :<: g
Haskell very strictly doesn't support instance contexts driving selection of instances.
Haskell instance selection ... if you apply the same restriction to instance chains ...
What was confusing me is that there's a fault in the instance definitions for the Swierstra encoding as appears in the 2010 Instance Chains paper. I see in your 2015 paper that's been fixed. But before I go on to discuss, is there a typo in the 2015 paper? Figure 6 line 6 shows a type family equation
IsIn f g = Yep
That's supposed to mirror the Instance Chains solution Figure 3 line 6:
else f `In` g fails
So Figure 6/line 6's `Yep` should be a `Nope`?? Ok what was the fault in the 2010 paper? It correctly failed `instance f :<: (f :+: f)`, because that's ambiguous as to whether the wanted `f` should match left or right of `:+:`. But it didn't fail `instance f :<: ((f :+: f) :+: f)`, because from the failure above, the left operand of the outer `:+:`, viz `(f :+: f)`, is not an instance. So `f :<: ((fail) :+: f)` succeeds. I think this shows that using class instances to both define methods and drive selection logic can fail to separate concerns. You wrote [on the GCD thread]:
Of course, you'll have an easier time of it if you limit yourself to only considering type-level definitions, and not the corresponding method definitions. But doing so rather misses the point of instance chains.
It seems to me that in the 2010 paper, the fault arises from considering only the method definitions and failing to pay attention to the type-level. And yes, I want to make an easy time as possible for the programmer -- both writing and especially reading code. The second approach in the 2015 paper using a case-preparing Type Family seems to me to cleanly impose a phase distinction first type-level calculation then class instance selection/method overloading. So my end-game is to be able to remove FunDeps from the language, in favour of class and instance contexts giving Type Families with Equality constraints. (By all means, let's encourage those Type Families to be Associated within classes, per your Partiality paper with Richard.) To achieve that we need better support for overlaps. We need to do that in an understandable way for the programmer. That is, the 'umble programmer like me, not needing an advanced PhD in abstruse type theory. I think Instance Guards help readability by putting the instance selection criteria all in the one place at the instance head; not reliant on the reader scanning through a prior chain of instances/elses.
... there is no reason to imagine that using either instance chains or closed type families would be any obstacle to implementing them. [viz extensible variants/co-products]
No I'm not suggesting any lack of capability. If anything, Instance Chains are _too_ powerful. I'm working on showing how the Swierstra encoding could be catered for in Haskell 2010 + MPTCs+TypeEq. That is, was achievable in GHC 2004. (I could do with a few extra milli-Olegs of brain power.) It's a debate about whether/why/how we introduce syntactic sugar into current capability vs introducing a heretofore avoided feature into type inference viz: type class membership driving instance selection, as opposed to currently: types driving instance selection. AntC
On Sun, Jun 4, 2017 at 1:00 PM, Anthony Clayden
Ok what was the fault in the 2010 paper?
You have reiterated a point that is made at length in §3.2 of my 2015 paper, and §3.4.2 of my dissertation. I shouldn't, however, have suggested in 2015 that the deduplicated version is necessarily preferable. If you omit the deduplication constraints, you simply end up with Leijen-style scoped rows [Leijen, TFP05] instead of Rémy-Wand style rows. Of course, if, as we did in 2010, you use classes instead of branching to implement elimination on variants, you have no way to tell the difference between the two models of variants, and so there's no reason to prefer one or the other.
I'm working on showing how the Swierstra encoding could be catered for in Haskell 2010 + MPTCs+TypeEq.
You keep talking about guarding instances or equations. Guards are equivalent to closed type families, so of course they're sufficient to implement Swierstra's encoding (following any of Bahr or Oliveira et al. or my approaches), and will require auxiliary definitions and indirections that would not be required using instance chains. This conversation having precisely reattained its starting point, I don't imagine I could contribute further. /g -- Prosperum ac felix scelus virtus vocatur -- Seneca
participants (2)
-
Anthony Clayden -
J. Garrett Morris