With respect to the new RULES mechanism presented by
Simon Peyton Jones (Thu, 22 Apr 1999),
Carsten Schultz <[EMAIL PROTECTED]> writes
> [...]
> > And what about algebraic simplification? Say,
> The same applies to our beloved monads.
> The compiler could be told about the monad laws.
Somebody else (Olaf Chitil?) already remarked that most ``Monads'' aren't.
So to be more consistent,
how about changing the current class Monad into
(motivation see signature ;-):
> class HasMonadOps m where
> return :: a -> m a
> >>= :: m a -> (a -> m b) -> m b
> ...
and introduce:
> class (HasMonadOps m) => Monad m where
> {-# RULES
> "Monad-rightId" forall f. f >>= return = f
> "Monad-leftId" forall f,x. return x >>= f = f x
> ...
> #-}
Even if some still will not like this, would it be within
the scope of the current RULES mechanism?
Would others agree that is is desirable to have
class declarations like this accepted?
One might even imagine extended instance declarations
like the following:
> instance Monad []
> {-# PROOF
> "Monad-rightId"
> forall f. f >>= return
> = concat (map return f)
> = concat (map (:[]) f)
> = case f of
> [] -> concat []
> (x:xs) -> concat ([x]:map (:[]) xs)
> = case f of
> [] -> []
> (x:xs) -> x : concat (map (:[]) xs)
> = f
> "Monad-leftId" ...
> ...
> #-}
In the end, my dreams even include a proof format
that can be checked by the compiler :-)
Best regards,
Wolfram
=====================================================================
# ``Zheng Ming'' --
############## # Getting the names right
# ########
# # #
# # # Ancient Chinese motto,
# # ## ## # fervently supported
# # ## # also by Confucius
# ###### #
# # #
# # #########
# # ## #
# # ## # #
# # ## # #
# # # #
############## #########
# #
