On 3/18/06, Manuel M T Chakravarty <[EMAIL PROTECTED]> 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.
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
