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

[Anthony Clayden]

> On Wed May 31 14:19:55 UTC 2017, J. Garrett Morris wrote:

> [Apologies for breaking threading...]

Thanks Garrett, my email client does horribler things to
threading.

Since the O.P. was about the aesthetics/readibility of code,
I'm surprised you elided all the code.
(I suppose de gustibus non disputandum.)

>> On Wed May 31, Anthony Clayden wrote:
>> Leaving aside the question of backtracking
>> on instance non-match,
>> would anybody write a type-level GCD like this?

>Your question seems to be "would you use
> the standard recursive statement of
> Euclid's algorithm to demonstrate Euclid's algorithm?"
> This certainly seemed to be a reasonable idea in 2010.

I think the code I posted was using Euclid's algorithm.
I agree it's difficult to cast one's mind back to what was 
reasonable Haskell in 2010, but I didn't use Type Families.

 > If your concern is efficiency, ..

No, my concern is readability.

>> (And Subt needs a nasty kludge in case you're trying to
>>  subtract the larger: it returns Z.)

> What you call a nasty kludge, I call a standard operation
> on commutative monoids. 
[https://en.wikipedia.org/wiki/Monus]

Well, OK sometimes the kludge is justified ;-).
Not for GCD, methinks.
Because the equation guards specifically avoid the need.


>> I think these days (esp with TypeFamilies/Assoc types),

> You seem to be discovering that closed instance chains
> can be implemented by writing out truth tables.

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.
(In math, typically the condition is trailing with comma
sep.)
OK I'll mirror that style below.

>  I discussed this transformation at length,
> and suggested that doing might make your code
> harder to write and to read, ...

Ok, let's see. Here's the math (adapted from wikipedia):

  gcd(m, n) = m           , if m == n
  gcd(m, n) = gcd(m - n, n)  , if m > n
  gcd(m, n) = gcd(m, n - m)  , if m < n

Here's some Haskell (this works in Hugs,
just to make sure I'm getting the right vintage)

> data Z;  data S n
>
> data LT;  data EQ;  data GT
> data If t
>
> class Gcd m n p | m n -> p where
>     -- methods for Gcd go here
>
> instance (GcdCase m n p (If d), Diff m n d)
>       => Gcd m n p  where    -- single 'catch all'
instance
>     -- method definitions
>
> -- GcdCase instances mirror the Euclid equations
>
> class GcdCase m n p d | m n d -> p
> instance (HTypeCast m p)
>       => GcdCase m n p (If (EQ, d'))
> instance (Gcd d' n p)
>       => GcdCase m n p (If (GT, d'))
> instance (Gcd m d' p)
>       => GcdCase m n p (If (LT, d'))
>
> class Diff m n d  | m n -> d
> instance Diff Z Z (EQ, Z)
> instance Diff (S m') Z (GT, S m')
> instance Diff Z (S n') (LT, S n')
> instance (Diff m' n' d) => Diff (S m') (S n') d 
>
> -- HTypeCast omitted, use standard HList


> ... in my Haskell 2015 paper "Variations on Variants".

OK, will study. I see that's focussing on Wadler's
"expression problem", as does the Instance Chains paper.
It's the Swiestra example there I want to get on to.

> Of course, you'll have an easier time of it
> if you limit yourself to only considering
> type-level definitions, and not
> the corresponding method definitions. 
> But doing so rather misses the point
> of instance chains.

I've used classes throughout the above.
So could easily add methods.
The idiom (following HList 2004)
is some classes are type-level only.
So I see no harm making those Type Families
in 2017. (Whether they should be Closed TFs
vs stand-alone instances is a separate debate.)


AntC