Thread View: comp.lang.functional
2 messages
2 total messages
Started by Luc Duponcheel
Mon, 14 Dec 1992 15:00
for monad lovers only
Author: Luc Duponcheel
Date: Mon, 14 Dec 1992 15:00
Date: Mon, 14 Dec 1992 15:00
201 lines
5473 bytes
5473 bytes
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)
\_ \_\_\_ \_ \_ \_\_\_
\_ \_ \_ \_ \_ \_ \_
\_ \_ \_ \_ \_ \_\_\_
\_ \_ \_ \_ \_ \_
\_\_\_\_ \_\_\_ \_\_\_\_ \_
Re: for monad lovers only
Author: Mark P. Jones
Date: Wed, 16 Dec 1992 15:33
Date: Wed, 16 Dec 1992 15:33
117 lines
4870 bytes
4870 bytes
In article <1927@alcbel.be> ldup@ta7s49.alcbel.be (Luc Duponcheel) writes:
| 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.
Thanks Luc! I've worked through your message and I thought you (and
others) might be interested to see how it looks in the notation I'm
using.
First of all, Luc gives three equivalent conditions for being able
to compose two monads to form another. More precisely, Luc gives three
operators and states that, if you can find a definition for one of these
satisfying certain laws, then you can compose the monads (and give
definitions for the other two operators).
With this in mind, we introduce a two parameter class of composable
monads:
class (Monad m, Monad l) => Composable m l where
prod :: l (m (l a)) -> m (l a)
swap :: l (m a) -> m (l a)
app :: (l a -> m b) -> l (m a) -> m b
prod = app (return . join)
swap = prod . map (map return)
app f = join . map f . swap
In order to specify an instance of this class, we only need to specify
a value for one of the three functions prod, swap and app. The default
definitions at the end of the class declaration can be used to generate
the other two. (Of course, it would be a mistake to omit definitions
for all three since the definitions are obviously circular). For
example, we can express the fact that any monad is composable with the
list monad by writing:
instance Composable m [ ] where
swap [] = [ [] ]
swap (x:xs) = [ y:ys | y<-x, ys<-swap xs ]
(In the context of a type expression, the notation [ ] represents the
list constructor. I didn't want to make another reserved word, although
things might be prettier to if we wrote it as List.)
Now Luc's generalization of my generalization can be defined by:
mmap f = swap . map f
This is equivalent to Luc's original definition (from subsequent mail,
I think both Luc and I discovered this simpler form after he had sent
his message). You'll notice that I've left of the type of mmap; this
is so that I can show you that type inference really does give the
type we want:
? :t mmap
mmap :: Composable b d => (a -> b c) -> d a -> b (d c)
?
Ok, so we might have used names like l and m instead of b and d,
but other than that, this is the type that you would expect.
| 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
Here's the closest that I can get to this at the moment. I'm not
sure how useful this would be for practical programming though.
Perhaps somebody else can comment on that.
First, the definition of the composition of two type constructors:
type Comp f g a = f (g a) in mapComp, returnComp, joinComp
This uses a restricted type synonym; the expansion of Comp f g a
is only permitted in the binding groups of the functions mapComp,
returnComp and joinComp to be defined below.
Let's start with the fact that Comp f g is a functor:
mapComp :: (Functor f,Functor g) => (a->b) -> (Comp f g a->Comp f g b)
mapComp = map . map
instance (Functor f, Functor g) => Functor (Comp f g) where
map = mapComp
Now we can move on to describe the monad structure of the composition:
returnComp :: (Monad f, Monad g) => a -> Comp f g a
returnComp = return . return
joinComp :: (Composable f g) => Comp f g (Comp f g a) -> Comp f g a
joinComp = join . map prod
instance Composable f g => Monad (Comp f g) where
return = returnComp
join = joinComp
How does that look?
All the best,
Mark
Thread Navigation
This is a paginated view of messages in the thread with full content displayed inline.
Messages are displayed in chronological order, with the original post highlighted in green.
Use pagination controls to navigate through all messages in large threads.
Back to All Threads