You Could Have Invented Monads! (And Maybe You Already Have.)

Show that f' * unit = unit * f' = bind f'

——————————

f :: a -> b
f' :: a -> m a
unit :: a -> m a

lift f = unit . f
f' = lift f

The lift function in this tutorial is not the same as the liftM in Haskell. So you should use lift (but not liftM) with bind.

— Me@2015-10-13 11:59:53 AM

(f' * g') xs
= ((bind f') . (bind g')) xs

bind f' xs = concat (map f' xs)
unit x = [x]

bind unit xs
= concat (map unit xs)
= concat (map unit [x1, x2, ...])
= concat [unit x1, unit x2, ...]
= concat [[x1], [x2], ...]
= [x1, x2, ...]
= xs

(f' * unit) (x:xs)
= bind f' (bind unit (x:xs))
= bind f' (concat (map unit (x:xs)))
= bind f' (concat (map unit [x1, x2, ...]))
= bind f' (concat [[x1], [x2], ...])
= bind f' [x1, x2, ...]
= concat (map f' [x1, x2, ...])
= concat [f' x1, f' x2, ...]
= concat [(unit . f) x1, (unit . f) x2, ...]
= concat [(unit (f x1)), (unit (f x2)), ...]
= concat [[f x1], [f x2], ...]
= [f x1, f x2, ...]

(unit * f') (x:xs)
= ((bind unit) . (bind f')) (x:xs)
= bind unit (bind f' (x:xs))
= bind unit (concat (map f' (x:xs)))
= bind unit (concat (map f' [x1, x2, ...]))
= bind unit (concat [f' x1, f' x2, ...])
= bind unit (concat [(unit . f)  x1, (unit . f) x2, ...])
= bind unit (concat [(unit (f x1)), (unit (f x2)), ...])
= bind unit (concat [[f x1], [f x2], ...])
= bind unit [f x1, f x2, ...]
= concat (map unit [f x1, f x2, ...])
= concat [[f x1], [f x2], ...]
= [f x1, f x2, ...]

— Me@2015-10-15 07:19:18 AM

If we use the identity bind unit xs = xs, the proof will be much shorter.

(f' * unit) (x:xs)
= ((bind f') . (bind unit)) (x:xs)
= bind f' (bind unit (x:xs))
= bind f' (x:xs)

(unit * f') (x:xs)
= ((bind unit) . (bind f')) (x:xs)
= bind unit (bind f' (x:xs))
= bind f' (x:xs)

— Me@2015-10-15 11:45:44 AM

2015.10.15 Thursday (c) All rights reserved by ACHK