On Fri Jun 2 13:48:43 UTC 2017, Richard Eisenberg wrote:
I'm going to respond just to the few points that concern me directly.
Thanks Richard, blige! there's a lot to catch up with.
On Jun 2, 2017, at 9:34 AM, Anthony Clayden wrote:
There's a persistent problem for the compiler testing for type equality: the usage sites must have the types grounded. It's often more successful to prove disequality.
That's straight out of the HList paper [2], Section 9 "By chance or by design?". "We should point out however groundness issues. If TypeEq is to return HTrue, the types must be ground; TypeEq can return HFalse even for unground types, provided they are instantiated enough to determine that they are not equal."
While this may be true for HList's TypeEq, it is not true for closed type families. If we have
type family Equals a b where Equals a a = True Equals a b = False
HList's TypeEq is comparable from 2004!, using typeclasses/FunDeps/Overlaps:
class TypeEq a b p | a b -> p where instance TypeEq a a HTrue instance (p ~ HFalse) => TypeEq a b p
The False instance needs bare typevar `p` so that it overlaps; consequently needs UndecidableInstances. (I've used (~), but that was a typecast class in 2004.)
then (Equals [a] [a]) will reduce to True, even if `a` is universally bound. Indeed, even (Equals a a) will reduce to True. So there is no groundness issue any more.
Great stuff! And that TypeEq behaves likewise now. I was trying to cast the discussion back to ~2010, the Instance Chains work. IIRC groundedness was still a difficulty then.
and also:
I suspect that for the compiler, Instance Chains will be as problematic for type inference as with Closed Type Families: CTFs have a lot of searching under the covers to 'look ahead' for equations that can safely match.
That's from Richard, particularly this comment [3]. The whole blog post is relevant here, I think.
I'm not sure where you're getting "look ahead" from. Closed type families -- and that post, as far as I can tell -- don't discuss looking ahead. Instead, closed type families are all about looking *behind*,
Well, I think we're saying the same thing. Your last comment on that blog post links to the NewAxioms write-up. That has this example:
type family And (a :: Bool) (b :: Bool) where And False a = False And True b = b And c False = False And d True = d And e e = e
"All of these equations are compatible, meaning that GHC does not have to do the apartness check against the target." Faced with simplifying `And c False`, does GHC get stuck at the first or second equation, because it can't resolve `c` to `False` or `True`? No, it "looks ahead" to the third equation. Because it sees that if `And c False` unifies with either of the first two, it'll yield the same result `False`. Your comment on the blog post is "coincident overlap within closed type families (the new nomenclature for branched instances) would indeed be useful." I think it would be useful, too, for Instance Chains or Closed Classes. But there's a problem: Class instances must select method implementations, as well type improvement. So we need to fix on a specific instance, even though we only have `And c False`.
I think the situation has changed with the introduction of Type Families. They weren't applicable in 2010. So not relevant to the Instance Chains paper.
My mistake: I meant to say "... introduction of Closed Type Families".
Type families were introduced in 2005, I believe. At least, that's when the papers were written.
Hmm, careful. 2005 was Assoc types only. The usually cited paper for Type Families is Schrivers et al 2008. Garrett's papers cite that, not the 2005, and I agree that's the full write-up. But the 2008 paper was written in parallel with development. The feature appeared in GHC after the paper. And it wasn't complete: we waited a long time to get Type Families/(~) in superclass constraints. (There were a couple of release which supported the syntax superclass, but it did nothing.)
I don't know what version of GHC first included them, but I think it was before 2010.
Vintage ~2010 there was limited support for overlap in TF instances -- the equations had to be "confluent". (This is the (||) example near the top of your blog post, where you conclude "and we can just write || using separate instances, anyway." Yes you could just write separate instances in ~2010.) I don't see that Instance Chains has a comparable notion of "confluent" or "compatible". But perhaps I missed it.
"Look ahead" is exactly what Richard is describing in the bulk of that blog post.
I disagree here: ...
See above AntC