
On Thu, Jun 1, 2017 at 3:23 AM, Anthony Clayden
No, my concern is readability.
Well, presumably from the readability perspective, the point is that instance chains allow you to express Euclid's algorithm directly, following the mathematical presentation, whereas the alternative requires indirection through auxiliary truth table classes that are both unnecessary in the mathematical presentation and unhelpful to understanding. (The introduction of the SymmetricDifferenceAndAlsoOrdering class simply seems to hammer this point home.)
I must admit I hadn't though of stand-alone instances as being like rows in truth tables. They're like separate lines of equations, each guarded by a condition.
I sense a Dijkstra-like argument that we should avoid writing "else" or "otherwise", instead requiring the programmer to operate De Morgan's laws by hand. The tedium of this approach is only amplified when applied to instance chains, as we generally hope for programs to have meanings and thus for instance resolution to be coherent. For example, consider the simple chain: class C t u where f :: t -> u instance C Int Int where f = M else C t u where f = N where M and N are some well-typed Haskell expressions. Now, it is simple to define type equality t == u using functional dependencies, and so (following the discussion in section 7 of the 2010 paper, or section 7.1 of my dissertation) in the instance chains framework these could be written as separate instances. We might hope to get away with just one extra instance: instance C Int Int where f = M instance C t u if t == Int fails where f = N instance C t u if u == Int fails where f = N But note that the latter instances will seem incoherent to the compiler, even if the programmer is convinced they are not. So what we really need is instance C Int Int where f = M instance C t Int if t == Int fails where f = N instance C Int u if u == Int fails where f = N instance C t u if t == Int fails, u == Int fails where f = N And indeed, this set of instances is provably coherent (and is accepted by the prototype Habit compiler). But I hardly think we've made things clearer to the programmer---since we have taken one "intuitive" case and split it into three apparently distinct branches---or made things easier for the compiler--- since we now have four axiom clauses for class C instead of two, and 6 coherence checks instead of none. /g -- Prosperum ac felix scelus virtus vocatur -- Seneca