On Sun Jun 4 13:11:47 UTC 2017, J. Garrett Morris wrote:

...

On Sun, Jun 4, 2017 at 1:00 PM, Anthony Clayden wrote: ... You have reiterated a point that is made at length ...

Good, so we're agreed that the 2010 paper is inconsistent to reject `(f :+: f)` but accept `((f :+: f) :+: f)`.

I shouldn't, however, have suggested in 2015 that the deduplicated version is necessarily preferable.

I don't follow. The 2015 version is consistent.

If you omit the deduplication constraints, you simply end up with Leijen-style scoped rows [Leijen, TFP05] ...

Ouch! Its "A novel aspect of this work is that records can contain duplicate labels, " is about the most blood-chilling claim I've seen in the many papers on records systems. It is true, though, compared to what you seem to suggest "effectively introducing a form of scoping over the labels. " If `((f :+: g) :+: (h :+: f))` is to be supported, what's the basis for preferring `f` to the left or right?

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

Is the only point I was wanting to make: using a single class fails to separate concerns, in this example.

...

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,

I think not. They're somewhere between CTFs and Instance Chains. In that guarded instances are not closed. Which also appears to be your claim wrt Instance Chains.

... so of course they're sufficient to implement Swierstra's encoding (following any of ...),

(I was specifically aiming to implement using Haskell as at 2010, but let it pass ...) Yes any of these approaches are "sufficient". That's not in debate.

and will require auxiliary definitions and indirections

Yes, see code I posted subsequent to your message.

that would not be required using instance chains.

Huh? Your 2015 paper uses auxiliaries class `In` Figure 3 in the Instance Chains version. True that the 2010 paper uses no auxiliaries, but it thereby ends up inconsistent. What is "wrong" with using auxiliaries? (Again, in terms of readability.) AntC