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