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

[Anthony Clayden]

> On Thu Jun 1 09:51:25 UTC 2017, J. Garrett Morris wrote:

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

What I see in the mathematical presentation,
is that each equation is stand-alone, with a guard.
I guess we'll just agree to differ on the readability of the
Haskell.
(What if Euclid had taken up lazy functional programming
..?)

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

If I'm in the company of Dijkstra and Euclid,
that's good enough for me.

> ... we generally hope for programs to have meanings

Yes we do.

> and thus for instance resolution to be coherent.  

I agree the current (under-/non-)specified rules for overlap
don't help us reason much about coherence.
(But see my post on the cafe last month
 wrt "Well-behaved instances".)

> 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

This is an example where overlap is well-behaved.
(Assuming those are the only instances.)

> Now, it is simple to define type equality t == u

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.

> using functional dependencies, and so (...)
> in the instance chains framework these could be written
> as separate instances. 

This is a case of well-behaved overlap,
so they'd work as separate instances anyway.

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

That first most specific instance exhibits 3 type
equalities:

(t ~ Int. u ~ Int, t ~ u)

So there's various ways to slice up the space.

I think Instance Guards both have less lexical clutter,
and help the compiler see what's coherent:

>    instance  C Int Int                    where f = M
>    instance  C t t     | t /~ Int        where f = N
>    instance  C t u     | t /~ u         where f = N

> [4-instance example elided]

> ... we have taken one "intuitive" case and split it into
> three apparently distinct branches ...

I guess what's intuitive will depend on the application.
It's difficult to make much claim in the abstract.

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

The compiler author will love having precise rules
for when instances are apart.
And being able to check that when compiling the instance
(not delay it to the usage site).
And needing to validate only each pair of instances;
not worry about overlaps of overlaps.

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.


AntC