the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

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