On 3/18/06, Manuel M T Chakravarty
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.
Indeed, this looks all very good and I truly believe this is the direction we should move in. Still, a question: do you propose to go as far as to replace the "traditional" single parameter type-classes with /partial/ type constructors? This is really a naive question -- I don't claim to understand everything this implies. A couple examples to illustrate my thinking: type Show :: + -- where + is representing an (open) subset of the * kind. type Show = s -- 's' binds to the result of the partial type function being defined where show :: s -> String -- alternative, maybe showing better the closing gap between classes and types -- type Show :: + -- where show :: Show -> String type Show = Char where show = ... type Show = [s] where s = Show -- "constraining" the type variable s show = ... -- alternatively -- type Show = [Show] -- where show = ... --------------------------------- -- Revisiting a familiar example type Collect :: + -> + type Collect a = c where insert :: a -> c -> c type Collect elem = Set elem where elem = Ord insert = ... ------------------------ -- Here begins the fun. type Functor :: * -> + type Functor = f where map :: (a -> b) -> f a -> f b Cheers, JP.