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