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