Transcription
Composing monads Mark P. JonesYale UniversityNew Haven, CT, U.S.A.jones-mark@cs.yale.eduLuc DuponcheelAlcatel Bell TelephoneAntwerp, Belgiumldup@ra.alcbel.beResearch Report YALEU/DCS/RR-1004, December 1993AbstractMonads are becoming an increasingly important tool for functional programming. Different monads can be used to model a wide range of programming language features. However, real programs typically require a combination of differentfeatures, so it is important to have techniques for combining several features in asingle monad. In practice, it is usually possible to construct a monad that supportssome specific combination of features. However, the techniques used are typicallyad-hoc and it is very difficult to find general techniques for combining arbitrarymonads.This report gives three general constructions for the composition of monads,each of which depends on the existence of an auxiliary function linking the monadstructures of the components. In each case, we establish a set of laws that theauxiliary function must satisfy to ensure that the composition is itself a monad.Using the notation of constructor classes, we describe some specific applicationsof these constructions. These results are used in the development of a simple expression evaluator that combines exceptions, output and an environment of variablebindings using a composition of three corresponding monads.1IntroductionIn recent years, the concept of a monad – an idea that was originally motivated byhigh-level abstract algebra – has become an important and practical tool for functionalprogrammers. The reason for this is that monads provide a uniform framework for describing a wide range of programming language features including, for example, state,I/O, continuations, exceptions, parsing and non-determinism, without leaving the framework of a purely functional language. Many of these techniques were already familiar tofunctional programmers, but there are many new insights when they are reinterpretedas specific instances of a more general concept. A Gofer script containing executable versions of the programs described in this report is currentlyavailable by anonymous ftp from nebula.cs.yale.edu in the file pub/yale-fp/reports/RR-1004.gs.1
Much of the initial interest in monads has been motivated by the work of Wadler [14, 15]who, in turn, drew inspiration from the work of Moggi [9] and Spivey [12]. Monadsare already widely used in both small and large programs (for example, the GlasgowHaskell compiler, the largest Haskell program known to us at the time of writing, makessubstantial use of monads [2]). New approaches to old problems have been proposed,relying heavily on the use of monads. For example, the I/O monad proposed in [11]is already widely used and may soon be included as part of the definition of Haskell.Monads are even influencing the design of programming languages. For example, monadsprovide an important motivating example for the system of constructor classes presentedin [5].With the exception of [8], questions about how monads can be combined have, so far,received surprisingly little attention. This is an important topic because many realprograms require a combination of features, for example, state, I/O and exceptions. Inpractice, it is usually possible to construct a suitable monad that supports the desiredcombination of features, but the methods used are typically ad-hoc and monolithic.The goal of this report is to investigate some techniques for combining monads by aprocess of composition and to illustrate how these constructions can be used in practice.The conditions required to build a composite monad are quite complex, but we hope thatthis work will provide a step towards a more modular approach to the use of monads.One of the nicest features about monads is that, with a little practice (and perhaps, somecarefully chosen syntax), it is actually quite easy to write programs in a monadic stylewithout any knowledge of the abstract theoretical underpinnings. In the same spirit,this report is directed at functional programmers with an interest in using monads aspart of a practical programming project, rather than the underlying category theory. Tothis end, in a number of places, we have intentionally chosen to give definitions or resultswithout reference to the corresponding categorical concepts. Readers with an interestin a more technical, category theoretic presentation of the ideas described in this reportare referred to [1].We will assume some familiarity with the motivation for monads and their use in structuring functional programs; Wadler [14, 15] provides an excellent introduction to thesetopics. Programming examples will be written using the syntax of Gofer, a small, experimental, purely functional language based closely on the definition of Haskell [3]. Thisenables us to use constructor classes [5] to show how our results can be expressed in aconcrete programming language.For completeness, we have included detailed proofs for many of our results. In keepingwith our aim to avoid unnecessary technical details, most of the proofs are constructedfrom first principles using simple equational reasoning. Working in this manner has leadto some surprising insights. For example, one of our results in Section 3 correspondsclosely to a result stated in [8], but a careful study of the laws that are actually used inthe proof has allowed us to weaken the hypotheses and state the result in a slightly moregeneral form. However, recognizing that some readers may prefer to omit such details,most of the proofs are presented in boxed figures that are easily identified and skipped.2
The remainder of this report is organized as follows. Section 2 gives a definition of thealgebraic properties of a monad, and these are then used to describe the constructionof compositions of monads in Section 3 and their converses in Section 4. Moving onto practical applications, Section 5 describes how these results about composition ofmonads can be expressed using the notation of constructor classes, with several examplesin Section 6. A simple application, building on this framework, is included in Section 7.Finally, Section 8 illustrates that there are other ways of combining certain monads,setting a direction for future work.2Monads for functional programmingWadler [14] defines a monad as a unary type constructor M together with three functionsmap, unit and join whose types are given by:map :: (a b) (M a M b)unit :: a M ajoin :: M (M a) M aIn addition, these functions are required to satisfy a collection of algebraic laws:map idmap f . map g id map (f . g)(1)(2)unit . f map f . unit(3)joinjoinjoinjoin (4)(5)(6)(7).map (map f )unitmap unitmap joinmap f . joinididjoin . join(We use the standard infix period notation for function composition, (f . g) x f (g x ),and the symbol id to represent the identity function id x x . It is well known thatcomposition of functions is associative with id as both a left and right identity; insymbols, f . (g . h) (f . g) . h and f . id f id . f for all f , g and h of appropriatetypes.)For the purposes of this report, it will be convenient to break this down into stages; ifM is a unary type constructor, then we will say that: M is a functor if there is a function map :: (a b) (M a M b) satisfyinglaws (1) and (2) above. M is a premonad if it is a functor with a function unit :: a M a satisfying law(3) above. M is a monad if it is a premonad with a function join :: M (M a) M a satisfyinglaws (4), (5), (6) and (7) above.3
It should be mentioned that there are several other (equivalent) ways to define theconcept of a monad, each of which comes with its own collection of monad operators andequational laws. For example, Wadler [15] describes how a monad can be characterizedusing just the unit function together with an operatorbind:: M a (a M b) M bBoth the map and join operators that we have described can be defined using bind andunit. The bind operator is particularly useful in practical work with monads and as ameans of translating the notation of monad comprehensions [14, 15, 5]. Furthermore,only three laws are needed to specify the properties of a monad in this case. Nevertheless,we have chosen to work with the map, unit, join formulation of monads outlined above.One reason for this decision is that, in our opinion, many of the proofs are easier toexpress in this framework. In addition, we will see that the ability to distinguish betweenmonads and premonads will also be quite useful in the following work.3Conditions for compositionSuppose that M and N are functors. To avoid confusion, we will write mapM and mapNfor the corresponding map functions in each case. How is it possible to compose thesefunctors in some sensible way? Certainly, we can think of a composition of M and N asa type constructor that takes any type a to the type M (N a), but we also need to beable to give a definition formap :: (a b) (M (N a) M (N b))satisfying the functor laws (1) and (2). Fortunately, this is quite easy! If f :: a b,then we can apply mapN to obtain mapN f :: N a N b and then apply mapM toobtain mapM (mapN f ) :: M (N a) M (N b). This gives the definitionmap mapM . mapNand we can use the proofs in Figure 1 to show that this does satisfy the necessary laws.These proofs use standard techniques of equational reasoning, writing the justificationfor each step in the right hand column. In many cases, this is just a reference to thelaw that has been used, with the convention that, for example, (1M) is the version oflaw (1) for the constructor M . Where a step follows directly from the definition of afunction (either by folding or unfolding the definition), we will simply write the name ofthe function involved as justification.Composition of premonads is similar. Most of the work (the definition of the composedtype constructor) has already been dealt with in the composition of functors. A suitableunit function for the composition is:unitunit:: a M (N a) unitM . unitN4
map id mapM (mapN id ) mapM id idmap(1N)(1M)map f . map g map, map(2M)(2N)mapmapM (mapN f ) . mapM (mapN g)mapM (mapN f . mapN g)mapM (mapN (f . g))map (f . g)Figure 1: Composition of functors, laws (1)–(2)(unitM and unitN being the unit functions for M and N respectively) and the proof inFigure 2 demonstrates that this does indeed satisfy law (3).unit . f unitMunitMmapMmap f. unitN . f. mapN f . unitN(mapN f ) . unitM . unitN. unitunit(3N)(3M)map, unitFigure 2: Composition of premonads, law (3)Unfortunately, our real goal, composition of monads, is rather more difficult. Recallthat, to define the composition of two monads M and N , we need to find a function:join :: M (N (M (N a))) M (N a)that satisfies the monad laws (4)–(7). As a first guess, and following the pattern of theprevious examples, we might consider the function joinM . joinN where joinM and joinNare the join functions in the component monads. But this is, in general, not even typecorrect! If x :: N (N a) (for some a), then the result of joinN x will have type N awhile joinM expects an argument with a type of the form M (M b).In fact, we can actually prove that, in a certain sense, there is no way to construct ajoin function with the type above using only the operations of the two monads (seethe appendix for an outline of the proof). It follows that the only way that we mighthope to form a composition is if there are some additional constructions linking thetwo components. In this report we will concentrate on four methods for constructing acomposite monad, described in the following sections.5
3.1The trivial case, by definitionThe composite of two premonads M and N is a monad if there is a polymorphic function:join :: M (N (M (N a))) M (N a)satisfying the laws (4), (5), (6) and (7). This, of course, follows directly from thedefinitions above.3.2The prod constructionThe composition of a monad M with a premonad N is itself a monad if there is apolymorphic function:prod:: N (M (N a)) M (N a)with the join function defined by:join joinM . mapM prodsatisfying the following four laws:prodprodprodprod.mapN (map f )unitNmapN unitmapN join map f . prodidunitMjoin . prodP(1)P(2)P(3)P(4)The proofs for this are given in Figure 3. One interesting point is that, when we startedthis work, we had assumed that it would be necessary to require that both M and Nbe monads. In fact, from the proofs, we see that we did not actually need any of themonad laws for N at all! As a result, we can construct a ‘composition of monads’ undersomewhat weaker conditions than originally expected.3.3The dorp constructionThe composition of a premonad M with a monad N is itself a monad if there is apolymorphic function:dorp :: M (N (M a)) M (N a)with the join function defined by:join mapM joinN . dorpsuch that the following laws hold:dorpdorpdorpdorp.map (mapM f )unitmap unitMjoin map f . dorpmapM unitNidjoin . map dorpD(1)D(2)D(3)D(4)Full proofs for this are given in Figure 4. In this case, we use the fact that N is a monad,although M can be an arbitrary premonad.6
join . map (map f )joinM . mapMjoinM . mapMjoinM . mapMjoinM . mapMjoinM . mapMmapM (mapNmap f . joinjoin . unitjoinM . mapM prod . unitM . unitNjoinM . unitM . prod . unitNprod . unitNidjoin, unit(3M)(5M)P(2)join . map unitjoinM . mapM prod . mapM (mapN unit)joinM . mapM (prod . mapM unit)joinM . mapM unitMidjoin, map(2M)P(3)(6M)join . map joinjoinM . mapMjoinM . mapMjoinM . mapMjoinM . mapMjoinM . mapMjoinM . joinMjoinM . mapMjoin . joinjoin, map(2M)P(4)join(2M)(7M)(4M)join, joinprod . mapM (mapN (map f ))(prod . mapN (map f ))(map f . prod )(map f ) . mapM prod(mapM (mapN f )) . mapM prodf ) . joinM . mapM prodprod . mapM (mapN join)(prod . mapN join)(join . prod )(joinM . mapM prod . prod )joinM . mapM (mapM prod ) . mapM prod. mapM (mapM prod ) . mapM prodprod . joinM . mapM prodjoin, map(2M)P(1)(2M)map(4M)map, joinFigure 3: Composition of monads, laws (4)–(7), with join joinM . mapM prod7
join . map (map f )mapM joinN . dorp . map (mapM (mapN f ))mapM joinN . map (mapN f ) . dorpmapM joinN . mapM (mapN (mapN f )) . dorpmapM (joinN . mapN (mapN f )) . dorpmapM (mapN f . joinN ) . dorpmapM (mapN f ) . mapM joinN . dorpmap f . joinjoin, mapD(1)map(2M)(4N)(2M)map, joinjoin . unitmapMmapMmapMmapMidjoinD(2)(2M)(5N)(1M)join . map unitmapM joinN . dorp . map (unitM . unitN )mapM joinN . dorp . map unitM . map unitNmapM joinN . map unitNmapM joinN . mapM (mapN unitN )mapM (joinN . mapN unitN )mapM ididjoin, unit(2)D(3)map(2M)(6N)(1M)join . map joinmapM joinN . dorp . map (mapM joinN . dorp)mapM joinN . dorp . map (mapM joinN ) . map dorpmapM joinN . map joinN . dorp . map dorpmapM joinN . mapM (mapN joinN ) . dorp . map dorpmapM (joinN . mapN joinN ) . dorp . map dorpmapM (joinN . joinN ) . dorp . map dorpmapM joinN . mapM joinN . dorp . map dorpmapM joinN . join . map dorpmapM joinN . dorp . joinjoin . joinjoin, join(2)D(1)map(2M)(7N)(2M)joinD(4)joinjoinN . dorp . unitjoinN . mapM unitN(joinN . unitN )idFigure 4: Composition of monads, laws (4)–(7), with join mapM joinN . dorp8
3.4The swap constructionWe can also define the composition of two monads M and N in terms of a polymorphicfunction:swap :: N (M a) M (N a)with the join function defined by:join mapM joinN . joinM . mapM swapsatisfying a collection of laws given below. Note that this is equivalent to:join joinM . mapM (mapM joinN . swap)since:mapM joinN . joinM . mapM swap joinM . mapM (mapM joinN ) . mapM swap joinM . mapM (mapM joinN . swap).(4M)(2M)In order to state the laws for swap, we define two (familiarly named) functions as abbreviations for expressions involving swap:prod mapM joinN . swapdorp joinM . mapM swapWe will justify the use of these names below, but first we state the laws that the swapfunction must satisfy:swap . mapN (mapM f )swap . unitNswap . mapN unitMprod . mapN dorp mapM (mapN f ) . swapmapM unitNunitMdorp . prodS(1)S(2)S(3)S(4)It is possible to prove the existence of the composite monad using these definitions alone.However, it is easier, and perhaps more instructive, to do this indirectly by exploringthe relationship between swap, prod and dorp.First of all, note that the definition of join coincides with the join that would be obtainedusing the prod construction (with the above definition of prod ):joinM . mapM prod joinM . mapM (mapM joinN . swap) joinprodjoinFurthermore, the definition of join also coincides with the join function that we wouldobtain using the dorp construction (with the above definition of dorp):mapM joinN . dorp mapM joinN . (joinM . mapM swap) joindorpjoinAssuming that laws S(1)–S(4) are satisfied, the proofs in Figures 5 and 6 show that prodand dorp satisfy laws P(1)–P(4) and D(1)–D(4), respectively. Note that, in each case,both M and N must be monads if the composite is also to be a monad. For example, theproof of P(1)–P(4) requires the monad laws for N , while the prod construction requiresthat M should also be a monad.9
prod . mapN (map f )mapM joinN . swap . mapN (mapM (mapN f ))mapM joinN . mapM (mapN (mapN f )) . swapmapM (joinN . mapN (mapN f )) . swapmapM (mapN f . joinN ) . swapmapM (mapN f ) . mapM joinN . swapmap f . prodprod , mapS(1)(2M)(4N)(2M)map, prodprod . unitNmapMmapMmapMmapMidprodS(2)(2M)(5N)(1M)prod . mapN unitmapM joinN . swap . mapN (unitM . unitN )mapM joinN . swap . mapN unitM . mapN unitNmapM joinN . unitM . mapN unitNunitM . joinN . mapN unitNunitMprod , unit(2N)S(3)(3M)(6N)prod . mapN joinprod . mapN (mapM joinN . dorp)mapM joinN . swap . mapN (mapM joinN ) . mapN dorpmapM joinN . mapM (mapN joinN ) . swap . mapN dorpmapM (joinN . mapN joinN ) . swap . mapN dorpmapM (joinN . joinN ) . swap . mapN dorpmapM joinN . mapM joinN . swap . mapN dorpmapM joinN . prod . mapN dorpmapM joinN . dorp . prodjoin . prodjoinprod , (2N)S(1)(2M)(7N)(2M)prodS(4)joinjoinN . swap . unitNjoinN . mapM unitN(joinN . unitN )idFigure 5: Proof of P(1)–P(4) from S(1)–S(4) with prod mapM joinN . swap10
dorp . map (mapM f )joinM . mapM swap . mapM (mapN (mapM f ))joinM . mapM (swap . mapN (mapM f ))joinM . mapM (mapM (mapN f ) . swap)joinM . mapM (mapM (mapN f )) . mapM swapmapM (mapN f ) . joinM . mapM swapmap f . dorpdorp, map(2M)S(1)(2M)(4M)map, dorpdorp . unitjoinM . mapM swap . unitM . unitNjoinM . unitM . swap . unitNswap . unitNmapM unitNdorp, unit(3M)(5M)S(2)dorp . map unitMjoinM . mapM swap . mapM (mapN unitM )joinM . mapM (swap . mapN unitM )joinM . mapM unitMiddorp, map(2M)S(3)(6M)dorp . joinjoinMjoinMjoinMjoinMjoinMjoinMjoinMjoin .dorp, join(4M)(7M)(2M)dorpS(4)(2M), mapjoin. mapM swap . joinM . mapM prod. joinM . mapM (mapM swap) . mapM prod. mapM joinM . mapM (mapM swap) . mapM prod. mapM (joinM . mapM swap . prod ). mapM (dorp . prod ). mapM (prod . mapN dorp). mapM prod . map dorpmap dorpFigure 6: Proof of D(1)–D(4) from S(1)–S(4) with dorp joinM . mapM swap11
3.5SummaryAt first glance, the constructions in the previous sections may seem rather mysterious;in each case, we gave a type for some polymorphic function, stated some laws that itshould satisfy . . . and ‘presto!’ we have another way of composing monads. In fact,these constructions were discovered largely by experimentation, ‘guessing’ a definition ofjoin in some particular form, for example join joinM . mapM prod , then attemptingto prove the monad laws, for example, to determine what properties prod should satisfy.Types played an essential part in this process, helping to suggest ways to define joinand ensuring that the laws we used are well-typed.The following diagram summarizes these results and the relationship between the different constructions for compositions of monads:prod :: N (M (N a)) M (N a)satisfying P(1)–P(4)Nµ¡¡swap :: N (M a) M (N a)satisfying S(1)–S(4)M, NM@@R-join :: M (N (M (N a))) M (N a)satisfying (4)–(7)@RM@dorp :: M (N (M a)) M (N a)¡µ¡Nsatisfying D(1)–D(4)In each case, the arrows between different constructions represent implications, with thelabels indicating which of the constructors M and N is required to be a monad.4Converse resultsWe now have a number of different ways of composing two monads, but we have notmade any attempt to see how general each approach might be. In particular, it is naturalto ask what kinds of monads can be obtained using the constructions described above.Thinking of the diagram at the end of the previous section, we know by definition thatall compositions of M and N must have a join function as specified by the rightmostbox. The goal of this section is to establish what conditions are necessary to move back,in the opposite direction of the arrows, to each of the other three constructions.More formally, suppose that M and N are monads and that there is a composition ofM and N with operators map, unit and join satisfying the laws (1)–(7) and such that:map mapM . mapNunit unitM . unitNThe problem now is to determine which composite monads defined in this way can beobtained using each of the prod , dorp and swap constructions.12
4.1The prod constructionIt is actually fairly easy to give a definition for a prod function (of the required type) interms of the various monad operators available:prod join . unitMShowing that this definition of prod satisfies the laws P(1)–P(4) is also straightforward,as detailed by the proofs in Figure 7. In fact, the only difficulty arises when we try tomap f . prodmap f . join . unitMjoin . map (map f ) . unitMjoin . mapM (mapN (map f )) . unitMjoin . unitM . mapN (map f )prod . mapN (map f )prod(4)map(3M)prodprod . unitNjoin . unitM . unitNjoin . unitidprodunit(5)prod . mapN unitjoin . unitM . mapN unitjoin . mapM (mapN unit) . unitMjoin . map unit . unitMunitMprod(3M)map(6)prod . mapN joinjoin . unitM . mapN joinjoin . mapM (mapN join) . unitMjoin . map join . unitMjoin . join . unitMjoin . prodprod(3M)map(7)prodFigure 7: Proof of P(1)–P(4) from the existence of a compositionshow that the join function we obtain from the prod construction is the same as the joinfunction that we started with. One way to do this is as follows:joinM . mapM prod joinM . mapM (join . unitM )joinM . mapM join . mapM unitMjoin . joinM . mapM unitMjoin13prod(2M)J(1)(6M)
Note that this depends on an assumption about the way that join and joinM ‘commute’with one another:joinM . mapM join join . joinMJ(1)This condition may seem a little arbitrary, but it turns out that every composite monadobtained by the prod construction has this property:joinM . mapM join joinMjoinMjoinMjoinMjoin . mapM. mapM. joinM. mapMjoinM(joinM . mapM prod )joinM . mapM (mapM prod ). mapM (mapM prod )prod . joinMjoin(2M)(7M)(4M)joinIt follows that the set of composite monads that can be obtained using the prod construction are precisely those satisfying J(1).4.2The dorp constructionAs in the previous case, it is easy to find a suitably typed definition of the dorp functionusing the operations of the composite monad and its components:dorp join . map (mapM unitN )The proofs in Figure 8 show that this definition satisfies the laws D(1)–D(4) as we wouldhope. Once again, the most difficult task is to show that the join function obtainedfrom this dorp function using the earlier construction is equal to the join operator inthe composite monad. One way to prove this is as follows:mapM joinN . dorp mapM joinN . join . map (mapM unitN ) join . map (mapM joinN ) . map (mapM unitN ) join . map (mapM (joinN . unitN )) join . map (mapM id ) joindorpJ(2)(2), (2M)(5N)(1M), (1)This also depends on an assumed law, this time linking the behaviour of join and joinN :join . map (mapM joinN ) mapM joinN . joinJ(2)In fact, law J(2) holds for all composite monads obtained using the dorp construction,as demonstrated by the following:join . map (mapM joinN )mapM joinN . dorp . map (mapM joinN )mapM joinN . map joinN . dorpmapM (joinN . mapN joinN ) . dorpmapM (joinN . joinN ) . dorpmapM joinN . mapM joinN . dorpmapM joinN . join14joinD(1)map, (2M)(7N)(2M)join
dorp . map (mapM f )join . map (mapM unitN ) . map (mapM f )join . map (mapM (unitN . f ))join . map (mapM (mapN f . unitN ))join . map (map f ) . map (mapM unitN )map f . join . map (mapM unitN )map f . dorpdorp(2), (2M)(3N)(2), (2M), map(4)dorpdorp . unitjoin . map (mapM unitN ) . unitjoin . unit . mapM unitNmapM unitNdorp(3)(5)dorp . mapjoinjoinjoinjoinid(mapM unitN ) . map unitM(mapM unitN . unitM )(unitM . unitN )unitdorp(2)(3M)unit(6)dorp . joinjoinjoinjoinjoinjoinmap (mapM unitN ) . joinjoin . map (map (mapM unitN ))map join . map (map (mapM unitN ))map (join . map (mapM unitN ))map dorpdorp(4)(7)(2)dorpunitM. map. map. map. map.Figure 8: Proof of D(1)–D(4) from the existence of a composition15
4.3The swap constructionOur goal in this section is to determine the class of composite monads that can beconstructed using the swap construction presented in Section 3.4. From the resultsgiven there, any composite obtained using swap can also be obtained from a prod ora dorp construction, so it follows (from the results in the last two sections) that anymonad obtained from swap must satisfy at least J(1) and J(2). In fact, we will nowshow that these two properties are not only necessary, but also sufficient.Following the pattern in the previous cases, we start with a definition for the swapfunction in terms of the join of the composite monad:swap join . unitM . mapN (mapM unitN )or, equivalently:swap join . map (mapM unitN ) . unitMsince:join . unitM . mapN (mapM unitN ) join . mapM (mapN (mapM unitN )) . unitM join . map (mapM unitN ) . unitM .(3M)mapNote that these definitions of swap can also be expressed in terms of the prod and dorpfunctions used in the previous two sections:swap join . unitM . mapN (mapM unitN ) prod . mapN (mapM unitN )swapprodswap join . map (mapM unitN ) . unitM dorp . unitMswapdorpAssuming J(2), we can show that the definition of prod in terms of swap given in Section 3.4 coincides with the prod function specified in terms of join in Section 4.1:mapM joinN . swap mapM joinN . join . unitM . mapN (mapM unitN ) join . map (mapM joinN ) . unitM . mapN (mapM unitN ) join . unitM . mapN (mapM joinN ) . mapN (mapM unitN ) join . unitM . mapN (mapM (joinN . unitN )) join . unitMswapJ(2)map, (3M)(2N), (2M)(5N), (1M), (1N)In a similar way, assuming J(1), we can show that the definition of dorp from swap inSection 3.4 gives the same function as the definition of dorp in Section 4.2:joinM . mapM swap joinM . mapM (join . map (mapM unitN ) . unitM ) joinM . mapM join . mapM (map (mapM unitN ) . unitM ) join . joinM . mapM (map (mapM unitN ) . unitM ) join . map (mapM unitN ) . joinM . mapM unitM join . map (mapM unitN )16swap(2M)J(1)map, (4M), (2M)(6M)
With these results, it is straightforward to show that, given a composite monad satisfyingJ(1) and J(2), the swap function defined above satisfies the laws S(1)–S(4) required forthe swap construction; see Figure 9 for the proofs. For convenience, we have usedswap . mapNdorp .dorp .map fmapMswap . unitNdorp . unitM . unitNdorp . unitmapM unitNswapunitD(2)swap . mapN unitMdorp . unitM . mapN unitMdorp . map unitM . unitMunitMswap(3M), mapD(3)dorp . (mapM f )unitM . mapN (mapM f )map (mapM f ) . unitM. dorp . unitM(mapN f ) . swapproddorp . join . unitMjoin . map dorp . unitMjoin . unitM . mapN dorpprod . mapN dorpswap(3M), mapD(1)map, swapprodD(4)map, (3M)prodFigure 9: Proof of S(1)–S(4) from the existence of a compositionthe properties of dorp described by the laws D(1)–D(4) to establish these properties ofswap. Similar derivations are also possible using the laws for prod , or directly using thedefinition of swap in terms of join although the proofs are a little longer, particularly inthe second case.Given the comments above, this completes the proof that the set of monads which canbe constructed from a swap function are precisely those satisfying both J(1) and J(2).4.4SummaryCorresponding to the diagram in Section 3.5, we can summarize the results about theconverses for the prod , dorp and swap constructions as follows:17
prod :: N (M (N a)) M (N a)satisfying P(1)–P(4)J(2)¡¡ªswap :: N (M a) M (N a)satisfying S(1)–S(4)J(1), J(2)¾J(1)@I@join :: M (N (M (N a))) M (N a)satisfying (4)–(7)@IJ(1)@dorp :: M (N (M a)) M (N a)¡¡J(2)ªsatisfying D(1)–D(4)This time, we have labeled the arrows between the different constructions with theadditional properties required to establish the converse.The properties J(1) and J(2) that we have used in these results are actually fairly similar,each given by a law of the form:join . map f f . joinFor J(1), the join and map functions here should be read as the corresponding operatorsfor the monad M with f the join function in the composite monad. For J(2), the joinand map operators are taken from the composite monad with f mapM joinN .Incidentally, functions satisfying a law of the form shown above are actually quite widelystudied in functional programming. For example, in the special case of the list monadwhere join is just the concatenation of a list of lists (the concat function in Haskell),functions satisfying the law above are often referred to as list homomorphisms.5Programming monad compositionOur goal in this and remaining sections is to show how the different constructions formonad composition presented above can be used in a practical programming language.For convenience, we will use the notation of constructor classes [5] implemented as partof the Gofer system, although the same ideas can also be applied to a much wider rangeof languages.In this section, we present a general framework for working with different forms ofmonad composition. Later, we will describe a number
Yale University New Haven, CT, U.S.A. jones-mark@cs.yale.edu Luc Duponcheel Alcatel Bell Telephone Antwerp, Belgium ldup@ra.alcbel.be Research Report YALEU/DCS/RR-1004, December 1993 Abstract Monads are becoming an increasingly important tool for functional program-ming. Different monads can be used to model a wide range of programming lan .
