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