On Fri Jun 2 10:26:16 UTC 2017, J. Garrett Morris wrote:

This conversation has become deeply mysterious to me.

Hi Garrett, thank you for the opportunity to debate the ideas in Instance Chains, and correct any misunderstandings I might have gained. The interaction of Overlapping Instances with other Haskell features has been vexing for a long time. There have been many approaches. I find this continuing situation particularly frustrating, because it seems to me there was an answer in 2002 [1], whose effectiveness was confirmed by the HList work 2004 [2]. I've been banging this drum for a long time [4].

I understand that you're revisiting arguments on the structuring of conditionals ...

No. Until your comment yesterday re Dijkstra (thank you for the tip), I was continuing ideas in the Sulzmann and Stuckey Constraint Handling Rules approach [1]. Although your papers/Dissertation cite some of S&S's work, you seem unaware of type disequality guards. I think that's a significant oversight.

... that were tried and discarded in the 70s;

I can see why Dijkstra's ideas might be discarded for term-level calculation: * the impossibility of determining whether guards are mutually exclusive (that's a specie of the halting problem) * the deliberate non-determinacy But that first objection is not applicable for instances/guards, because they have a very simple semantic structure: pattern-match on the instance head, then type (dis-)unifiability test. The second is a definite plus-feature for instance selection. (Reflecting how GHC works today.) So I'm fully up with the programme of the great programmer.

what I don't understand is why you need to repeatedly mischaracterize my work to do so.

If I'm mischaracterising, I apologise. I note, though, you haven't demurred at my observation that instance chains need backtracking. I find backtracking far more unacceptable than indeterminacy.

For one example, I have no idea why you make the following claim:

...

Nevertheless, I can only write one Instance Chain per class. So I can't (say in another module) introduce a new datatype with instances.

The instance chains paper is quite explicit in ruling out this interpretation; when introducing the notion of chains, we wrote:

In ilab, a class can be populated by multiple, non-overlapping instance chains, where each chain may contain multiple clauses (separated by the keyword else).

For another, you give a fanciful description of the

Then I apologise. The two chief examples in that paper (gcd and the Swierstra encoding) both show a final `else ... fails` branch with a catch-all instance head. Section 3.2 comments "..., closing the Gcd class." For the Swierstra encoding in particular, the algorithm requires the class to be total (it must be closed), so that the recursive descent test/validation for go-left/go-right can be determinate. problems that

might arise in implementing instance chains, including:

I reject "fanciful". So I'm going to give citations.

...

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."

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.

Luckily, both instance chains and closed type families have formalizations that can be checked to evaluate these claims.

Yes, Overlapping Instances has suffered for too long from under-/non-formalised semantics. What I'll be doing for Instance Guards is giving a translation into Haskell2010 + MPTCs __without__ overlaps. (I will need to assume, though, a type-level type equality test/total function. You've already commented that's easliy produced.) A serious weakness of Instance Chains, it seems to me, is it can't be translated to existing Haskell.

In neither case do we find either equality limited to ground types or anything that should be construed as 'look ahead'.

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. "Look ahead" is exactly what Richard is describing in the bulk of that blog post. That is, looking down the sequence of instance equations, to see if any would match and be confluent. This significantly helps progress in inference. If Instance Chains aren't going to be doing that, that's another weakness.

Perhaps you're trying to refer to the use of infinitary unification in checking apartness (but not in checking equality) for closed type families?

No, infinitary unification is a whole 'nother bag of spanners. I am still goggling at your joint paper with Richard.

Here again, not only is there no use of or need for infinitary unification with instance chains, ...

Good!

but I discussed this difference and its consequences in my 2015 paper.

OK. I've not yet got through that paper. What I do see in the 2010 paper (perhaps this has changed subsequently) is using typeclass membership to determine whether a type is a member of the __same__ class. This seems to be essential to the Swierstra encoding such as:

else f :<: (g :+: h) if f :<: g else f :<: (g :+: h) if f :<: h

Gloss: "f is related to (g :+: h), if f is related to g". And likewise for f related to h. So: * this needs look inside the ( :+: ) to see if f is related to g or to h, or to both (fail) or to neither (fail). And now you tell me there might be other instance chains for `:<:`, so the compiler has to work through them. * it breaks down the 'phase distinctions' in instance selection. I feel very queazy about a recursion like that at the class level. We can express Russell's paradox:

else f :<: g fails if f :<: g

Haskell very strictly doesn't support instance contexts driving selection of instances. That is confusing for newbies, but it's for very good decidability reasons.

Finally, you make various claims about what is and is not a solution to the expression problem which have no apparent relationship to any of the existing work on the expression problem or its encodings. ... Again, this is all laid out, with examples, in my 2015 paper.

I was being brief. (And this post has gone on plenty long enough, too.) I'll come back and debate that point when I've worked through your 2015 paper. What's strongly motivating me with Haskell is getting the type system to cater for extensible/anonymous records. (I'm a Relational Theorist by trade.) Closed instances (be they Chains or Type Families, or the proposed Closed Classes) are just not going to hack it. Adam G for the Overloaded Records Fields work has eschewed Type Families in favour of FunDeps. That's because it needs to create instances 'on the fly'. Now he hasn't needed overlaps yet (ORF is at an early stage), but anonymous/extensible records will. Just like HList. AntC [1] Sulzmann & Stuckey 2002 "A Theory of Overloading", esp section 8.2 "Overlapping Definitions" [2] Kiselyov et al 2004 "Strongly Typed Heterogeneous Collections" [3] https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-fa... [4] https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/DiscussionPage