Re: the MPTC Dilemma (please solve)

Jean-Philippe Bernardy:

On 3/18/06, Manuel M T Chakravarty wrote:

...

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?

No. Type classes are fine as they are. However, if you want to associate types with classes, where the definition of these types varies on an instance by instance basis, I argue that associated types (ie, type definitions in classes) are more appropriate than MPTCs with FDs[*]: http://hackage.haskell.org/trac/haskell-prime/wiki/AssociatedTypes Associated types are *open* definitions of type functions (ie, you can always extend them by adding more instances). In some situations *closed* definitions of type functions are preferable (as in the Peano arithmetic example above, which can for example be nicely combined with GADTs to define bounded lists). AFAIK nobody has a worked out a proposal for how to add closed type functions to Haskell, but Tim Sheard has argued for their usefulness in his language Omega: http://www.cs.pdx.edu/~sheard/papers/LangOfTheFuture.ps Manuel [*] I am unsure whether we want MPTCs if we have associated types. It seems that the typical uses of MPTCs become single parameter classes when associated types are used instead of FDs.