fundeps for extended Monad definition

Hal Daume III hdaume@ISI.EDU
Fri, 28 Feb 2003 08:39:27 -0800 (PST)


> The reason, which is thoroughly explained in Simon Peyton-Jones'
> message, is that the given type signature is wrong: it should read
> 	f1 :: (exists b. (C Int b) => Int -> b)

Right.  Simon pointed out that this is a pretty useless function, but not
entirely so, since the result of it is not of type 'forall b. b', but
rather of 'forall b. C Int b => b'.  Thus, if the C class has a function
which takes a 'b' as an argument, then this value does have use.

> Hal Daume's original example works as well:
> 
> > newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) => mb)
>        
> 
> > class Monad2 m a ma | m a -> ma, ma -> m a where
> >   return2 :: a -> ma
> >   bind2   :: ma -> (a -> (MM2 m a)) -> (MM2 m a)
> >   unused :: m a -> ()
> >   unused  = \_  -> ()

This wasn't quite my original example.  The type of bind2 needs to be:

>   bind2   :: ma -> (a -> (MM2 m b)) -> (MM2 m b)

Which does typecheck.  However, you cannot seem to write instances of it:

instance Monad2 [] a [a] where
  return2 x = [x]
  bind2 l f = MM2 (concatMap (unmm2 . f) l)
    where unmm2 (MM2 mb) = mb

yields our friend "cannot unify mb with [b]", both in hugs and ghc.