Re: [Haskell-cafe] Type-level GCD [Instance Chains]
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
On Thu, Jun 1, 2017 at 3:23 AM, Anthony Clayden
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, whereas the alternative requires indirection through auxiliary truth table classes that are both unnecessary in the mathematical presentation and unhelpful to understanding. (The introduction of the SymmetricDifferenceAndAlsoOrdering class simply seems to hammer this point home.)
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", instead requiring the programmer to operate De Morgan's laws by hand. The tedium of this approach is only amplified when applied to instance chains, as we generally hope for programs to have meanings and thus for instance resolution to be coherent. 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 where M and N are some well-typed Haskell expressions. Now, it is simple to define type equality t == u using functional dependencies, and so (following the discussion in section 7 of the 2010 paper, or section 7.1 of my dissertation) in the instance chains framework these could be written as separate instances. 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, even if the programmer is convinced they are not. So what we really need is instance C Int Int where f = M instance C t Int if t == Int fails where f = N instance C Int u if u == Int fails where f = N instance C t u if t == Int fails, u == Int fails where f = N And indeed, this set of instances is provably coherent (and is accepted by the prototype Habit compiler). But I hardly think we've made things clearer to the programmer---since we have taken one "intuitive" case and split it into three apparently distinct branches---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. /g -- Prosperum ac felix scelus virtus vocatur -- Seneca
participants (2)
-
Anthony Clayden -
J. Garrett Morris