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

Question

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.)

Harlequinade

Answer 1

No. Consider the trivial monad:

data Trivial a = Cow

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

Nehru

...better known as Const (). – Thule

Why would I pass the opportunity to write Cow in a Haskell program? – Nehru

Another trivial one is Cont (), whose only proper inhabitant is cont (\_ -> ()) or however that's spelled. – Bouleversement

What about non-trivial monads? – Bouleversement

@dfeuer: Parametricity plus the need to comply with the monad laws can be used rule out the middle ground, the trivial monad is the only case where this is violated, everything else needs to call the function passed to (>>=) with a valid a -- or it'll fails the first monad law. -- Cont () is the trivial monad up to isomorphism -- The proof of both of these observations is left to you as an exercise. ;) There is a dual argument available in the comonad case, if w a = w b structurally then either w is the uninhabited comonad or a = b. – Bilious

@EdwardKMETT, any monad with just one element (up to bottoms) is trivial, of course. Cont has nasty things like _|_ vs. const _|_. Ah yes, I started thinking about f >=> return and somehow got stuck on that without considering the far more relevant return >=> f. – Bouleversement

Note: Cont Void and Cont () both work but for subtly different reasons. – Bilious

@EdwardKMETT, return produces sensible inhabitants of Cont Void a for any inhabited a, but none of them can be distinguished from each other because none of them can ever be applied to a sensible function. Right? This is just a -> not (not a), while Cont () gets the less exciting a -> True. – Bouleversement

@Bouleversement Depends. Do you consider absurd to be sensible? – Harlequinade

absurd is sensible, even classically. It is simply the logical principle of ex falso quodlibet, or that you can build a function from the empty set, by enumerating where it sends all inhabitants of the set. The existence of undefined :: Void is the degenerate part. – Bilious

@EdwardKMETT: you're using special properties of Haskell here. There are plenty of monads in mathematics whose unit is not injective. – Nehru

Absolutely. That was more or less implied by the question using return and my reply exploiting parametricity. =) – Bilious

Is that a cow-monad? – Verda