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

[Anthony Clayden]

I'm re-reading the Instance Chains paper.
http://dl.acm.org/citation.cfm?id=1863596
[2010, so before Type Families got off the ground]

And wondering about some of [*] their motivating examples.
[Disclaimer: with a view to writing up something I think is
better.]

Leaving aside the question of backtracking on instance
non-match,
would anybody write a type-level GCD like this?

We have the usual type-level Naturals and Booleans:

> {-# LANGUAGE  MultiParamTypeClasses,
FunctionalDependencies,
>               OverlappingInstances, EmptyDataDecls  #-}
>
> data Z;  data S n
>
> data T;  data F

And then:

> class Gcd m n p | m n → p --p=gcd(m,n)
> instance Gcd m m m           -- OVERLAPPABLE OK
> instance (Lte n m T, Subt m n m', Gcd m' n p)
>       ⇒ Gcd m n p
> instance (Lte n m F, Subt n m n', Gcd m n' p)
>       ⇒ Gcd m n p

Those latter two instances overlap (heads are identical)
in an irresolvable way.
(They're trying to distinguish the `m > n` vs `m < n`
cases.)

The code is closely following how you might write with
Integers, I guess.
But I'm not convinced it's such a good approach for Peanos.

Class Lte compares two Peanos, tells which is the larger.
Class Subt subtracts one from the other.
They're both traversing the (S (S (S ... Z...))) nesting.
(And Subt needs a nasty kludge in case you're trying to
 subtract the larger: it returns Z.)

I think these days (esp with TypeFamilies/Assoc types),
I'd write those latter two instances with a case helper.
And a discriminator type fun `Diff` that provides the
absolute diff,
and tells which param is smaller.
But to keep in the same style, I'll put `Diff` as a class:

> instance (Diff m n d, GcdCase d m n p)
>       => Gcd m n p            -- single 'catch all'
instance
>
> class GcdCase d m n p | d m n -> p
> instance (Gcd d' n p)
>       => GcdCase (T, d') m n p
> instance (Gcd m d' p)
>       => GcdCase (F, d') m n p
>
> class Diff m n d  | m n -> d
> instance Diff Z (S n') (T, S n')
> instance Diff (S m') Z (F, S m')
> instance (Diff m' n' d) => Diff (S m') (S n') d 

Seems to me the code is more succinct,
and easier to follow.
(And by the way doesn't need egregious overlaps.)

[*] Actually, I'm dubious about all of their examples.
More to follow ...

AntC