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

score 64 · Accepted Answer · edited Jan 25 '16 at 23:40

64

No. Consider the trivial monad:

data Trivial a = Cow

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

edited Jan 25 '16 at 23:40

recursion.ninja

5,377
7
46
78

answered Jan 25 '16 at 23:34

Andrej Bauer

2,458
17
26

19

...better known as `Const ()`. – leftaroundabout Jan 25 '16 at 23:47
53

Why would I pass the opportunity to write `Cow` in a Haskell program? – Andrej Bauer Jan 25 '16 at 23:56
1

Another trivial one is `Cont ()`, whose only proper inhabitant is `cont (\_ -> ())` or however that's spelled. – dfeuer Jan 26 '16 at 02:00
7

What about non-trivial monads? – dfeuer Jan 26 '16 at 02:10
14

@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`. – Edward Kmett Jan 26 '16 at 03:39
@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`. – dfeuer Jan 26 '16 at 03:46
2

Note: `Cont Void` and `Cont ()` both work but for subtly different reasons. – Edward Kmett Jan 26 '16 at 04:04
@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`. – dfeuer Jan 26 '16 at 05:22
@dfeuer Depends. Do you consider `absurd` to be sensible? – PyRulez Jan 26 '16 at 14:28
1

`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. – Edward Kmett Jan 26 '16 at 16:37
@EdwardKMETT: you're using special properties of Haskell here. There are plenty of monads in mathematics whose unit is not injective. – Andrej Bauer Jan 26 '16 at 17:28
Absolutely. That was more or less implied by the question using `return` and my reply exploiting parametricity. =) – Edward Kmett Jan 26 '16 at 17:57
1

Is that a cow-monad? – coredump Jan 31 '16 at 10:40

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

1 Answers1