the MPTC Dilemma (please solve)

Manuel M T Chakravarty chak at
Sun Mar 19 11:39:55 EST 2006

Jean-Philippe Bernardy:
> On 3/18/06, Manuel M T Chakravarty <chak at> 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

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:


[*] 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.

More information about the Haskell-prime mailing list