[Haskell-cafe] Type-level GCD [Instance Chains]
anthony_clayden at clear.net.nz
Thu Jun 1 02:23:54 UTC 2017
> 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
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.
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
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'
> -- 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.)
More information about the Haskell-Cafe