the MPTC Dilemma (please solve)

[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? 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.