the MPTC Dilemma (please solve)

Manuel M T Chakravarty chak at cse.unsw.edu.au
Sat Mar 18 15:15:11 EST 2006


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




More information about the Haskell-prime mailing list