search

tomjaguarpaw / tilapia

Improving all Haskell's programmer interfaces
65 stars 2 forks source link

Improve MonadFail docs - isn't 'fail s' always a left zero? #120

Open tomjaguarpaw opened 2 years ago

tomjaguarpaw commented 2 years ago

The MonadFail docs say that fail s must be a "left zero", i.e.

fail s >>= f  =  fail s

But given that fail s :: forall a. m a is there any way that it couldn't be a left zero?

kindaro commented 2 years ago

How do you even begin to prove this?

  1. fail s cannot contain any values of an arbitrary type a.
  2. Therefore, f can never be invoked by >>=.
  3. Since f cannot be invoked, >>= must behave the same way for any f.
  4. Take f be pure — by a law of monad >>= pure ≡ id. Therefore, by №3 >>= f ≡ id for any f.
  5. id (fail s) ≡ fail s. ∎

— Maybe like this.

But this all on the assumption that everything is defined. Is this an admissible assumption? Otherwise, we can consider situations where >>= invokes f with undefined — then f can either crash (≢ fail s) or return an arbitrary value (≢ fail s).

tomjaguarpaw commented 2 years ago

Apparently you can prove it by parametricity. See https://www.reddit.com/r/haskell/comments/u5k4gv/is_it_possible_for_fail_s_not_to_be_a_left_zero/.