🚀 go-pugleaf

In his article jones-mark@cs.yale.edu (Mark Jones) writes something like :

>Now we're ready for the generalization.  The type constructor
>State b is a monad M so that we could actually define a more general
>version of row that works for any monad M using:
>
>
>    mapl  :: (a -> M b) -> ([a] -> M [b])
>    mapl f []     = unitM []
>    mapl f (x:xs) = f x         `bindM` \y ->
>                    mapl f xs   `bindM` \ys ->
>                    unitM (y:ys)
>




Now that the function row has been generalised
we might as well go one step further by generalising mapl.



First I would like to introduce (for notational convenience only)
the function 

appM :: (a -> M b) -> M a -> M b
appM = flip bindM

Using this function and writing L a instead of [a] one has

mapl :: (a -> M b) -> L a -> M (L b)
mapl f []     = unitM []
mapl f (x:xs) = appM (\y -> appM (unitM . (y:)) (mapl f xs)) (f x)


The generalisation involves the combination of monads.

If M and L are monads, then their composition (M . L) is also a monad 

IFF there exists a function

joinL_M :: L (M (L a)) -> M (L a)

with the following properties

joinL_M . unitL = id
joinL_M . joinL = joinL_M . mapL joinL_M
joinL_M . mapL unitML = unitM
joinL_M . mapLML g = mapML g . joinL_M
joinL_M . mapL joinML = joinML . joinL_M

where

unitML = unitM . unitL
mapML = mapM . mapL  
joinML = joinM . mapM joinL_M
 

or, equivalently, IFF there exists a function

swapL_M :: L (M a) -> M (L a)

with the following properties

swapL_M . unitL = mapM unitL
swapL_M . joinL = mapM joinL . swapL_M . mapL swapL_M
swapL_M . mapL unitM = unitM
swapL_M . mapL joinM = joinM . mapM swapL_M . swapL_M
swapL_M . mapLM f = mapML f . swapL_M


or, equivalently, IFF there exists a function

appM_L :: (L a -> M b) -> L (M a) -> M b

with similar properties 

(the details will appear in a forthcoming paper)

the functions joinL_M, swapL_M and appM_L
can be defined in terms of each other as follows :

swapL_M = joinL_M . mapL (mapM unitL)
appM_L f = joinM . mapM f . swapL_M
joinL_M = appM_L (unitM . joinL)

888888888888888888888888888888888888888888888
88 Now we are ready for the generalisation 88
888888888888888888888888888888888888888888888

we can define a general purpose function


	mapM_L :: (a -> M b) -> L a -> M (L b)
	mapM_L f = joinL_M . mapL (mapM unitL . f)



In the case of lists the function appM_L looks as follows

appM_L f [] = f []
appM_L f [m] = appM (f . unitL) m
appM_L f (m:ms) = appM (\y -> appM_L (f . (y:)) ms) m


Let's proof that mapl and mapM_L are equal !

it is clear that

mapl f []     = unitM []
and
mapl f (x:xs) = 
 appM (\y -> appM (unitM . (y:)) (mapl f xs)) (f x)


mapM_L f [] = unitM []
and
mapM_L f (x:xs) 
 = joinL_M . mapL (mapM unitL . f) (x:xs)
 = (appM_L (unitM . joinL) . mapL (mapM unitL . f)) (x:xs)
 = appM_L (unitM . joinL) (mapL (mapM unitL . f) (x:xs))
 = appM_L (unitM . joinL) (mapM unitL . f) x : (mapL (mapM unitL . f) xs)
 = appM (\y -> appM_L (unitM . joinL . (y:)) (mapL (mapM unitL . f) xs) (mapM unitL . f) x
 = appM (\y -> appM_L (unitM . joinL . (y:)) (mapL (mapM unitL . f) xs) (mapM unitL (f x))
 = appM (\y -> appM_L (unitM . joinL . ((unitL y):)) (mapL (mapM unitL . f) xs)) (f x)

(the last equation uses : appM g . mapM f = appM (g . f))


thus mapl f [] = mapM_L f [] and we can now use INDUCTION
 

thus we have to prove that

appM (unitM . (y:)) ((appM_L (unitM . joinL) . mapL (mapM unitL . f)) xs)
 is equal to
appM_L (unitM . joinL . ((unitL y):)) (mapL (mapM unitL . f) xs)

or equivalently

appM (unitM . (y:)) . appM_L (unitM . joinL) . mapLM unitL 
 is equal to
appM_L (unitM . joinL . ((unitL y):)) . mapLM unitL 

NOW

appM (unitM . (y:)) . appM_L (unitM . joinL) . mapLM unitL
 = appM (unitM . (y:)) . joinL_M . mapL (swapL_M . unitL)
 = appM (unitM . (y:)) . joinL_M . mapL swapL_M . mapL unitL 
 = appM (unitM . (y:)) . mapM joinL . swapL_M . mapL swapL_M . mapL unitL
 = appM (unitM . (y:) . joinL) . swapL_M . mapL (swapL_M . unitL)
 = appM (unitM . joinL . ((unitL y):)) . swapL_M . mapLM unitL


and we are done!!


TO CONCLUDE :


If M and L are monads and if their combination M . L is again a monad,
then one can define a function

 
	mapM_L :: (a -> M b) -> L a -> M (L b)
	mapM_L f = joinL_M . mapL (mapM unitL . f)


of which mapl (and therefore also row) is a special case.


BTW: 

 I'd like to thank Mark Jones for all the 
 work he is doing for making the use of monads
 in gofer notationally more convenient.


PS:

it would be nice to be able to write something like


	( Monad M, Monad L) => Monad (M . L) where
		prod :: (L . M . L) a -> (M . L) a

		map = map . map
		unit = unit . unit
		join = join . map prod
 



Luc Duponcheel.  (ldup@alcbel.be)


    \_        \_\_\_    \_   \_    \_\_\_    
     \_        \_    \_  \_   \_    \_   \_     
      \_        \_    \_  \_   \_    \_\_\_
       \_        \_   \_   \_   \_    \_
        \_\_\_\_  \_\_\_    \_\_\_\_   \_