[Haskell-cafe] Type-level GCD [Instance Chains]

[J. Garrett Morris]

On Thu, Jun 1, 2017 at 3:23 AM, Anthony Clayden
<anthony_clayden at clear.net.nz> wrote:
> 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