Subject: Re: the MPTC Dilemma (please solve) Newsgroups: gmane.comp.lang.haskell.prime Date: Saturday 18th March 2006 20:15:11 UTC (over 11 years ago) Claus Reinke: > > I'm forwarding an email that Martin Sulzmann asked me to post on his > > behalf. > > thanks. well, that is one view of things. but it is certainly not the only one. > > first, about those "acrobatics": my type-class-level programs tend to > start out as straightforward logic programs over types - no acrobatics > involved, easy to understand. the acrobatics start when I'm trying to > fit those straightforward programs into the straightjackets imposed > by current systems - be they explicit restrictions or accidental > limitations. wrestling them leads to the need to introduce complex > work-arounds and implementation-specific tricks into the formerly > clean logic programs. The big question is: do we really want to do logic programming over types? I'd say, no! We are not doing logic programming over values either, are we? I have done my share of Prolog programming and what I repeatedly found is that I write functional programs using a horrible syntax (because you can't nest expressions) and with lots of cuts to prevent backtracking to kick in. If we want to express computations over types, we'll see the same advantages when using a functional style as we do see on values. Let's look at an example. Here addition and multiplication on Peano numerals using MPTCs and FDs: data Z data S a class Add a b c | a b -> c instance Add Z b b instance Add a b c => Add (S a) b (S c) class Mul a b c | a b -> c instance Mul Z b Z instance (Mul a b c, Add c b d) => Mul (S a) b d It's a mess, isn't it. Besides, this is really untyped programming. You can add instances with arguments of types other than Z and S without the compiler complaining. So, we are not simply using type classes for logic programming, we use them for untyped logic programming. Not very Haskell-ish if you ask me. I'd rather write the following: kind Nat = Z | S Nat type Add Z (b :: Nat) = b Add (S a) (b :: Nat) = S (Add a b) type Mul Z (b :: Nat) = Z Mul (S a) (b :: Nat) = Add (Mul a b) b Well, actually, I'd like infix type constructors and some other syntactic improvements, but you get the idea. It's functional and typesafe. Much nicer. Manuel |
|||