Search code examples
haskellmonadssemanticsequalityequational-reasoning

If return a = return b then does a=b?


Can you prove that if return a = return b then a=b? When I use =, I mean in the laws and proofs sense, not the Eq class sense.

Every monad that I know seems to satisfy this, and I can't think of a valid monad that wouldn't (Const a is a functor and applicative, but not a monad.)


Solution

  • No. Consider the trivial monad:

    data Trivial a = Cow
    
    instance Monad Trivial where
      _ >>= _ = Cow
      return _ = Cow