On Mon May 15 16:20:09 UTC 2017, Richard Eisenberg wrote:
Lots to respond to!
Thanks Richard, phew! yes. Let's break it down a bit.
I do think think there's one overarching question/theme here: Do we want functional dependencies or type-level functions? Behind AntC's arguments, I see a thrust toward functional dependencies. (Not necessarily their *syntax*, but the idea of type improvement and flexible -- that is, multidirectional -- type-level reasoning.) My dependent types work pushes me toward type-level functions.
Yes there is an overarching question. I don't think it's specifically FunDeps vs Type Functions. (Although I disagree the **Functional** Dependencies are somehow not "functional". Yes Mark Jones got the idea from Relational database theory. Where did Ted Codd get the idea from? Mathematical (binary) "relations", which are a set-theoretic account of, um, functions.) "Multidirectional type-level reasoning" is what all functional languages do: from Robinson's unification to Hindley-Milner to OutsideIn(X) to System F-subscript-superscript. There's been an example in Haskell's Prelude since ~1991: the `read` method's return type is 'demand-pulled' from context, not 'supply-pushed' from its parameter. Similarly if I write:
x :: Int x = a + (b * c)
We infer a, b, c must all be Int. Perhaps in another universe, Haskell had explicit type application from day 1, and insisted on giving type signatures for all vars (like nearly all procedural/OO languages). But we aren't in that universe, and I love Haskell/FP for being both type-safe and not pernickety in that way.
... [big snip - I'll reply separately]
I expect AntC would prefer disequality guards over closed classes.
Oh yes! I was about to say (repeating my earlier message): if we're going to ground type family instances in classes, then we need a way to distribute type instances as associated types, unless ... you're going to suggest something daft like closed classes. And then you did.
I would be interested to hear more from the community on this choice -- they're really the same as ordered equations under the hood, and it's just a choice of syntax. Maybe we can even have both.
Yes please all chip in. There were strong views expressed 5~8 years ago. My two-penn'orth: I think we can mechanically translate closed equations to guards (equality and 'apart' tests). The example in my earlier post tried to show how. For class instances (with overlaps), I think there's also a mechanical translation, but only for 'well-behaved' sets of instances. (For Incoherent sets we don't have a chance.) And of course as soon as some imported instance overlaps, we have to start again to assess well-behavedness.
Now, on to individual points:
...the Hard Thought in order to be backward compatible. (This backward compatibility necessity is one of the reasons I love working with Haskell. When adding a feature to the language, we just can't take easy ways out!)
The backwards-compatibility I particularly want to preserve is "distributed instances". That is, putting the instance code close to type decls and other functions that build or consume that type. I also want to put explicitly *in the instance decl* the restraints on what types that instance applies for. Not implicit from where it appears in a closed but lengthy/voluminous sequence of equations. Yes there must be global coherence for the class/type instances. That's a mechanical check which compilers are good at, but humans not so much.
... it was awkward to describe the overlap between two branched instances. AntC might argue that, if we just had disequality guards, it would all be much simpler. He might be right.
I'd argue it's simpler to understand each instance on its own grounds. Although a bunch of guards can get quite complex. (There was Andy A-M's example back in 2013.) The cumulative effect of the preceeding equations in the closed family is more complex. IMO.
In retrospect, it would have been nice to have the proposals process active when designing closed type families; we might have come up with a better design.
There was a huge and rather repetitive (unfortunately) discussion in several rounds 2009~2012, somewhat prompted by trying to 'fix' the Haskell 2010 standard. So that we could include MPTCs in the standard. But you can't have MPTCs without FunDeps or Type Families, or without agreeing a position on overlaps. (good luck with that!) So although MPTCs were in both GHC and Hugs before 1998, they're still not 'official' >sigh<. MPTC's omission for Haskell2010 is what I meant by:
we've lost 7~8 years of opportunity.
My recollection at the time [of developing closed Families] is that other approaches were more functional-dependency-like in character. (To wit: instance chains.)
I wish Martin Sulzmann could have been more active at the time. (He occasionally expresses the intention of getting back into Haskell.) Instance guards are really a continuation of the CHR approach. So fit nicely into whole-of-program inference with type improvement. [I dislike the non-distributivity of instance chains for the same reason I dislike closed families. Although instance chains do have some nice features. Instance guards give me that feature more directly. Whereas closed type families don't give that feature at all.]
When I did the closed type family work, I was thinking that type families were better than functional dependencies; now, my view is much more nuanced (leaning strongly toward fundeps instead of partial type families).
I'm a little unsure what you mean at the top of the post about the "idea" of FunDeps vs their specific syntax. I can simulate FunDeps with superclass constraints using Type Funs and Equality constraints. This even achieves multi-directional improvement. Is that what you want to include? It took me a long time to realise this works out better than the FunDeps arrow business, especially with overlaps. The dreaded "Instances inconsistent with FunDeps" error is a devil to fiddle with. And often ends up breaking the coverage condition. [As Iavor frequently points out.] Martin pointed out that breaking coverage (using UndecidableInstances) is not as 'safe' as SPJ had been assuming.
I don't see what's so hard [about non-unifiability].
It's not nearly as hard from a fundep point of view. ...
... [another big snip: thanks for the pointer to the
paper.]
I do have to say all this talk has made me think more about apartness constraints in FC, at least. They might be a touch simpler than the current story.
I think apartness is the criterion that's always applied to resolve instance selection under overlaps. The trouble is that the semantics for overlap has never been spelled out. (Nor, I suspect the criterion for a 'well-behaved' set of instances. I can volunteer that for you.) Apartness does not intrude inside constraints in the class/instance contexts, nor inside the body of a class instance/methods. It might help with instance selection wrt the rhs of type instance equations. AntC