home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #30 / NN_1992_30.iso / spool / comp / lang / function / 1455 < prev    next >
Encoding:
Internet Message Format  |  1992-12-14  |  5.1 KB
  1. Path: sparky!uunet!mcsun!ub4b!alcbel!ta7s49.alcbel.be
  2. From: ldup@ta7s49.alcbel.be (Luc Duponcheel)
  3. Newsgroups: comp.lang.functional
  4. Subject: for monad lovers only
  5. Message-ID: <1927@alcbel.be>
  6. Date: 14 Dec 92 15:00:47 GMT
  7. Sender: ldup@alcbel.be
  8. Organization: Alcatel Bell Telephone, Antwerpen, Belgium
  9. Lines: 207
  10.  
  11. In his article jones-mark@cs.yale.edu (Mark Jones) writes something like :
  12.  
  13. >Now we're ready for the generalization.  The type constructor
  14. >State b is a monad M so that we could actually define a more general
  15. >version of row that works for any monad M using:
  16. >
  17. >
  18. >    mapl  :: (a -> M b) -> ([a] -> M [b])
  19. >    mapl f []     = unitM []
  20. >    mapl f (x:xs) = f x         `bindM` \y ->
  21. >                    mapl f xs   `bindM` \ys ->
  22. >                    unitM (y:ys)
  23. >
  24.  
  25.  
  26.  
  27.  
  28. Now that the function row has been generalised
  29. we might as well go one step further by generalising mapl.
  30.  
  31.  
  32.  
  33. First I would like to introduce (for notational convenience only)
  34. the function 
  35.  
  36. appM :: (a -> M b) -> M a -> M b
  37. appM = flip bindM
  38.  
  39. Using this function and writing L a instead of [a] one has
  40.  
  41. mapl :: (a -> M b) -> L a -> M (L b)
  42. mapl f []     = unitM []
  43. mapl f (x:xs) = appM (\y -> appM (unitM . (y:)) (mapl f xs)) (f x)
  44.  
  45.  
  46. The generalisation involves the combination of monads.
  47.  
  48. If M and L are monads, then their composition (M . L) is also a monad 
  49.  
  50. IFF there exists a function
  51.  
  52. joinL_M :: L (M (L a)) -> M (L a)
  53.  
  54. with the following properties
  55.  
  56. joinL_M . unitL = id
  57. joinL_M . joinL = joinL_M . mapL joinL_M
  58. joinL_M . mapL unitML = unitM
  59. joinL_M . mapLML g = mapML g . joinL_M
  60. joinL_M . mapL joinML = joinML . joinL_M
  61.  
  62. where
  63.  
  64. unitML = unitM . unitL
  65. mapML = mapM . mapL  
  66. joinML = joinM . mapM joinL_M
  67.  
  68.  
  69. or, equivalently, IFF there exists a function
  70.  
  71. swapL_M :: L (M a) -> M (L a)
  72.  
  73. with the following properties
  74.  
  75. swapL_M . unitL = mapM unitL
  76. swapL_M . joinL = mapM joinL . swapL_M . mapL swapL_M
  77. swapL_M . mapL unitM = unitM
  78. swapL_M . mapL joinM = joinM . mapM swapL_M . swapL_M
  79. swapL_M . mapLM f = mapML f . swapL_M
  80.  
  81.  
  82. or, equivalently, IFF there exists a function
  83.  
  84. appM_L :: (L a -> M b) -> L (M a) -> M b
  85.  
  86. with similar properties 
  87.  
  88. (the details will appear in a forthcoming paper)
  89.  
  90. the functions joinL_M, swapL_M and appM_L
  91. can be defined in terms of each other as follows :
  92.  
  93. swapL_M = joinL_M . mapL (mapM unitL)
  94. appM_L f = joinM . mapM f . swapL_M
  95. joinL_M = appM_L (unitM . joinL)
  96.  
  97. 888888888888888888888888888888888888888888888
  98. 88 Now we are ready for the generalisation 88
  99. 888888888888888888888888888888888888888888888
  100.  
  101. we can define a general purpose function
  102.  
  103.  
  104.     mapM_L :: (a -> M b) -> L a -> M (L b)
  105.     mapM_L f = joinL_M . mapL (mapM unitL . f)
  106.  
  107.  
  108.  
  109. In the case of lists the function appM_L looks as follows
  110.  
  111. appM_L f [] = f []
  112. appM_L f [m] = appM (f . unitL) m
  113. appM_L f (m:ms) = appM (\y -> appM_L (f . (y:)) ms) m
  114.  
  115.  
  116. Let's proof that mapl and mapM_L are equal !
  117.  
  118. it is clear that
  119.  
  120. mapl f []     = unitM []
  121. and
  122. mapl f (x:xs) = 
  123.  appM (\y -> appM (unitM . (y:)) (mapl f xs)) (f x)
  124.  
  125.  
  126. mapM_L f [] = unitM []
  127. and
  128. mapM_L f (x:xs) 
  129.  = joinL_M . mapL (mapM unitL . f) (x:xs)
  130.  = (appM_L (unitM . joinL) . mapL (mapM unitL . f)) (x:xs)
  131.  = appM_L (unitM . joinL) (mapL (mapM unitL . f) (x:xs))
  132.  = appM_L (unitM . joinL) (mapM unitL . f) x : (mapL (mapM unitL . f) xs)
  133.  = appM (\y -> appM_L (unitM . joinL . (y:)) (mapL (mapM unitL . f) xs) (mapM unitL . f) x
  134.  = appM (\y -> appM_L (unitM . joinL . (y:)) (mapL (mapM unitL . f) xs) (mapM unitL (f x))
  135.  = appM (\y -> appM_L (unitM . joinL . ((unitL y):)) (mapL (mapM unitL . f) xs)) (f x)
  136.  
  137. (the last equation uses : appM g . mapM f = appM (g . f))
  138.  
  139.  
  140. thus mapl f [] = mapM_L f [] and we can now use INDUCTION
  141.  
  142.  
  143. thus we have to prove that
  144.  
  145. appM (unitM . (y:)) ((appM_L (unitM . joinL) . mapL (mapM unitL . f)) xs)
  146.  is equal to
  147. appM_L (unitM . joinL . ((unitL y):)) (mapL (mapM unitL . f) xs)
  148.  
  149. or equivalently
  150.  
  151. appM (unitM . (y:)) . appM_L (unitM . joinL) . mapLM unitL 
  152.  is equal to
  153. appM_L (unitM . joinL . ((unitL y):)) . mapLM unitL 
  154.  
  155. NOW
  156.  
  157. appM (unitM . (y:)) . appM_L (unitM . joinL) . mapLM unitL
  158.  = appM (unitM . (y:)) . joinL_M . mapL (swapL_M . unitL)
  159.  = appM (unitM . (y:)) . joinL_M . mapL swapL_M . mapL unitL 
  160.  = appM (unitM . (y:)) . mapM joinL . swapL_M . mapL swapL_M . mapL unitL
  161.  = appM (unitM . (y:) . joinL) . swapL_M . mapL (swapL_M . unitL)
  162.  = appM (unitM . joinL . ((unitL y):)) . swapL_M . mapLM unitL
  163.  
  164.  
  165. and we are done!!
  166.  
  167.  
  168. TO CONCLUDE :
  169.  
  170.  
  171. If M and L are monads and if their combination M . L is again a monad,
  172. then one can define a function
  173.  
  174.  
  175.     mapM_L :: (a -> M b) -> L a -> M (L b)
  176.     mapM_L f = joinL_M . mapL (mapM unitL . f)
  177.  
  178.  
  179. of which mapl (and therefore also row) is a special case.
  180.  
  181.  
  182. BTW: 
  183.  
  184.  I'd like to thank Mark Jones for all the 
  185.  work he is doing for making the use of monads
  186.  in gofer notationally more convenient.
  187.  
  188.  
  189. PS:
  190.  
  191. it would be nice to be able to write something like
  192.  
  193.  
  194.     ( Monad M, Monad L) => Monad (M . L) where
  195.         prod :: (L . M . L) a -> (M . L) a
  196.  
  197.         map = map . map
  198.         unit = unit . unit
  199.         join = join . map prod
  200.  
  201.  
  202.  
  203.  
  204. Luc Duponcheel.  (ldup@alcbel.be)
  205.  
  206.  
  207.     \_        \_\_\_    \_   \_    \_\_\_    
  208.      \_        \_    \_  \_   \_    \_   \_     
  209.       \_        \_    \_  \_   \_    \_\_\_
  210.        \_        \_   \_   \_   \_    \_
  211.         \_\_\_\_  \_\_\_    \_\_\_\_   \_      
  212.  
  213.  
  214.  
  215.  
  216.  
  217.  
  218.