Notions of Category Theory in Functional Programming by Shauna C. A . Gammon B.Sc , Memorial University of Newfoundland, 2005 A THESIS SUBMITTED IN PARTIAL F U L F I L M E N T OF T H E R E Q U I R E M E N T S FOR T H E D E G R E E OF Master of Science in The Faculty of Graduate Studies (Mathematics) The University Of British Columbia August, 2007 © Shauna C. A. Gammon 2007 Abst rac t We present a detailed examination of applications of category theory to func-tional programming languages, with a primary focus on monads in Haskell. First, we explore E. Moggi's work in categorical semantics, which provides the theoretical foundation for employing monads in functional languages. In particular, we examine his use of Kleisli triples to model notions of com-putation. We then study P. Wadler's implementation of Moggi's ideas as a means to mimic side-effects in the purely functional language Haskell. We explicitly demonstrate the connections between Kleisli triples, category-theoretic monads, and Haskell monads. It is our principal aim to provide a coherent translation between the abstracted concept of monads that exists in category theory, and the formulation of monads as type-constructors that is implemented in Haskell. n Table of Contents Abstract ii Table of Contents iii Acknowledgements v Dedication vi 1 Introduction 1 1.1 Background 1 1.2 Composition of Natural Transformations 3 1.2.1 Vertical Composition 4 1.2.2 Horizontal Composition 4 1.3 Monads in Category Theory 7 1.3.1 Definition 7 1.3.2 Examples 7 1.4 Category Theory in Haskell 11 1.4.1 Functional Languages and the A-Calculus 11 1.4.2 Cartesian Closed Categories 14 1.4.3 Types in Haskell 15 1.5 Haskell 20 1.5.1 Haskell's Type System 20 2 Moggi's Monads 23 2.1 Motivation for Monads in Haskell 23 2.1.1 Heuristics 23 2.2 Kleisli constructions 25 2.2.1 Example: State Updates 28 2.3 Triples 30 2.3.1 Example Revisited: State Updates 33 2.4 Strong Monads 36 iii Table of Contents 3 W a d l e r ' s M o n a d s 39 3.0.1 The Maybe Monad 39 3.0.2 Definition of a Monad 40 3.1 Examples 42 4 E q u i v a l e n c e 51 4.1 Preliminary Connections 51 4.1.1 Comparative Motivations for » = , j o i n , and .* . . . . 54 4.2 Monad Laws 55 4.2.1 Alternate Laws 55 4.2.2 Law Equivalence 58 4.3 Concluding Connections 61 4.3.1 List in Translation 61 4.3.2 Distributive Laws 62 B i b l i o g r a p h y 69 iv Acknowledgements I would like to acknowledge my supervisor, John MacDonald, for his guid-ance, encouragement, and kindness. In addition, I am grateful to my second thesis examiner, Kee Lam, for his helpful suggestions. Finally, I would like to acknowledge Steve Wolfman and the ELMers for their enthusiastic and enlightening dinnertime discussions. Dedicat ion To Leonard, Art & Adam. Chapter 1 Introduct ion We begin with a brief overview of the key concepts from category theory that wil l be needed to investigate monads. Notably, we wi l l not provide an independent section pertaining to background Haskell material, choosing instead to offer relevant introductory concepts and syntax within the con-texts they are needed. We refer the Haskell-interested reader to [4] for an excellent introduction. 1.1 Background A monoid (M, -,e) is a set M together with an associative binary op-eration • : M x M —> M and identity element e £ M, such that Vm 6 M,e • m = m = m • e. The properties of this familiar algebraic construct can be expressed via commutative diagrams—which abound in category theory—as follows. Let p\ : M x M —> M and p2 : M x M be projections defined by: Vm,m ' € M, p\(m,m') = m = p2{m',m). We define a monoid M to be a set M together with functions fi : M x M —> M and n : 1 —> M, where 1 = {e} with e € M, such that the following diagrams commute: MxMxM-^^MxM i x M - ^ M x M ^ M x l lixl M x M pi M M M M The theoretical settings in which we work are categories: the struc-tures central to the study of category theory. A category C is a 6-tuple (OQ, AC, dom, cod, o, id), where: •. Oc and Ac are sets of objects and morphisms (or arrows), respectively; • dom and cod are functions-that assign to each morphism f € A objects dom/ and cod/, the domain and codomain of /, respectively. For an arrow / with dom/ = a, cod/ = b, we write / : a —> b; 1 Chapter 1. Introduction • id is a function that assigns to each object c G Oc an identity morphism i d c G Ac, with i d c : c —> c satisfying the (standard algebraic) identity law; • o is an associative binary operation that assigns to a pair of morphisms (/ : a —+ b, g : b —> c) G Ac x Ac a morphism 5 o / : a —> c. The associativity of morphism composition can be used to prove the following useful (albeit, simple) property of commutative digrams. Theorem 1.1.1. Let A,B,C,D,E,F G Oc and f,g,h,q,r,s,t G Ac, with domains and codomains as shown below. If the squares ABED and BCFE are commutative, then the outer rectangle ACFD, is also commutative. B C D E Proof. The commutativity of the left-hand square implies g°q = sof, and the commutativity of the right-hand square implies h o r = t o g. Thus, by the associativity of o, we have h o (r o q) = [h o r) o q = (t o g) o q = t o (g o q) = t o (s o / ) = (t o s) o / . • Many constructions in category theory capture set-theoretic ideas with the language of objects and arrows. A n example that we wi l l encounter in the context of computational semantics is that of a terminal object, which is the category-theoretic generalization of a singleton set. A n object 1 in a category C is a terminal object if for every C-object c there is exactly one arrow from c to 1 in C. Any two terminal objects in a category C must be isomorphic because if 1 and 1' are both terminal objects then there must exist C-arrows / : 1 —> l ' and g : l1 —> 1. Since 1 and l ' are terminal, idi and idj/ are the only arrows from 1 —> 1 and 1' —> 1', respectively. Thus, fog = idi , 0 o / = idi' and so / : 1 = 1'. A functor is a structure-preserving map between categories. Explicitly, a (covariant) functor F : C —» V is a function that satsfies: • Vc G Oc, 3d G Ov, with F(c) = d; • V/ : c i -> c 2 G A c 3F(/) : F ( c i ) -> F ( c 2 ) G Av, such that: i. Vc G Oc, F ( i d c ) = i d F ( c ) ; i i . F(g o /) = F(g) o F(f), whenever g o f e Ac is defined. 2 Chapter 1. Introduction T h e r e are several functors that wi l l provide' nice examples i n our s t u d y of m o n a d s . 1. F i r s t , let F : Set —> Grp m a p a set X G Set to the free group F r e e ( X ) generated b y the elements of X. N o t e that any func t ion between sets X a n d Y c a n be v iewed as a m a p between the generators of F r e e ( X ) a n d those of F r e e ( y ) , w h i c h extends to words i n X, preserves c o m p o s i -t i o n a n d equivalences, a n d is the un ique ly d e t e r m i n e d h o m o m o r p h i s m between these groups w i t h these extension propert ies . T h u s , we c a n define F to be the free group functor b y set t ing F(f) = hf, where / is a n a r b i t r a r y func t ion between objects i n Set a n d hf is the corre-s p o n d i n g group h o m o m o r p h i s m as descr ibed. 2. W e define another functor U : Grp —> Set to be the forgetful functor, w h i c h m a p s a group (G, •) to its u n d e r l y i n g set of elements a n d a g r o u p h o m o m o r p h i s m to the correspond ing func t ion between the u n d e r l y i n g sets. 3. T h e power set functor V : Set —> Set is defined b y m a p p i n g a set to its power set a n d a func t ion / : X —> Y between sets to the func t ion V(f) : V{X) -> V(Y) i n d u c e d b y t a k i n g / - i m a g e s of sets i n V(X). G i v e n functors F,G : C —» T>, a natural transformation r : F —> G is a m a p p i n g w i t h the p r o p e r t y that V a G Oc, 3Tq G A-r> such that V / : a —+ b G Ac, we have T(, O F(f) — G(f) o r a . Intuit ively, r c a n be thought of as a m a p that uses the s tructure of T> to slide F - d i a g r a m s onto G - d i a g r a m s . T h e s i tua t ion is descr ibed b y the fol lowing d i a g r a m , i n w h i c h the square is c o m m u t a t i v e : V Fa Ga Ff Gf Fb Gb. 1.2 Composition of Natural Transformations T h e def init ion of a m o n a d includes compos i t ions of n a t u r a l t r a n s f o r m a -tions. T h e r e are two ways that n a t u r a l t rans format ions c a n be c o m b i n e d 3 Chapter 1. Introduction (depending o n the d o m a i n a n d range functors of the n a t u r a l t rans format ions involved) , w h i c h we now introduce . 1.2.1 Vertical Composition G i v e n any three functors F,G, H : C a : F —> G, T : G —> H, v iewed vert ica l ly as T> a n d n a t u r a l t rans format ions V, H it is easy to see how to define a compos i te n a t u r a l t r a n s f o r m a t i o n r • a : F —> H. F o r any object c £ C, there exist "D-arrows ac : Fc —> Gc a n d T C : Gc —> He (the c components of the g iven n a t u r a l t rans format ions ) . W e define ( r • a)c = r c o ac to be the c o m p o n e n t s of the vert ica l c o m p o s i t i o n of n a t u r a l t rans format ions a a n d r . T o show that such p r o p o s e d c o m p o n e n t s for r • a indeed compr i se a n a t u r a l t rans format ion , we must show c o m m u t i v i t y of the outer rectangle i n fol lowing d i a g r a m , for / : b —> c i n C: Fc Ff Fd Gc Gf Gd 4 He Hf + Hd. T h e respective natural i t ies of a a n d T i m p l y the c o m m u t a t i v i t y of the left a n d r ight squares, a n d the c o m m u t a t i v i t y of the outer rectangle i m m e d i a t e l y follows f r o m T h e o r e m 1.1.1. 1.2.2, Horizontal Composition W e now define another type of c o m p o s i t i o n for n a t u r a l t ransformat ions . C o n s i d e r functors F,G : B —> C, H,J:C—^T>, a n d n a t u r a l t rans format ions a : F —> G, r : H - A J , v iewed hor izonta l ly as F H > > G J Deta i l s are as follows: for any S -objec t b, there exist C-objects Fb a n d Gb, a n d C - a r r o w : Fb —> Gb. W e have two ways b y w h i c h we c a n m a p 4 Chapter 1. Introduction these items to V; namely , v i a H or J. T h u s , we have the fol lowing d i a g r a m in V, w h i c h is c o m m u t a t i v e by the n a t u r a l i t y of r : HFb JFb H<7b Jcrb HGb -^*-> JGb T h a t is, B i" C H T> followed by B H C I ' D equals B H C I ' D followed by B {« C V. W e define the components of the hor i zonta l c o m p o s i t i o n of a a n d r to be the c o m p o s i t i o n of arrows f rom HFb to JGb as s h o w n in the above d i a g r a m ; expl ic i t ly , ( r o cr)b = TQb 0 H&b = J^b 0 TFb- T o verify that these c o m p o n e n t s do comprise a n a t u r a l t r a n s f o r m a t i o n , we must show that the fol lowing d i a g r a m c o m m u t e s for / : b —> c i n B: H F b i l^K job HFf JGf HFc JGc. B u t g iven the def in i t ion of the components for ( r o o~)c, this d i a g r a m c a n be b r o k e n into two squares: HFb -^_» HGb H F f \ HFc JGb HGf JGf Hcrc HGc TGc JGc. Since a is n a t u r a l , we have Gf o Cb = o~c ° Ff. B y m a p p i n g these objects a n d arrows to D w i t h the functor H, we establ ish the c o m m u t a t i v i t y of 5 Chapter 1. Introduction the le f t -hand square. Since Gf : Gb —> G c is a C-arrow, the n a t u r a l i t y of r impl ies the c o m m u t a t i v i t y of the r i g h t - h a n d square. T h u s , the above rectangle commutes . A Note on Notation W e take this o p p o r t u n i t y to emphas ize a no ta t iona l usage of key i m p o r t in the s t u d y of monads . C o n s i d e r the fol lowing arrangement: F > F' L e t b £ 0 B - T h e n , pb : Fb -> F'b is a n arrow i n C a n d T(pb) : TFb -+ TF'b is a n arrow i n V. W e thus let Tp, : TF -+ TF' denote the n a t u r a l t r a n s f o r m a t i o n w i t h such P - a r r o w s as its components : {Tp)b = T(pb). W e thus recognize that Tp is an example of hor i zonta l c o m p o s i t i o n . Specifically, Tp, = IT 0 p, where 1 l r is the ident i ty n a t u r a l t r a n s f o r m a t i o n on the functor T : F T > > F' T N e x t , consider the arrangement: T B -^-> C~[^V. > T> A g a i n , let b £ 0 B - T h e n , Fb £ C a n d vFb • TFb -* T'Fb is a n arrow in V. W e let vF : TF —+ T'F denote the n a t u r a l t r a n s f o r m a t i o n w i t h components g iven precisely by the F - i m a g e components of v : {vF)b — vp^. T h i s is another example of hor i zonta l c o m p o s i t i o n , where vF = v o\F ; F T > > F T1 T h u s , whi le the s y m m e t r y of such notat ions as 'pT' a n d 'Tp' reflects the conceptua l s y m m e t r y of the hor i zonta l compos i t ions discussed, care must be taken w h e n a p p l y i n g these m a p s due to the relat ively a s y m m e t r i c nature of the component -wise formulat ions of the n a t u r a l t rans format ions . 6 Chapter 1. Introduction 1.3 Monads in Category Theory 1.3.1 Definition W e now give the first f ormula t ion of the concept t h a t is of p r i m a r y i n -terest to us. In category theory, a m o n a d in a category C is a m o n o i d in the category of endofunctors of C , w i t h the b i n a r y opera t ion be ing functor c o m p o s i t i o n a n d the uni t element be ing the ident i ty endofunctor . W e c a n present the def ini t ion of a m o n a d d i a g r a m m a t i c a l l y us ing c o m m u t a t i v e d i a -grams like those g iven prev ious ly in the d i a g r a m m a t i c def init ion of a m o n o i d . T h a t is, g iven functors IQ,T,T2, T 3 : C —> C a n d n a t u r a l t rans format ions r\ : IQ —+ T, fi : T2 —> T , the 3-tuple (T, rj, fi) is a monad in C if the fol lowing d i a g r a m s c o m m u t e : T 3 f l T > T2 IT ^ > T2 < T v TI I'- ll T2 M > T T ' T = T. F o r ( n o t a t i o n a l brevity , we wi l l often denote a m o n a d (T, n, //,) b y its u n d e r l y -ing endofunctor T . In a d d i t i o n , we wi l l refer to the equat ions c o r r e s p o n d i n g to the left a n d r ight d i a g r a m s above as m o n a d laws 1 a n d 2, respectively. 1.3.2 Examples 1. W e beg in by w o r k i n g t h r o u g h the details of a s imple example . L e t (M, •, e) be a m o n o i d a n d T : Set —> Set a functor defined by TX = M x X for any X £ Set. Define the n a t u r a l t rans format ions fix '• M x M x I - > M x I b y ^ ( ( m , n,x)) = (m-n,x) a n d rjx : X —> M x X by Vx{x) = (e,a;). T h i s gives the fol lowing s i tuat ion: r 2 Set- ' Set > X T ( T 2 X ) T ( T X ) (l,m,n,x) i—> (l,m • n,x) TX T2(TX) i l r x » T ( T X ) (l,m,n,x) t—» (I • m, n, x). 7 Chapter 1. Introduction We can thus demonstrate the commutativity of the first defining dia-gram for a monad by showing that elements are mapped via pertinent paths in the same way.: M x M x M x X illF)x> M x M x X {TlAx M xM xX tlX f-X M x X (l,m,n,x) >lTX > (l-m,n,x) T(Wf) MX (l,m-n,x) ^x > (l-m-n,x). Similarly, for monad law 2 we have the situation: Set 1" Set X T(IX) TiTX) (m,x) i—> (m, e,x) TX I(TX) T{TX) (m,x) <—> (e,m,x). These mappings give rise to the following verification of commutativ-ity: TX T2X TX TX t*x : TX TX (m,x) > (e,m,x) (m,e,x) < (m,x) I'X fix (e -m,x) = (m • e,: 8 Chapter 1. Introduction There fore , ( T , n, JJL) is a m o n a d . L e t (P, <) be a p a r t i a l l y ordered set. If we consider the elements of P to be objects , a n d the re lat ionship x < y where x, y G P to be equivalent to a n arrow f r o m x to y, t h e n P c a n be v iewed as a category. B y the def ini t ion of a poset a n d t h a t of arrows in the category P, there c a n be at most one arrow between any two objects . T h u s , any endofunctor defined on P is a m o n o t o n i c funct ion . L e t T be such a functor a n d observe that the condi t ions descr ib ing the n a t u r a l t rans format ions rj a n d fi for a m o n a d are equivalent to the condi t ions x < Tx a n d T(T(x)) < T ( x ) , V x G P. B y a p p l y i n g T to the first of these inequal i t ies , we have T(x) < T(T(x)). C o m b i n e d w i t h the second inequal i ty a n d the def ini t ion of a poset, we have T(x) — T{T(x))\ that is, a m o n a d o n a poset P is a closure operat ion . R e c a l l the definit ions of the free group functor F : Set —> Grp a n d the forgetful functor U : Grp —» Set. B y c o m p o s i n g these functors , we have a n endofunctor T = U o F : Set —> Set, w h i c h m a p s a set X to the u n d e r l y i n g set of F r e e ( X ) . W e define a word in X to be a s tr ing of finite l ength of elements f rom XuX-1, where X~x = { x - 1 | a ; G X} is a set of formal inverses of elements i n X. T h e n TX is the set of equivalence classes of words m a d e u p of symbol s x a n d x _ 1 for al l x G X—equivalent under de le t ion of s tr ing segments ' r a - 1 ' a n d ix~1x,' for any x G X. If w is a w o r d i n X, we denote its equivalence class by [w] a n d typ ica l ly refer to the entire "equivalence class of the w o r d w" as s i m p l y the "word w." If we define rjx by sending x i—> [x] a n d fix b y the conca tena t ion of words i n TX, t h e n T is a m o n a d . N o t e that a w o r d i n T2X is c o m p o s e d of words f r o m TX, a n d concatenat ing words amounts to r e m o v i n g brackets , w i t h our no ta t ion . F o r example , if [z _ 1 j /a;] , G TX, then [ [ 2 _ 1 yx ] [a ; _ 1 y ] ] G T2X a n d ^jv([[z _ 1 ya;][a: _ 1 j /]]) = [z~lyxx~1y] = [z~lyy]-W e prov ide i l lustrat ions of the c o m m u t a t i v i t y of the m o n a d d iagrams . F o r m o n a d law 1: [[[xy][zxx}[y]][[x-'}[y]]} J^U [{xy\[zxx][y}[x-'}[y}\ PX [[xyzxxy}[x 1y}] > l x > [xyzxxyx 1y] 9 Chapter 1. Introduction N o t i c e that the c o m m u t a t i v i t y of this d i a g r a m c a n be s u m m a r i z e d by s ta t ing that the remova l of inner brackets c a n be done i n either order. F o r m o n a d law 2: TX TX T2X * P-x -. TX TX TX [xyz' - l i VTX [[xyz'1]] [[xyz-1]] [xyz-1] [xyz v-x nx - H - [xyz - H W h i l e the above d i a g r a m appears rather unenl ighten ing , it is inter-est ing to note that the m a p p i n g a long the u p p e r left arrow adds the outer set of brackets , whi le m a p p i n g v i a the u p p e r r ight arrow adds the inner set. T h e power set m o n a d is descr ibed by the power set functor a long w i t h n a t u r a l t rans format ions rj a n d fi, defined as follows. F o r any x € X,T]x{x) = {x}. L e t L be a set whose elements are subsets of X . Def ine \xx to be the m a p w h i c h takes L to the u n i o n of the elements of L. N o t e that fix{L) C X, as is necessary. T h i s example looks s imi -lar to that preceding , b u t there are key differences w h i c h we i l lustrate in the example below. Specifically, z^'s def ini t ion involves t a k i n g the u n i o n of subsets; therefore, elements that are m e m b e r s of more t h a n one subset wi l l show u p as on ly a single element in the u n i o n . In the case of s t r ing concatenat ion , any 'repeated' e lement is not condensed into a single copy of that element, b u t cancel lat ions c a n occur i n ac-c o r d w i t h the g iven equivalence re la t ion of w o r d reduc t ion . F u r t h e r , under the o p e r a t i o n of u n i o n , the order of elements in the resultant set is u n i m p o r t a n t ; b y contrast , the order is i m p o r t a n t i n s tr ing con-catenat ion . C o m p a r e the d iagrams be low to those of the preced ing example . 10 Chapter 1. Introduction {{{x,y}{z,x}{y}}{{x-i}{y}}} J^U {{x,y}{z,x}{y}{x^}} T(Mx) MX {{x,y,z}{x~l,y}} >XX » {x,x~l,y,z} {x,y,z^} ™U { { W 1 } } { { W 1 } } { W 1 } ^ I MX iix {xjy,z^} = {x,y,z-1}. 1.4 Category Theory in Haskell T h e m a i n focus of our s t u d y is the a p p l i c a t i o n of category theory to the p r o g r a m m i n g language Haske l l . H a s k e l l is a p o l y m o r p h i c a l l y t y p e d , p u r e l y func t iona l language. In the a p p r o p r i a t e contexts , we w i l l define each of these terms. W e b e g i n w i t h a brief d iscuss ion of the f u n d a m e n t a l connec t ion between category theory a n d the funct iona l p r o g r a m i n g p a r a d i g m . 1.4.1 Ftinctional Languages and the A-Calculus T r a d i t i o n a l approaches to the des ign a n d i m p l e m e n t a t i o n of p r o g r a m -m i n g languages have been centred a r o u n d the idea of a variable: a modi f iable assoc iat ion between a n a m e a n d values [9]. S u c h languages are cal led im-perative because p r o g r a m s based o n this concept are c o m p r i s e d of sequences of c o m m a n d s . E a c h c o m m a n d usual ly consists of the eva luat ing of a n ex-press ion a n d ass igning the r e t u r n value to a variable's name . M o r e o v e r , a c o m m a n d found at any step of the c o m p u t a t i o n sequence c a n be dependent o n variables u s e d — a n d potent ia l ly m o d i f i e d — i n preced ing c o m m a n d s . In this way, values c a n be passed d o w n t h r o u g h a c o m m a n d sequence, a n d the value assigned to a n a m e in one c o m m a n d can be rep laced b y a new value in a subsequent c o m m a n d . T h e s e ideas i m p l y that the order of c o m m a n d execut ion typ ica l l y affects a c o m p u t a t i o n result . In contrast , the functional p r o g r a m m i n g p a r a d i g m is founded o n s truc-t u r e d funct ion calls, a func t ion ca l l be ing a func t ion n a m e followed by a list of arguments i n parentheses. P r o g r a m s i n func t iona l languages consist of nested func t ion calls or, i n other words , are compos i t ions of funct ions. 11 Chapter 1. Introduction As such, function names behave as they do in the context of mathematical functions: they are formal parameters of other functions and are associated with values through calls to functions that have been given actual values. Once an association between a function name and a value has been made, it cannot be modified. In summary, a functional program is a single expression and executing such a program corresponds to evaluating the expression. This mathematical approach offers the following advantages to program-ming with functional languages [14]: • Declarativeness — The order of function execution need not be speci-fied by the programmer but rather can be inferred by the system based on relations that must be satisfied by evaluated functions. • Referential Transparency — If two functions f and g produce the same values when given the same arguments, then any occurence of f can be replaced by g without changing the meaning of the program. • Higher-Order Functions — Functions can accept functions as argu-ments and can output new functions. • Polymorphism — Individual algorithms can be written in such a way that they apply to several types of input (in certain cases, this is also referred to as function overloading). This is somewhat akin to saying that we can define the "same function" on different domains: an idea which makes mathematical sense in the context of a function being defined on a set and certain supersets. The most obvious candidate for a polymorphic function is the identity function. We can define the identity function for any input a by returning a unchanged. It is often more convenient to think of a single, "umbrella" identity function than to define a new identity function for each type of input being considered. Thus, in Haskell for example, the identity function id is a polymorphic function that accepts an input of any type and returns a copy of this input. Many approaches to the semantics of polymorphic type systems are founded on the typed X-calculi; in particular, Haskell is based on A-calculus. The two core concepts of the A-calculus are those of function abstraction and application. The former refers to the generalization of expressions via the introduction of names, and the latter refers to the assignment of partic-ular values to names as a means to evaluate generalized expressions [14]. In this work, we will not provide a comprehensive introduction to or detailed explanations of the A-calculus. We will, however, include some references to the A-calculus on occassion, with aims to benefit those already familiar and 12 Chapter 1. Introduction entice unfamiliar readers to learn more independently. Formally, a typed A-calculus is an axiomatic system consisting of terms, types, variables and equations. For every term a in a typed A-calculus, there is a corresponding primitive type A called the type of a, with the correspon-dence denoted by a 6 A. Since Haskell's type system will be of recurring importance throughout our study, we cite the A-calculus axioms pertaining to term- and type-formation here as general background information [2] (for the 11 other rules necessary to define a typed A-calculus, also see [2]): • There is a unit type 1. • There is a term * of type 1. • If A and B are types, then there exists a product type A x B and a . functional type [A —> B], where [A —> B] denotes the set of functions from A to B. • If a and b are terms of type A and 73, respectively, then there is a term (a, b) of type Ax B. • If c is a term of type Ax B, there are terms proj1(c) and proj2(c) of type A and B, respectively. • If a is a term of type A and / is a term of type [A —> B\, then there is a term / a of type B. • For each type A, there is a countable set of terms xf of type A called variables of type A. • If x is a variable of type A and 4>(x) is a term of type B, then ^x€A<t>{%) € [A —• B\. Here, cfi(x) denotes a term </> that might contain the variable x. In addition, we define a free variable to have the following properties: If x is a variable, then x is free in the term x. If an occurrence of x is free in either of the terms a or b, then that occurrence of x is free in (a, b). If x occurs freely in either / or a, then that occurrence of x is free in / a. Finally, there exists at least one occurrence of x that is not free—called bound—in Xx4>{x). Note that the last item in the above list offers a notation for defining functions in the A-calculus. Another notation that is commonly found in the literature is Ax : <$>{x), which would be equivalent to Xxcf)(x) in the above notation. It can be shown that it is possible to define every computable function using' function abstraction and application of the A-calculus. This means that the A-calculus is a theoretical, universal machine code for programming languages. It is further suited for describing programming languages in that its purely mathematical nature facilitates constructing proofs about 13 Chapter 1. Introduction the language b e i n g descr ibed. Las t ly , the s impl i c i ty of the A-calculus makes its i m p l e m e n t a t i o n i n languages re lat ively easy [9]. 1.4.2 Cartesian Closed Categories T h e A-ca lculus provides the first large l ink between funct iona l p r o g r a m -m i n g languages a n d category theory. T h e connec t ion is i n the correspon-dence between t y p e d A-ca lcu l i a n d cartes ian closed categories. A category C is a cartesian closed category if it satisfies the fol lowing ax ioms [2]: ' • T h e r e is a t e r m i n a l object 1. • F o r every pair of C-objects A a n d B, there exists a C-object A x B, the p r o d u c t of A a n d B, w i t h project ions p\ : A x B —> A a n d p2 • Ax B -> B. • F o r every pa ir of objects A a n d B, there exists a n object [A —> B] a n d a n arrow eval : [A —> B] x A —+ B w i t h the p r o p e r t y that for any arrow / : C x A —> B, there is a un ique arrow A / : C —> [A —> B] such that the compos i te arrow C x A [A -> B] x A ^ B is equa l to / . W i t h respect to the t h i r d property , we note that the exponent ia l [A —> — ] is a r ight adjoint to — x A : C —-> C a n d that eval is the couni t of this a d j u n c t i o n . N o t e also that the c o m p o s i t i o n of a functor F w i t h its r ight adjoint U determines a m o n a d ( T , r/, fj.) w i t h T — UF. A A- theory is a t y p e d A-calculus that is ex tended w i t h some a d d i t i o n a l terms, types , or equivalences between expressions [13]. It c a n be shown that the concepts of t y p e d A-calculus a n d cartes ian closed category are equivalent in the fol lowing sense: (i) G i v e n a A- theory L, we c a n cons truct a cartes ian closed category i n w h i c h each object corresponds to a type i n L a n d i n w h i c h a n arrow between objects A a n d B is a n equivalence class of terms of type B w i t h one free var iable of type A; (ii) g iven a cartes ian closed category C that is a s sumed to have finite p r o d u c t s , we c a n define a t y p e d A-ca lculus w h i c h has as types the objects of C. In p a r t i c u l a r , the types requ ired b y the first a n d second t y p e d A-ca lculus ax ioms g iven above are the objects 1, A x B a n d [A —> B). N o t e that the equivalence p r o o f shows the connec t ion between the nota-t ion used for funct ions in the A-calculus a n d the choice of the func t ion n a m e 14 Chapter 1. Introduction Xf i n the last l isted i t em. In fact, / a n d Xf are s i m p l y c o r r e s p o n d i n g m a p s u n d e r the a d j u n c t i o n ( - x A, -) = (-, [A -»-]): C x C —> Set. W e refer the reader to, for example , [2] for a vers ion of the equivalence proof. 1.4.3 Types in Haskell A n y p r o g r a m m i n g language has a means by w h i c h to group s imi lar k inds of values a n d expressions. A syntact ic m e t h o d for organ iz ing a n d imple -m e n t i n g levels of abs trac t ion in p r o g r a m s is cal led a type system, w i t h the cons tra ined d a t a values referred to as d a t a types or types. T y p i c a l examples of types in p r o g r a m m i n g languages inc lude p r i m i t i v e types (such as inte-gers, f loat ing po int numbers a n d characters) , tuples , lists, funct ion types a n d abstract d a t a types. H a s k e l l is a s tat ica l ly t y p e d p r o g r a m m i n g language. T h i s means that every expression i n H a s k e l l is assigned a type , a n d t y p e checking is c o m p l e t e d as par t of the compi l e - t ime , rather t h a n r u n - t i m e , process. A s a result , a compi l e - t ime error wi l l be generated if any func t ion i n the p r o g r a m is g iven a n argument of the w r o n g type . T h i s is he lpful i n l oca t ing a n d r e d u c i n g the n u m b e r of p r o g r a m m i n g errors (bugs) that c a n occur w h e n p r o g r a m m i n g . T h e type s ignature of a funct ion is a speci f icat ion of its argument a n d r e t u r n types. F o r example , the func t ion t o U p p e r is a H a s k e l l func t ion that takes a character as i n p u t a n d re turns the c o r r e s p o n d i n g u p p e r case char-acter as o u t p u t . W e denote the type s ignature of this func t ion w i t h the (Pre lude) n o t a t i o n t o U p p e r : : C h a r -> C h a r . T h e t y p e s ignature of a func t ion f of n variables is denoted b y f : : t i -> t-2 -> • • • -> t n -> r , where t j , . . . t n are the (possibly dist inct) i n p u t types a n d r is the r e t u r n type . E q u i v a l e n t l y , we c a n t h i n k of f as a func t ion that accepts k arguments t j , . . . tfc a n d returns a func t ion of n - fc arguments t ^ + i , . . . tn, w i t h the o u t p u t type of the r e t u r n func t ion of course be ing r . A func t iona l p r o g r a m m i n g language c a n be c o n s t r u e d as a category if we view the types of the language to be the objects a n d the funct ions de-fined between types to be the m o r p h i s m s . A s a s imple example , consider a funct iona l language w i t h p r i m i t i v e types B o o l h a v i n g one of the values true or false C h a r characters F l o a t floating-point numbers : real n u m b e r s w i t h no fixed n u m b e r of digits before or after their d e c i m a l po ints I n t (f ixed-precision) integers, a n d p r i m i t i v e funct ions 15 Chapter 1. Introduction Int F l o a t • * Int —> Int :: F l o a t —> F l o a t : Int —> Bool greatest integer less than or equal to input identity (returns an identical copy of input) increment an integer by 1 increment a floating-point number by 1 test for zero square a number convert an integer to a floating-point number convert a lower-case character to upper-case. Clearly, the polymorphic function i d will correspond to the identity mor-phism for any object in the category. Excluding identity and composition arrows, the category corresponding to the above data would look like: f l o o r :: i d :: * -in c - i n t :: incpioat i s z e r o : Float Float SV-: Int Int t o F l o a t :: Int -> F l o a t toUpper :: Char —•> Char mc I n t, sqr Int i s z e r o Char f l o o r toUpper t o F l o a t Bool incpioat, sqr Fl o a t We can neatly display the commutativity of certain operations in a lan-guage using commutative diagrams. For example, Int > Int toFloat toFloat F l o a t > F l o a t inCFloat summarizes the equivalence between incrementing an integer and then con-verting it to a floating-point number with converting an integer to a floating-point number and incrementing the result. 16 Chapter 1. Introduction O v e r l o a d e d F u n c t i o n s a n d I m p l i c i t Conve r s i on s There is an interesting connection between the transformations whose commutativity is considered semantically valid in a given language and the use of overloading in that language. Overloading is a case of type poly-morphism in which an operator has a different implementation depending on the type of its arguments. The main purpose of overloading is to in-crease the intuitiveness or convenience of a language's syntax. For exam-ple, it would be disheartening if programmers had to distinguish between two operations (+i n t ) and (+Fioat) when trying to add two "numbers." The same idea is true for the sqr function shown in the category above (note the overloading implemented there). Yet, the action that a compiler should take when faced with an expression such as l e t x i n F l o a t = i + j , where i and j are integers is not obvious, the two possibilities be-ing x = t oF l oa t ( i ) + F i o a t ' t o F l oa t ( j ) and x = t o F l o a t ( i + i n t j ) . Of course, from a mathematical standpoint these options are equivalent, which sug-gests that perhaps a compiler should be indifferent to the interpretation of these expressions as well. This has motivated approaches to formalizing proper designs of overloaded functions and implicit conversions, so that their commutivity upon insertion into a compiler is semantically irrelevant. In the case of i nc , sqr or (+) discussed above, the 'semantic commu-t iv i ty ' that arises does so because Z C K. In our programming context, this means that data of type I n t can be implicit ly converted to that of type F l o a t . In many cases, an implicit conversion function corresponds to the inclusion function between appropriate types. This mathematical analogy does not nicely extend to all cases of implicit conversions, however. For example, it may be useful to consider integer expressions as a type; that is, a mathematical expression in which all terms are integers (for example, x + y, where x and y are of type Int). Here, the integer variables (for example, x, where x is of type Int) can be viewed as a subtype of the integer expres-sions, when viewing an integer variable as a subtype of integer expressions. The difficulty in defining a "set of integer expressions" prohibits a natural extension of the inclusion analogy for these types. To generalize the notion, we briefly introduce Reynold's approach of con-sidering an alternate construction of a category representative of a functional language [15]. We again let the objects of the category be the types of the language, but we use them to form a partial order in which the arrows be-tween types correspond to valid implicit conversions. As an example, we use the same objects as in the type category figure above, along with a 'univer-sal ' object Value. This object is a contrived maximum for the type partial 17 Chapter 1. Introduction order, it be ing denned as a super type of all other types i n the category. W i t h this, the p a r t i a l order 0, w o u l d look like: V a l u e Char Float Bool Int W e define a carrier C : Cl —> Set to be a functor that m a p s a type t £ to the set of values of type t. T h e m o r p h i s m s t < t' in $1 are m a p p e d to impl i c i t convers ion funct ions between sets of types , whose b e h a v i o u r is res tr ic ted b y the d e n n i n g propert ies of the functor C. E x p l i c i t l y , the def ini t ion of a functor C : il, —•> Set o n a p a r t i a l order f i is a m a p that satisfies: (a) C{t < t') e H o m ( C ( t ) , C ( t ' ) ) (b) C(t <t) = Ic{t) (c) If t < t! a n d *' < t", then C(t < t') = C{t' < t") o C(t < t1). L e t C2 : fl2 —> Set2 denote the functor denned on types t\, 2^ by C 2 ( t i , i 2 ) = ( C ( t i ) , C ( * 2 ) ) a n d o n arrows t\ < t[, t 2 < t'2 by C\h < t[,t2 < t'2) = (C(h < * i ) , C ( t 2 < t'2)). L e t x 2 : Set2 —> Set denote the functor denned on sets S i , ^ b y x2{Si,S2) = S i x 5 2 • a n d on set funct ions /1, / 2 b y x\h,f2) = h X / 2 . In the context of impl i c i t conversions, we are interested i n conver t ing a type t\ into another type t 2 , where t\ < i 2 . F o r example , we might consider the convers ion f r o m integers to real n u m b e r s or f r o m a n integer to a n integer 18 Chapter 1. Introduction expression (for the latter, consider converting the integer 1 to the expression '1' that evaluates to the integer 1). Therefore, from a categorical standpoint, we always assume that the partial order fi has a largest (catchall) element as described above-call it Value-that semantically encompasses all other types. This is the terminal object of the partial order. We thus let T$ • fi2 —> fi denote the functor denned on any two types h,t2 by r d ( i i , t2) = m&x{ti,t2} and on arrows t\ < t[,t2 < t'2 by r*(*i < t[,t2 < t'2) = (rs(h,t2) < r ^ t i . t a ) ) . The compiler-recognized commutivity of overloaded functions and im-plicit conversions can then be expressed by stating that for any types t\,t2 with t\ < t2 an overloaded function 7,5 is a natural transformation between 9 c2 2 £ 2 9 r<5 c the composite functors fi —^> Set —> Set and fi —> fi — > Set: x2oc2(t1:t2) ^ C o r ^ , ^ ) x2oC2(t1<t[,t2<t'2) Cors t2<t'2) x2oC2(t'1,t'2) ——* CoTs^tti 7*(ti.*2) The preceding discussion regarding the overloaded function (+)—or, in our new notation, 7+—can now be understood as an instance of the above diagram. If we let tx = t2 = Int, then C2{tut2) = (C{tx),C(t2)) = (C(lnt) ,C(Int)) and x2 o (C(lnt), C(Int)) = C(Int) x C(lnt). Further, in the partial order category there is an identity arrow Int < Int, which corresponds intuitively to the idea that any value of type Int can be implic-itly converted (trivially) to a value of type Int. Thus, T^Int, Int) = Int, and C o r<5(Int, Int) = C(lnt). Similar derivations are achieved by setting t'x — t'2 = Float, and defining the conversion function C(Int < Float) to be t o F l o a t gives rise to the following diagram: C(Int) x C(Int) — — • — C ( I n t ) toFloatxtoFloat toFloat C(Float) x C(Float) > C(Float). 7+'(Float, Float) 19 Chapter 1. Introduction 1.5 Haskell 1.5.1 Haskell's Type System Type Classes A s prev ious ly ment ioned , a n over loaded funct ion is a func t ion that c a n accept parameters of m o r e t h a n one type . T h i s is somewhat p r o b l e m a t i c for a stat ic t y p e checker, since there c a n be a m b i g u i t y as to w h i c h types a g iven o p e r a t i o n is defined for. C o n s i d e r first the ident i ty funct ion . T h i s func t ion c a n accept arguments of a l l types. In Haske l l , its t y p e s ignature is i d : : a -> a, where a is a type variable that c a n s t a n d for any defined type . A s such , a m b i g u i t y is avo ided a n d compi l er compl i ca t ions need not arise. However , consider the a d d i t i o n funct ion . W h i l e it is des irable for the func t ion (+) to be defined for types such as I n t or Float, it s h o u l d not be defined for, say, Bool or Char. T h u s , a type s ignature such as (+) : : a -> a -> a is too general for the over loaded o p e r a t i o n we have i n m i n d . T h e sy s t em used i n H a s k e l l to address this issue is that of t y p e classes. A type class is a set of func t ion (or constant) names , together w i t h their respective types , w h i c h mus t be g iven definit ions for every type that is to be long to the class. In other words, it is a set of constraints for a type variable . Specif ic definitions of the funct ion names of a type class are cal led methods. O n c e each of the m e t h o d s c o r r e s p o n d i n g to the func t ion names of a type class has been given, a n instance of the class has been defined; that is, the type of a n instance instance of t y p e class Class is instance : : Class. F o r example , the class Eq is in tended to be a class for types for w h i c h it makes sense to test for equal i ty or inequality. T h e class dec lara t ion is g iven b y c l a s s Eq a where (==), (/=) a -> a -> Bool T h e types Char, Double, Float, Int a n d Integer are instances of Eq, where each of t h e m provides definitions for the m e t h o d s ( = ) a n d ( /=) . N o w , the d o m a i n or range types of a funct ion c a n be cons tra ined to a type class that suits the desired boundedness of the p o l y m o r p h i s m . F o r example , the type of (+) in H a s k e l l is correct ly w r i t t e n as (+) : : Num a => a ->. a -> a, where Num is a class w i t h instances Double, Float, Int a n d Integer, a n d => denotes the res tr ic t ion of the type var iable a to the Num class. 20 Chapter 1. Introduction The Functor Type Class L e t [x] denote a list of elements of type x. In the P r e l u d e , a func t ion map is defined w i t h s ignature map : : (x -> y) -> [x] -> [y] . Its ac t ion is to accept a func t ion a n d a list, a n d o u t p u t the list of image elements under the g iven funct ion; that is map f [ x l , x2, . . . ] = [f (xl) , f (x2) , . . . ] . F o r example , map negate [1,-2,3] = [-1,2,-3] . T h e map funct ion , then , is a means to t r a n s f o r m a funct ion that n o r m a l l y acts o n elements of type a into a func t ion that acts o n lists of elements of t y p e a w i t h o u t chang ing the essence of the funct ion's behav iour . O f course, this idea al ludes to a n i m p l e m e n t a t i o n of the category-theoret ic concept of a functor . A s ant i c ipated , we define Hask to be a category w i t h H a s k e l l types as objects a n d H a s k e l l funct ions as m o r p h i s m s . N o t e that the (associative) op-erat ion of func t ion c o m p o s i t i o n in H a s k e l l is denoted . a n d that H a s k e l l has a p a r a m e t r i c p o l y m o r p h i c ident i ty funct ion . W e c a n conceive a n endofunc-tor o n Hask b y cons ider ing ( [ ] ) : : a -> [a] to be the "object part" of the functor a n d map to be the "arrow part" of the functor . T h e idea is general ized to fmap i n Haskel l ' s b u i l t - i n Functor class. It has the fol lowing dec larat ion: c l a s s Functor (f :: * -> *) where fmap :: (a -> b) -> (f a -> f b). T h a t is, to define a n instance of Functor, a m e t h o d fmap must be defined that accepts any func t ion g : : a -> b a n d re turns a func t ion f g w i t h t y p e s ignature f g : : f a -> f b. E q u i v a l e n t l y , we c a n v iew fmap as a func t ion that accepts a func t ion g : : a ->b a n d a functor element f a, a n d re turns another functor element f b. T h e n a m e of the Functor class is m o t i v a t e d b y the analogy between the def ini t ion of the class a n d the def ini t ion of a functor in category theory. A n y instance of Functor is c o m p r i s e d of a func t ion f that is defined on Haske l l types (objects i n Hask), a n d a means to m a p a n arrow g : : a -> b i n Hask to a n arrow f g : : f a -> f b that is also i n Hask. T y p i c a l l y , category theorists w o u l d labe l the m e t h o d fmap defined on arrows as f , the same n a m e as the p a r t of the functor that acts o n objects . In Haske l l , however, f a n d fmap t aken together are what c o r r e s p o n d to a category-theoret ic functor , where f is the p a r t of the functor that acts o n objects a n d fmap is the p a r t that acts o n m o r p h i s m s . O f course, the def init ion of any functor / in category theory includes two equat ions that / must satsify. F o r a n instance of the Functor class to behave p r e d i c t a b l y a n d consistent ly i n a Haske l l p r o g r a m , analogous laws must ho ld . W e demonstra te the consistency of ideas by g iv ing the fol lowing 21 Chapter 1. Introduction functor laws, which must hold for any instance of Functor. Recall that i d is a polymorphic function and so can act on objects both of type a and of type f a (where, analogous to lists, f a denotes a datatype in which the type of the contained data is a). Then, for f and fmap as given above, as well as functions g,h : : * -> *, the Haskell functor laws are given as: (Fl) fmap i d f a = f a (F2) fmap g . h f a = (fmap g . fmap h) f a. As a demonstration of these laws, recall the list example. This is really just an instance of the Functor class with [] being the 'f : : * -> *' from the class declaration, and map fulfilling the definition for the method fmap. In this case, • map i d [a] ; = [ id a] = [a] = i d [a] • map g . h [a] = C(g . h) a] = map g [h a] = map g (map h [a]) = (map g . map h) [a] . Intuitively, we can think of fmap as a function that applies a given op-eration to objects inside a "container" and then returns a container of the same shape. The shape of the container is left unchanged by fmap (Fl) and the contents are not shuffled relative to one another under the mapping operation (F2). That is, fmap preserves the structure of the category Hask. 22 Chapter 2 Moggi ' s Monads 2.1 Motivation for Monads in Haskell Haskell is a purely functional language. This means that whenever a function is executed, no effects other than the computation of the function output will occur. This is a product of the fact that Haskell abides by the principle of referential transparency (see Section 1.4.1), and that all dataflow is made explicit. Since a program written in a functional language consists of a set of equations, the latter guarantees that the value of a function is only dependent on the function's free variables (Section 1.4.1). It also ensures that the order in which computations are made does not affect a program's meaning [14]. This is not the general case for impure functional or imperative lan-guages, and any state changes unrelated to the output of a function are called side-effects. Printing to the screen, reading a file, or updating a da-tum assignment to a variable are examples of side-effects. Of course, it is hard to imagine doing much useful programming without such capabilities! Haskell employs monads to achieve the usefulness and convenience of impure effects without compromising the purity of the language. While these facts motivate our study, the introduction of monads to computer science actually began with Eugenio Moggi's work in formalizing programming language semantics using category-theoretic concepts, which he called a "categorical semantics of computations" [12]. Moggi's work pro-vides the foundational theory for monads in Haskell, making a detailed ex-amination of it both interesting and important in our context. His approach began with the adoption of the view taken by the denotational theory of semantics, in which programs are thought of as morphisms in a category with the types of a given language as objects. 2.1.1 Heuristics A classical approach to computational semantics is to view a program as a function that maps an input value to an output value. Heuristically, 23 Chapter 2. Moggi's Monads a p r o g r a m (or a p r o g r a m i n a n env ironment) / c o u l d be descr ibed as a c o m p o s i t i o n of funct ions / = / n _ i ° • • • ° / i , where ,f\ : A\ —> A2, • • •, fn-i '• A n - \ —> 4 n a n d V i £ { 1 . . . n) the are types of a g iven language. T h u s , the p r o g r a m w o u l d accept a n i n p u t value a\ £ A\ a n d o u t p u t a value an £ An. M o g g i ' s twist o n the classic m o d e l was to consider p r o g r a m s not as m a p s f r o m values to values, b u t rather as m a p s f rom values to computations. Here , a c o m p u t a t i o n is to be thought of as the denota t ion or m e a n i n g of a p r o g r a m a n d the t e r m "notion of c o m p u t a t i o n " wi l l refer to a qual i ta t ive descr ip t ion of the d e n o t a t i o n of a p r o g r a m . In a c c o r d w i t h d e n o t a t i o n a l semantics , we c a n rephrase this idea as: a c o m p u t a t i o n is to be thought of as the m e a n i n g of a n arrow i n a category of types. If T is a g iven n o t i o n of c o m p u t a t i o n , t h e n TA w i l l denote a c o m p u t a t i o n w i t h r e t u r n t y p e A, a n d wi l l be referred to as a c o m p u t a t i o n of type A. B e a r i n g in m i n d that the goal is to construct a category whose m o r p h i s m s are p r o g r a m s , we now have the choice to m o d e l p r o g r a m s as m a p s of the f o r m f : Ai —> TAn or g : TA\ —* TAn. W e choose the former because it subsumes the latter: any c o m p u t a t i o n of type A\ is a value of type TA\. In s u m m a r y , the categor ica l cons truc t ion used b y M o g g i is as follows [11]: • W e consider a category C w i t h a n opera t ion T that carries a C-object A, representat ive of the set of values of type A, to TA, representat ive of the set of c o m p u t a t i o n s of t y p e A. T c a n be thought of as a u n a r y type -cons truc tor that is some n o t i o n of c o m p u t a t i o n , w i t h the elements of TA be ing v iewed as the denotat ions of p r o g r a m s of type A. • A p r o g r a m that takes a value of type A as i n p u t , per forms a c o m p u -ta t ion , a n d re turns a value of type B, can then be identif ied w i t h a C-arrow f r o m A to TB. • A m i n i m u m set of requirements for values a n d c o m p u t a t i o n s is f ound so that p r o g r a m s indeed c o r r e s p o n d to m o r p h i s m s of a sui table category. B u t what sorts of p r o g r a m m i n g concepts c a n not ions of c o m p u t a t i o n s capture? W e c a n t h i n k of t h e m as a d d i t i o n a l effects that c a n occur d u r i n g the eva luat ion of a funct ion . C o m p u t a t i o n s w i t h except ions a n d c o m p u t a -tions w i t h state modif icat ions are b o t h examples of not ions of c o m p u t a t i o n s . In the former, the d e n o t a t i o n of a p r o g r a m (that is, its semant ic in terpreta-tion) is either a value or a n except ion , d e p e n d i n g o n whether the execut ion of the p r o g r a m involves the o r d i n a r y ca l cu la t ion of a value or the cons iderat ion of a user-defined spec ia l case (for example , a d iv i s i on by zero), respectively; i n the latter, a p r o g r a m denotes a m a p f rom a store to a pa ir c o m p r i s e d of a 24 Chapter 2. Moggi's Monads value a n d a modi f i ed store. T h e s e not ions of c o m p u t a t i o n s are precisely the k inds of effects that were prev ious ly par t i cu lar to i m p e r a t i v e languages a n d thus lay the c o n c e p t u a l foundat ions for i m p l e m e n t a t i o n of such features i n specific pure languages, such as Haske l l . N o w recal l that , i n general , we consider a p r o g r a m to be a func t ion that is the c o m p o s i t i o n of several funct ions , a n d consider the task of m o d i f y i n g such a p r o g r a m so that at some stage of ca l cu la t ion (that is, at some level of c o m p o s i t i o n ) , a n o t i o n of c o m p u t a t i o n is i n t r o d u c e d . F o r example , let us in i t ia l ly assume the classic m o d e l , w i t h a p r o g r a m g iven b y ALB^C^D. Say that we want to in troduce a side-effecting c o m p u t a t i o n T to the func t ion g, b u t otherwise leave the p r o g r a m unchanged . W e thus want to alter the o u t p u t type of g f r o m C to TC a n d the o u t p u t type of h f r o m D to TD (the latter so that the side-effect is carr ied t h r o u g h to the end of the program's evaluat ion) . T h i s alone cannot be done, however, because while we c a n easily envis ion rep lac ing g by a func t ion g : B —> TC, the d o m a i n of h is C a n d not TC. AU B ^TC TD. W e thus need a means to (i) c o m p u t e the desired side-effect; (ii) alter the func t ion h so that it c a n be c o m p o s e d w i t h g; (iii) leave the behav iour of the p r o g r a m otherwise unchanged . T h e s e guidel ines lead to the category-theoret ic concepts of K l e i s l i tr iples a n d K l e i s l i categories for use i n p r o g r a m m i n g semantics . 2.2 Kleis l i constructions A Kleisli triple over a category C is a tr iple (T,n,.*), where T : Oc —» Oc, VA- A-+TA a n d / * : TA —> TB, for A,B,C £ Oc, a n d f : A -* TB, a n d the fol lowing equat ions ho ld: (KTI) rfA = i&TA (KT2) f*°VA = f (KT3) g* o / * = (g* o / ) * w i t h g : B —> TC £ Ac-A K l e i s l i t r ip le models a n o t i o n of c o m p u t a t i o n a n d the above propert ies c a n be in tu i t ive ly u n d e r s t o o d i n the fol lowing m a n n e r . T h e m a p p i n g TJA is the inc lus ion m a p p i n g of values into c o m p u t a t i o n s (any value c a n be thought of 25 Chapter 2. Moggi's Monads as a "constant" c o m p u t a t i o n ) a n d / * is the extens ion of a func t ion / f r o m values to c o m p u t a t i o n s to one f r o m c o m p u t a t i o n s to c o m p u t a t i o n s . Intu-itively, this extens ion c a n be thought of as first eva luat ing a c o m p u t a t i o n a n d t h e n a p p l y i n g / to the r e t u r n value. T h e formal funct ion def init ion for / * c a n be g iven i n terms of the l e t - cons truc tor , w h i c h is i n t r o d u c e d in Sect ion 2.4. A n y K l e i s l i tr iple gives rise to a c o r r e s p o n d i n g K l e i s l i category: g iven a K l e i s l i tr iple ( T , 77, _*) over C , the Kleisli category CT is defined in terms of objects a n d arrows i n C . Since we are cons truc t ing CT f r o m C, we m a y use the same labe l to refer to a n object or arrow i n CT as one i n C. In the case of possible ambigui ty , the category of context wi l l be m a d e expl ic i t . T h e c o n s t r u c t i o n of the K l e i s l i category is defined i n terms of C-objects A, B a n d C-arrows / : A -> TB,g : B —> TC is as follows: • 0Ct = Oc • UomCT(A,B) = Homc(A,TB), where V 4 , B £ C an arrow A -> B £ CT is a n arrow A —> TB. • \/A £ 0cT, 3 id A £ AQT such that i d ^ = T)A, where VA '• A —• TA € Ac-• T h e c o m p o s i t i o n goT f of CT arrows is g iven by the c o m p o s i t i o n g*of: A —> TC i n C. W i t h regard to these ax ioms , note that the defined c o m p o s i t i o n g* o f c a n be thought of as: (i) t a k i n g a value a £ A; (ii) a p p l y i n g / to o b t a i n a c o m p u t a t i o n fa; (iii) execut ing or eva luat ing fa to o b t a i n a value b £ B; (iv) a p p l y i n g g to b to p r o d u c e the resultant c o m p u t a t i o n . W e c a n use the cons truc t ion ax ioms for CT to express the left uni t , r ight uni t , a n d assoc iat iv i ty ax ioms for CT solely i n terms of objects a n d arrows f r o m C as follows. L e t A,B,C be objects i n CT- F o r the left un i t a x i o m c o r r e s p o n d i n g to i d s , let / : A —> B be an arrow i n CT, SO that i d s oT f = f £ CT- W e c a n express the le f t -hand side of the preced ing e q u a t i o n i n terms of C-objects a n d C-arrows us ing the t h i r d a n d f o u r t h c o n s t r u c t i o n ax ioms l isted above: i d s oT f = rjA o f. S imi lar ly , for the right un i t a x i o m c o r r e s p o n d i n g to id/3, let g '• B —» C £ CT, SO that g OT id/5 = 9 G CT, a n d m o v i n g f rom CT to C , we have: g oT id/3 — 9* 0 VB-F i n a l l y , the assoc iat iv i ty a x i o m for CT is easily expressed in terms of C-objects a n d C-arrows us ing the four th cons truc t ion a x i o m . L e t / : A —> B, g : B C, h : C - D £ CT- T h e n , hoT(goTf) = h*o{goTf) = h*o(g*of) a n d (h oT g) oT f = (h oT g)* o f — (h* o g)* o / . T h u s , CT is a category. W e s u m m a r i z e ent irely i n terms of objects a n d arrows i n C , v i a the cor-respondence between HomcT{A, B) a n d E.omc(A,TB) g iven i n the second 26 Chapter 2. Moggi's Monads c o n s t r u c t i o n a x i o m . T h a t is, g iven C-arrows / : A —> TB, g : B —> TC a n d h : C —> TD, we interpret the CT ax ioms i n C as: ( K C 1 ) n*Bof = f , left un i t ( K C 2 ) f* onA = f r ight un i t ( K C 3 ) h* o (g* o f) = (h* o g)* o f associativity. N o w , we c a n d irec t ly prove the equivalence between the K l e i s l i tr iple ax ioms ( K T 1 ) - ( K T 3 ) a n d the K l e i s l i category ax ioms ( K C l ) - ( K C 3 ) . F i r s t , assume ( K T 1 ) - ( K T 3 ) . B y ( K T 1 ) , => V*B° f = idTB ° / => V*B°f = f-T h u s , ( K C 1 ) holds. T r i v i a l l y , we have ( K C 2 ) = ( K T 2 ) . ( K T 3 ) states that h* o g* = (h* o g)*. T h u s , h*o(g*of) = (h*og*)of w h i c h impl ies ( K C 3 ) . N e x t , assume ( K C 1 ) - ( K C 3 ) . B y ( K C l ) , VA0I = / » f o r a n y / t h a t h a s c o d o m a i n TA. In p a r t i c u l a r , take / = idrA- T h e n , rfA o idTA = ICITA r)*A = idTA, a n d so ( K T 1 ) holds. A g a i n , we i m m e d i a t e l y have ( K T 2 ) = . ( K C 2 ) . F i n a l l y , ( K C 3 ) states that h* o (g* o / ) = (h* o g)* o / . R e c a l l that g : B —> TC, so that 5* : TB -> T C a n d (/i* o 5 ) * : T S T D . T a k e / i n ( K C 3 ) to be the ident i ty arrow on TB, f — i d r s - T h e n , h*og* = {h*og)*oidTB a n d ( K C 3 ) impl ies ( K T 3 ) . T h u s , ( K T 1 ) - ( K T 3 ) are equivalent to ( K C 1 ) -( K C 3 ) , as desired. 27 Chapter 2. Moggi's Monads 2.2.1 Example: State Updates We begin to concretize our work with triples by examining a side-effecting computation; namely, modifications to (variable) state. To show that state updates can be modelled using a suitable Kleis l i triple, we must propose def-initions for the three maps (T, 77,-*), and show that they satisfy the Kleis l i triple axioms. As briefly mentioned above, a computation with a state update can be thought of as a computation that takes an init ial store or state variable, and returns a value (the output of the computation's underlying function) along with the modified store. For example, say that we have a simple program that adds several numbers together, and that we want to include a side-effecting computation in which the number of additions that the function performs is kept track of as the function is evaluated. This computation could accept s = 0 as the init ial store, and return the pair (sum, s'), where sum is the return value of the function, and s' is the number of addition operations that were performed to obtain sum. W i t h this motivation, we define the first component of the state update triple to be the functor T(_) = (_ x S)s, where 5 is a nonempty set of stores [10]. We offer the corresponding maps n and _* to form a Kleis l i triple (T, r/,_*) that models state updates: • nA : A -> (A x S)s a h~* VA(a) • S —> A x S s *—* (a, s) • for / : A -> (B x S)s, f*:{Ax S)s -> (B x S)s, a -> f*{a) : S -» B x S where (b, s) = a(s). At a glance, these maps appear a bit ghastly to deal with, so we introduce a small amount of notation that wil l make calculations easier. Any function /:!?—> Rs maps an element d of its domain to a map f(d) : S —> R. We can, of course, evaluate this function on an element s G S to obtain a value r G R\ that is, f(d)(s) = r. Thus, / can be interpreted as a function that accepts a pair of values and returns a single image value. It wi l l be convenient to emphasize this using the following notation: given a map / as above, we define a (redundant) map /1 : D —•> Rs by f\ = /, and a corresponding map /2 : Dx S -> R, such that Vd e D, Vs G S, f2({d, s)) = fi{d){s). As a word of caution, while this notation wil l prove to be expedient in the calculations below, there is one case in which it is somewhat counter-intuitive; namely, with regard to the identity map. For example, if D is 28 Chapter 2. Moggi's Monads taken to be a func t ion space, say D = (A x S)s, w i t h a e (Ax S)s a n d s £ S, then we c o u l d write i d i ( a ) ( s ) = id2 ( (a , s)). Not i ce that whi le the r i g h t - h a n d side of this equal i ty is suggestive of a n eva luat ion to (a, s), the a c t u a l eva luat ion shou ld be i d 2 ( ( a , s ) ) = ( idi(oj))(s) = a(s) ^ ( a , s). W i t h this setup, the p r o p o s e d K l e i s l i t r ip le c a n be presented i n a new form. W e c l a i m that the 3-tuple ( T , 77, _*) defined by: • TA = (A x S)s (S ^ 0) • V a £ A, Vs £ S, r)A2((a,s)) = (a, s) • W l , / 3 6 O c w i t h / : A -> (5 x 5 ) 5 a n d a £ ( A x S)s, / 2 *( (a , s ) ) = / 2 ( a ( s ) ) , where / 2 * : ( A x S)s x S - x 5 a n d /j*(a)(s) = / » ( s ) = is a K l e i s l i tr iple . W e note here that a c o m m o n way to define this tr ip le is to use A-ca lculus no ta t ion . W e have avo ided i n t r o d u c i n g that n o t a t i o n here, b u t give the f o r m u l a t i o n for reference [12]: • r]A{a) = As : 5 . (a , s) • for / : A -» (B x S)s a n d a £ (A x S)s, f*(a) = As : S.(let (a, s') = a(s) i n / (a ) ( s ' ) ) . T h e n o t a t i o n As : denotes that the func t ion fol lowing the ':' is g iven i n terms of the independent variable s, a n d the n o t a t i o n S. denotes that the independent variable i n the func t ion fol lowing the ' . ' i s restr icted to S ( in this case, we have s £ 5 ) . W e now show that the g iven 3-tuple satisfies ( K T 1 ) - ( K T 3 ) as follows. F o r ( K T 1 ) , we have idTA • {A x S)s (Ax S)s', where V a £ (A x S)s idxAict) = a Vs £ 5 , idjv i (a: ) ( s ) = a ( s ) . T h u s , 77^ = i d y / i t r i v ia l l y b y the second f o r m u l a t i o n for 77 g iven above. F o r ( K T 2 ) , let / : A -> (B x S)s, a £ A, s £ S. T h e n , ( r°7M) . i (a ) ( s ) = / 1 *(7 ? / U (a) ) ( s ) = /2 (?Mi(a ) ( s ) ) = / 2 ( ( a , s » = / i ( a ) ( s ) . T h u s , f* or]A = f. T o prove that ( K T 3 ) holds , we first prove the fol lowing propos i t ion: 29 Chapter 2. Moggi's Monads P r o p o s i t i o n 2.2.1. Given maps f :A-+(B x S)s andg:B^{Cx S ) ' we have: 5i 0 / l = 92 ° h-Proof. L e t / a n d g be as g iven, a n d let a £ A, s £ 5. T h e n , = 52 ( / i ( a ) ( « ) ) = 2 2 ( / 2 « a , S » ) = (52 ° / 2 ) 2 ( ( a , s ) ) = (52 ° /2)i(a)(s), as desired. N o w , to show ( K T 3 ) , let a £ {Ax S)s a n d s £ 5. W e have: (5* o / ) ! ( £ * ) ( * ) = ^(^(a))^) = 52 ( / i (a ) ( s ) ) = 52 ( / 2 (a(s) ) ) = (520/2)2(^(5)) = (5i 0 / i ) 2 ( a ( s ) ) p r o p o s i t i o n T h u s , 5* o / * = (#* o / ) * a n d ( T , 7?, _*) is a K l e i s l i tr iple . 2.3 Triples W h i l e K l e i s l i triples are intu i t ive ly just i f iable as a means to theoret i -ca l ly m o d e l c o m p u t a t i o n s , they are equivalent to another very interest ing category-theoret ic cons truct ion; n a m e l y . . . monads ! Incidently , the equiva-lence explains the other n a m e "triples" for m o n a d s that appears i n m u c h of the l i terature . T h e o r e m 2.3.1. There is a one-to-one correspondence between Kleisli triples and monads. Proof. G i v e n a K l e i s l i tr iple ( T , 77, _*), we c l a i m that the c o r r e s p o n d i n g m o n a d is ( T , 77, fi), where: (i) T is the extension of the func t ion T : OQ —* OQ to the endofunctor T : C —> C , defined o n any C-arrow / : A —> B by T(f) — (ilB o / ) * a n d (ii) fj,A = i d f ^ . T o prove this , we first show that T is indeed a functor . L e t / : A —> B,g : B —> C. T h e n , 30 Chapter 2. Moggi's Monads T(gof) = (vco(gof))* = ((rjc o g) o / ) * assoc iat iv i ty i n C = ( ( ( r ? C ° 2 ) * ° ? ? B ) ° / ) * ( K T 2 ) = (ivc ° g)* o (IB o f))* = (rjc o g)* o (nB o f)* ( K T 3 ) = TgoTf. F u r t h e r , T(idA) = (r)AoidA)* = rfA - \dTA. T h u s , T is a n endofunctor o n C. N e x t , we show that ry a n d p are n a t u r a l t rans format ions . L e t / : A —> B be a n arrow i n C. F o r ry, we have Tf or)A = (rjQ o /)* o r)A defn of extens ion of T = VB°f. ( K T 2 ) T h u s , ry is a n a t u r a l t rans format ion . T o show p is n a t u r a l , we have Tf OPA = {VB ° / ) * 0 fJ-A defn of T = {VB ° / ) * ° idTA defn of pA = UvB°fyo\dTAy (KT3) = ((vBojyy = ( i d r B ° {VB o / )*)* = ( ( i d f B o r y T B ) o ( r y W ) T ( K T 2 ) = ( i d ^ B 0 (VTB o {r)B ° /)*))* = i d ^ B 0 (.VTB 0 {j]B 0 /)*)*) ( K T 3 ) = MB 0 (VTB ° (VB 0 / )* )* defn of pB = HB°T(riB°fy defn of T = pBoT{Tf). defn of T T h u s , p is a n a t u r a l t rans format ion . W e now show that the m o n a d laws are satisfied. N o t e that i d ^ : T2A —> TA a n d \d*TiA : T 3 A -> T2A. T h u s , we have M/l 0 f-TA = idTA o idT2A = (id*TAoidT2Ay ( K T 3 ) - ( i d ^ ) * = {idTA o id*TA)* = ( ( i d ^ o r / T v O o i d ^ , ) * ( K T 2 ) = (i<*TA 0 (rlTA o id*TA)y = id*TA o (m-A o id*TA)* ( K T 3 ) 31 Chapter 2. Moggi's Monads = i d ^ o T ( i d ^ ) = fj,AoTu.A. To show that the proposed 3-tuple satisfies the second monad law, we com-pute: HA 0 VTA = i d T A o rjTA = i d ™ (KT2) = V*A (KT1) = {idTA °VA)* = ((^TA 0 VTA) o VA)* (KT2) = ( i d f / i 0 (VTA 0 VA)T = \dTAo{nTAo TJA)*. (KT3) Since TJA is an arrow from A to TA, by the definition of the extension of T from a function to a functor given in Theorem 2.3.1, we have T(T]A) = {VTA ° VA)*- Thus, . = i d ^ o Tr]A defn of extension of T = \IAOTT)A. Thus, the Kleisl i triple gives rise to a monad. To show the converse, if we are given a monad (T, v,f), then we claim the corresponding Kleisl i triple is (T, 77, _*), where: (i) T is the restriction of the endofunctor T to the objects of C and (ii) for / : A —> T73 E Ac, f* = HB 0 (T1/)- We show that this 3-tuple is indeed a Kleis l i triple as follows. First, rfA = HA o TT]A = idTA, by the second monad law. Thus, (KT1) holds. Next, we compute /* ° VA = {HB 0 Tf) o TJA = HB 0 VTB 0 f = id^B ° / monad law 2 - /• Thus, we have (KT2). Finally, we show that (KT3) holds by 9* °f* = (fic ° Tg) o (/j B o Tf) = Mc ° HTC ° T2g o Tf = HC 0 THC 0 T2g o Tf monad law 1 = He o T{HC oTgof) = {HC °Tgo /)* = (5*0/)*, 32 Chapter 2. Moggi's Monads which implies that (T, TJ, _*) is a Kleis l i triple. Therefore, there is a one-to-one correspondence between Kleisl i triples and monads. • This correspondence immediately gives us an alternative description for Kleis l i categories, which is stated thus [8]: given a monad (T, n, n) in a category C, assign to each object A 6 C a new object Ax and to each C-arrow / : A —>'TB a new arrow fK : AT —> Bj-. These new objects and arrows constitute the Kleis l i category of the monad Cx when the composition of C^-arrows fK : AT —> BT, gK • BT —> CT is defined by gK o fK = (fie ° Tg o f)K. Proofs of the right and left unit laws and the associative law can be summarized with the following commutative diagrams, where f : A -* TB, g : B -> TC, h : C TD G Ac. Notice that the identity arrow for Cj- is {T]A)k '• AT —* Ax-A fK o (nA)K = fK f TB TB Va TA VTB + TB (vc)K o gK = gK • h« °(gK of«) = (hK °gK)of fK B TC Tvc T C J ^ - T2C T 2 C TsD T2D PC P-TD PD TC T2D -^-> TD 2.3.1 Example Revisited: State Updates Using the correspondence given in Theorem 2.3.1, we can now refor-mulate our earlier example in terms of monadic, rather than Kleis l i , maps. Recall that for state updates, we define the endofunctor T to act on objects by TA = (A x S)s. Thus, from the theorem we have HA = id*TA : {(A x S)s x S)s -> {A x S)s. 33 Chapter 2. Moggi's Monads We can semantically interpret this map in terms of state modifications by observing how this function behaves on input values. Let / £ ((A x S)s x S)s,f £ (Ax S)s,a £ A and s,s ',s" £ S. Further, let f(s) = (/',s'} and f'(s') = (a,s"). Then, pA(f)(s) = idTA1(f)(s) = idTA2(f(s)) = i d r A 2 « / V » = i d ™ (/')(*') = / V ) = (a, a")-That is, pA(f) is a computation which, on input s (a store), first computes a pair comprised of a new computation and a modified store, f(s) = {/', s'} and then outputs the value-store pair f'(s') = (a,s"). We note that in the A-calculus, this would typically be denoted by idTA(f) = As : 5.eval(/s). The theorem likewise supplies definitions for r\ and for the action of T on a given function. Using these, we can verify that the monad laws hold. First, we show equality of the outputs returned by each of the functions \±A ° f-TA and pA o TpA on input (f,s), for / £ T3A = (((A x S)s x S)s x S)s and s £ S. To facilitate this, let / ' £ T2A, f" £ TA, a £ A and s', s" £ S, with f(s) = (f',s') f'(s') = (f",s») f"(s") = (ay). We have: (AM ° W r v i ) i (/) ( * ) = ([d*TA °id*T2A)i(f)(s) = i d T / l i ( i d T 2 ^ i ( / ) ) ( s ) = idTA2(idT2A1(f)(s)) = id T ^2( id T 2^ 2 (/ ( s ) ) ) = i d T ^ 2 ( i d r 2 j 4 2 ( ( / / , s ' ) ) ) = i d ™ ( idr^i (/')(*')) = idTA2(f'(s')) = \dTA1(f")(s") = (a,s"') 34 Chapter 2. Moggi's Monads and {fiAoTfiA)(f)(s) = i d T A o (nTA o\dTA)*)(f){s) = idTA2{{r)TA°idTAY1{f)(s)) = idTA2{{VTA ° idTA)i{f'){s')) = i d T ^ ( r ? ^ i ( i d ^ 1 ( / ' ) ) ( 5 / ) ) = idTA2((idTM(f),s')) = id^ (/')(*') = i<W/V)) = idTA2((f",s")) = f"(s") = (a,s">). Thus, the first monad diagram commutes. Similarly, we compute the return values for [/.A ° VTA and \XA ° TTJA on (/", s") G (A x S)s x 5 as follows: (HA°rrrA)i(f")(s") = ( i d ^ o ^ ) ^ / " ) ^ " ) = idTA1(VTA1(f"))(s") = i d i M 2 ( r 7 i v i i (/")(*")) • = idTA2((f",s")) = f(s") idT A(f")(s") and (HA°Tr,A)(f")(s") = (id*TAo TrlAHf")(s") (idTA o {ryiA ° VAY)\U"){S") ^TAI{{VTAOVAYIU")){S") idTA2((VTA°AY(f")(s")) idTA2((VTA°VAh(f"(s"))) idTA2{(VTA o r M ) 1 ( a ) ( s " ' ) ) ^TA2{VTA\{VA\{a)){s'")) ^TA2((VAl(a),s"')) VAi(a)(s"') 35 Chapter 2. Moggi's Monads = / " ( « " ) • Thus, we have verified that the 3-tuple (T, n, fi) for state updates is a monad. 2.4 Strong Monads We are about to investigate the connections between our work thus far with the so-called "monads" of Haskell. The implementation of monads in Haskell was led by Phi l ip Wadler, whose work on the subject uses the theory of Moggi 's notions of computations. We conclude this chapter by examining another category-theoretic concept used in Moggi 's work, which is technically required for Wadler's implementation. In Section 1.4.1, we commented that the A-calculus served as a foun-dation for many functional languages, such as Haskell. Since Moggi's aim was to provide a categorical semantics of computations for studying lan-guages based on typed A-calculi, his theory had to be rich enough to be able to interpret A-terms. We have already noted the equivalence between the A-calculus and cartesian closed categories, but a monad over a cartesian closed category does not have sufficient structure to interpret A-terms in a computational model [10]. One problem that arises involves a form of local definition that is used in functional languages. A local definition is the introduction of an association between a name and value for use within an expression, and the form we are interested in here is called the let-constructor. The let-constructor is equivalent to function application, and we briefly motivate its definition before explaining its relevance in Moggi's computational A-calculus. A typical A-function applied to an argument can be represented as A (name), (body) (argument), where (name) is a bound variable, and (body) and (argument) are A-expressions. The function evaluation requires that we replace all free occurrences of (name) in (body) with (argument), prior to evaluating (body). Equivalently, we can think of associating (name) and (argument) throughout the evalua-tion of (body). We notationally capture this equivalent conception of func-tion evaluation using the let-constructor [9]: let (name) = (argument) in (body). 36 Chapter 2. Moggi's Monads As referred to in Section 2.2, the let-constructor is used to define the extension of a function / to /*; specifically, given a notion of computation T, types A, B, a program / : A —> T73, and a denotation of a program c £ we define the extension of / by /*(c) =' (let a; = c in f(x)). Despite its importance, the interpretation of an expression such as (let x = e in e') is problematic in a category with finite products and a monad, when e' has free variables aside from x, as is shown in [10]. Essentially, the problem is that even in a category with cartesian products and a monad, there is not enough structure to transform a value-computation or computation-computation pair into a computation of a pair. A similar problem arises in the interpretation of functional types, in which it is necessary to obtain a computation that computes a pair from a given pair of computations. We can resolve these problems by requiring our monad to be a strong monad—a monad along with a natural transformation that is defined as follows. A strong monad over a category C with finite products is a monad (T, rj, p) together with a natural transformation t with value tA,B from A x TB to T(A x B), such that the following diagrams are commutative [11]: 1 x TA -^ -> T( l x A) TA TA {A x B) x TC <*A,B,TC tAxB.C T((A xB)xC) I TaA,B,C Ax(Bx TC) i d " x t B - c , A x T(B x C) T(A x (B x C)) Ax B id A X T)B AxTB id i d A x l tA,B A x T2B T(A x TB) Ax B VAxB T{A x B) VAxB ^ > T2(A x B) 37 Chapter 2. Moggi's Monads where rA • 1 x A —> A and CXA,B,C '• (A x B) x C —> A x (B x C) are natural transformations. The given natural transformation t A l B acts to transform a value-computation pair into a computation of a pair of values in the following manner: tA,B • AxTB -> T(A x 73) (a,c) ' ^ (let y = c in (a,y)). For example, in the case of state updates, the natural transformation tA,B (Q! c) is a function which, given a store s returns the computation (let (b, s') = c(s) in ((a,b),s')) [12]. Since Haskell is based on the A-calculus, the applied category-theoretic concepts we explore must be compatible with the interpretation of A-terms. Hence, the "monads" that we wi l l examine in Haskell are actually strong monads. 38 Chapter 3 Wadler ' s Monads By now, it should not be a surprise that in Haskell, monads are data types that are used to represent computations. If m is a monad, then an object of type m a represents a computation with return type a. The definition of a particular monad wi l l reflect the sort of side effect that the monad is trying to computationally mimic. Its use wi l l ensure that type checker can verify that the side-effects are managed consistently throughout the program. In this way, monads are a means to encode the behaviour of computations, as opposed to values, in Haskell's type system. Before we examine the Monad class declaration, let us informally consider a motivating example. 3.0.1 The Maybe Monad Consider a function or operation that is undefined at one or more values: for example, division. In a composition of functions in which at least one of the functions involves division, an attempt to divide by zero means that the computation can not be completed. For instance, consider the simple function f :: Int -> Int -> Int -> F l o a t f x y z = (1 / x) + 1 / (y + z) On init ial inspection, it appears that before this function can be evaluated we must check to see if both of the terms are actually integers. In general terms, to add error handling to a program written in a purely functional language, the result type of the program would have to be modified to include error values, and failures would have to be checked for and handled appropriately at each recursive call in the program. We can avoid such failure checking, however, by carrying out such an operation in the Maybe monad. In Haskell, Maybe is the name of both a data type and a monad, with the declaration of the former given as follows: da ta Maybe a = Jus t a I Noth ing 39 Chapter 3. Wadler's Monads As a technical aside, we note the difference between 'data ' declarations and 'type' declarations. The former introduces a new data type (for example, Maybe) and new constructors for values of that type (Just and Nothing), while the latter defines a synonym for a pre-existing type. Either kind of declaration can be used in the definition of a monad. In the Maybe monad, the validity of an expression such as that given above can be implicit ly checked and used to determine the value that is returned: if there are no undefined terms in the expression, the function wil l return a Maybe value of type Jus t , whereas an erroneous evaluation wi l l return Nothing. For example, if our function above is evaluated using an implementation of the Maybe monad, then f 1 0 1 would return Ju s t 2 and f 1 -1 1 would return Nothing. The benefit is that this function can now be composed with other func-tions and, in the case of failure, the "error" wi l l cascade through the program in a safe and predictable way. Note that in a series of computations that included the latter evaluation of f above, any computations that did not involve f would evaluate as normal, and computations that did involve f would now return Nothing. In general, the Maybe monad provides a means to combine a chain of computations, each of which may return Nothing, by terminating the chain early if any step does in fact return Nothing. 3.0.2 Definition of a Monad In the context of Haskell, we define a monad to be a 3-tuple (M, r e t u r n , >>=), where M is a type constructor and r e t u r n and » = (read "bind") are polymorphic functions with type signatures as shown in the (minimal) class declaration below: c l a s s Monad m where r e t u r n :: a -> m a ( » = ) : : m a -> (a -> m b) -> m b Let us examine these methods in detail. For use as a model monad by which to exemplify the concepts discussed, we provide the instance declaration of the Maybe monad: i n s t ance Monad Maybe where r e t u r n a = Jus t a Noth ing >>= f = Noth ing Ju s t x >>= f = f x 40 Chapter 3. Wadler's Monads T h e r e t u r n O p e r a t o r Any compositions within a monad must involve monadic-typed argu-ments. Informally, the purpose of the r e t u r n operator is to get us into the monad. More specifically, it converts a value into a computation that returns a value of the same type—that is, into a corresponding monadic type. The technical means by which this is done wil l depend on the particular monad under consideration, but in a general sense, r e t u r n carries a value to the "simplest" corresponding monadic-typed value, while leaving the original value otherwise unaltered. As shown in the instance declaration, r e t u r n is defined to be Jus t in the Maybe monad. T h e ( » = ) O p e r a t o r For a monad M, The infix operator (>>=) provides a way to apply a function of type a -> M b to a computation of type M a. Intuitively, we can think of the operation (M a) >>= f in the following way. First, the monadic structure of the argument M a is removed to unveil any number of values of type a inside. The actual means of doing this is specific to the definition of ( » = ) for the particular monad under consideration. These non-monadic values can then be passed to f one at a time, with each application of f to a value of type a producing a corresponding monadic element of type M b. Next, the monadic structure of each of these f-output elements is removed, yielding a collection of elements of type b. Finally, the monadic structure is reassembled over this collection (in a way that must be defined specifically for the particular monad M under consideration), producing a single monadic element of the correct type, M b. We may refer to the process in its entirety as "binding M a to f." As an example of this process, consider the Maybe monad, in which we have (Jus t x) » = f = f x, for x : : t and f : : a -> Maybe a. That is, the monadic layer of Jus t x is "removed" and just the value x is unveiled. The value x is then passed to f : : a -> Maybe a, which returns a Maybe-typed value (either Jus t y for some y, or Nothing). As is also shown in the instance declaration, Noth ing >>= k = Nothing. This is consistent with the intuitive idea that no value is extracted from Nothing, so nothing is passed to k and no output value is produced. Each instance of the monad class must satisfy 3 laws in order to behave properly in the program. Note that for user-defined monads, it is up to the user to ensure that the laws are satisfied, since it is impossible for the type 41 Chapter 3. Wadler's Monads checker to do so [6]. The statement of the laws makes use of Haskell syntax that is based on shorthand A-calculus notation; namely, an expression of the form \ x —•> e(x) explicitly defines the function that maps a variable x to an expression e(x), with e(x) dependent on x. That is, we code the A-calculus expression Ax : e(x) in Haskell as \ x -> e (x ) . For example, the expression \ x -> s i n x is similar to defining the function e(x) = s inx in standard mathematical notation, except that we do not need to explicitly give the function defined by the former expression a name (such as 'e ' in the lat-ter). The Haskell notation is helpful to use in conjunction With expressions involving more than one occurrences of the (infix) operator ( » = ) , which accepts a monadic element on the left and a function on the right. W i t h this, the Haskell monad laws are: ( M l ) r e t u r n x » = f = f x (M2) n » = r e t u r n = n (M3) (n » = f ) » = g = n » = (\x -> (f x » = g ) ) , where x : : a, n : : m a, f : : a -> m b and g : : b -> m c. The first two monad laws ensure that r e t u r n preserves all information about its argument. That is, for (M l ) , if we define a tr iv ial computation r e t u r n that accepts a value a and returns a, and bind this computation with another computation f, then the result is the same as if we had applied f to a directly. For (M2), if we perform the computation n and then pass the result to the tr ivial computation r e t u r n , the result is the same as if we had just performed the computation n. The third law (M3) is essentially an associativity law for (>>=), which accounts for the type signature of the operator. Given this definition of a monad and the associated laws, we raise our primary question of interest: What is the precise connection between monads as defined and used in Haskell, and the category theoretic definition of monads discussed in Section 1.3? 3.1 Examples We present further examples of monads in Haskell, so as to build an intuition of how they work. 42 Chapter 3. Wadler's Monads 1. The simplest monad is the identity monad, with the triple defined as: type Id a = a r e t u r n :: a -> Id a r e t u r n a = a ( » = ) : : Id a -> (a -> Id b) -> Id b x » = f f x. Here, Id is the identity function restricted to types (implicitly), r e t u r n is the identity function, and ( » = ) simply evaluates f x. Were this monad implemented, no non-trivial computation would take place along with the regular evaluation of the function. 2. We have already investigated in detail the theory behind state updates as monads, and we continue this example with a Haskell implemen-tation. To begin, we give a simple Haskell evaluator whose task is to compute a quotient of two integers [17]. We define a data type Term by: da ta Term = Con Int I D iv Term Term, where a term is to be either a constant Con a for an integer a, or a quotient D iv t u of terms t and u. The evaluator is then simply: e v a l :: Term -> Int e v a l (Con a) a e v a l (Div t u) = e v a l t ' q u o t ' e v a l u. As indicated by the type signature, the function e v a l accepts a term and returns an integer. If the term is a constant (that is, an integer rather than an expression involving a division), then that constant is returned. If the term is a quotient, then the expressions comprising the numerator and denominator are: (i) evaluated as subterms; (ii) the division is computed once the subterms are reduced to constants; (iii) the quotient is returned (the function ' q u o t ' is integer division). For example, we have eva l (D i v (D i v (Con 11904)(Con 2) ) (Con 3)) = 1984, W i t h this as an evaluator template, we can consider making mod-ifications that mimic side-effects. Say we want to keep track of the number of divisions performed during a calculation made by e v a l us-ing state updates. We begin with Moggi's notion of computation and declare two data types: 43 Chapter 3. Wadler's Monads type M a = S ta te -> (a, S ta te ) type S ta te = Int. Certainly, the evaluator can be adapted to the task of counting op-erations as it calculates, without the use of monads. However, the alteration is tedious because for each call of the evaluator, the current state must be passed in, and the updated state must be extracted from the result and passed on appropriately. The modified evaluator can be coded to require an additional input integer that is to be thought of as a counter variable, with sO being the init ial state. Divisions are carried out using recursive substitutions (until a constant is reached), where each recursive step also involves substituting an incremented state variable value for the previous state variable value. This can be done using the let-constructor syntax in Haskell. Haskell code involving l e t statements is to be interpreted as the obvious substitution operation: let x — x' in E(x) means substitute x' for x in expression E. Such a modified evaluator could look like: e v a l :: Term -> Int -> M Int e v a l (Con a) sO = (a,sO) e v a l (Div t u) sO = l e t ( a , s i ) = e v a l t sO i n l e t (b,s2) = e v a l u s i i n (a ' q u o t ' b, s2+l) To demonstrate its operation, an input of e va l (D i v (D i v (Con 11904)(Con 2) ) (Con 3)) 0 corresponds to t = Div(Con 11904) (Con 2 ) ,u = Con 3 and sO = 0. Bearing in mind Haskell's lazy evaluation, this computation proceeds as: - let (a, s i ) = eval D iv (Con 11904)(Con 2) 0 in let (b, s2) = eval (Con 3) s i in (a 'quot' b,s2 + 1) - let (a, s i ) = eval D iv (Con 11904)(Con 2) 0 in let (b,s2) = (3, s i ) in (a 'quot' b, s2 + 1) - let (a, s i ) = eval D iv(Con 11904)(Con 2) 0 in (a 'quot' 3, s i + 1) 44 Chapter 3. Wadler's Monads - let (a, si) = (let (a', si') = eval (Con 11904) 0 in let (b',s2') = eval (Con 2) s i ' in (a''quot' 6',s2' + l)) in (a 'quot' 3, s i + 1) et (a, si) = (let (a', si') = eval (Con 11904) 0 in let (b',s2') = {2, si') in (a' 'quot' b',s2' + 1)) in a 'quot' 3, s i + 1) et (a, si) = (let (a', si') = eval (Con 11904) 0 in (a' 'quot' 2, s i ' + 1)) in a 'quot' 3, s i + 1) et (a, si) = (let (a', si') = (11904,0) in (a' 'quot' 2, s i ' + 1)) in a 'quot' 3, s i + 1) et (a, si) = (11904 'quot' 2,0 + 1) in a 'quot' 3, s i + 1) 5952 'quot' 3,1 + 1) 1984,2) As desired, the return of the computation is the ordered pair that has the result of the division calculation as its first component and the number of divisions performed as its second. To implement monadic abstractions in the evaluator, we re-define the evaluation function in terms of the r e t u r n and >>= operations. As offered in [17], we have: eval : : Term -> M Int eval (Con a) = re t u r n a eval (Div t u) = eval t >>= \a -> eval u » = \b -> re t u r n a 'quot' b, noting that the compiler implicitly inserts brackets into the above expression as follows (that is, the compiler automatically interprets the expression with the following precedence):' eval (Div t u) = ((eval t) »= (\a —> ((eval u) »= (\b —+ (return (a 'quot'.6)))))). 45 Chapter 3: Wadler's Monads This monadic evaluator can be verbally described as follows: the type signature indicates that the evaluator accepts a term and performs a computation with return type Int. To evaluate a constant term, simply return it. A computation of the form (Div t u) is performed by first computing t (which may be a constant or an expression involving the Div operator) and binding a to the result, then computing u and binding b to the result, and lastly returning a 'quot' b. Informally, the expression t is simplified to a constant, this re-sult being a monadic type M Int. The integral value contained in the monadic-typed term is extracted from the monad and passed as an ar-gument to the function \ a -> e v a l u >>= \b -> r e t u r n a ' q u o t ' b. In standard mathematical notation, if we call the extracted inte-gral value c and label the preceding function as /(a), then the last step amounts to removing the monadic layer from the output of eval t to obtain c, and then computing /(c). Similarly, the expression e v a l u >>= \b -> r e t u r n a ' q u o t ' b simplifies u to a constant element in M Int and passes it as an argument to a function that maps input b to the (monadic-typed) constant a ' q u o t ' b. Essentially, then, all that is happening is that the given expressions t and u are simplified to constants and the quotient of these constants is returned. The >>= operation allows us to easily pass along the simplified results, accounting for the monadic types as required. Having offered a general monadic (division) evaluator, we now de-fine the triple specific to the case of state updates. In the following code, r e t u r n a returns the computation that accepts an init ial state x and returns the pair comprised of the value a and the unchanged state variable x. The call m » = f first performs the computation m in the init ial state sO. This computation yields the value a and updated state s i . Then, the computation f a is performed in state s i , which returns the pair comprised of the value b and the final state s2. The triple is given as: type M a = S ta te -> (a, S ta te ) type S ta te = Int r e t u r n :: a -> M a r e t u r n a = \ s0 -> (a, sO) ( » = ) : : M a -> (a -> M b) -> M b m >>= f = \ s0 -> l e t ( a , s i ) = m sO i n l e t (b,s2) = f a s i i n (b,s2) 46 Chapter 3. Wadler's Monads To complete the task of counting the number of divisions that are performed during a calculation, we define a method count by: count :: M() count = \s -> ( 0 , s + l ) This function increments the state by 1 and returns the empty value (). To count the number of divisions as they occur in a calculation, we simply replace the call r e t u r n a ' q u o t ' b by count >>= \_ -> r e t u r n a ' q u o t ' b in the original monadic evaluator [17]. 3. The monadic evaluator from the preceding example can also be em-ployed to demonstrate use of the monad laws (M1)-(M3). We modify it slightly so that it performs a multiplication, rather than division operation: da ta Term = Con Int I Mult Term Term e v a l : : Term -> M In t e v a l (Con a) = r e t u r n a e v a l (Mult t u) = e v a l t >>= \ a -> e v a l u >>= \b -> r e t u r n a * b and use the monad laws to show that multiplication as performed by the evaluator is associative; that is, eval Mu l t t (Mult u v) = eval Mu l t (Mult t u) v. We begin by expanding the left-hand side using the definition of e va l : eval (Mult t (Mult u v)) = eval t »= (\a —> eval (Mult u v) >>= (\x —> return a * x)) = eval t >>= (\a —* (eval u >>= (\6 —•» eval v »= (\c —> return b * c))) >>= (\x —> return a * x)). Law (M3) implies that the order of parentheses does not affect the output of the computation: — eval t »= (\a —•> eval u >>= (\b —> eval v »= (\c —> return 6 * c >>= (\x —» return a * x)))), and by (M l ) , we have the return of the evaluator on input Add t (Add u v ) : = eval t >>= (\a —> eval u >>= (\6 —> eval v >>= (\c —> return a * (b * c)))). 47 Chapter 3. Wadler's Monads Similarly, for the right-hand term we have: eval (Mult (Mult t u) v) = eval Mu l t t u »= (\x —> eval v »= (\c —* return x * c)) = (eval t >>= (\a —* eval u >>= (\b —> return a * b))) >>= (\x —> eval u >>= (\c —•> return x * c)) = eval t »= (\a —> eval u »= (\b —> return a* b >>= (\x —> eval i> >>= (\c —> return x * c)))) = eval t »= (\a —* eval u »= (\b —> eval v >>= (\c —> return (a * 6) * c))). Thus, associativity of integer multiplication implies associativity of the evaluator multiplication. 4. Lists were previously introduced in the discussion on the Functor type class, where we mentioned that [a] denotes a list of elements of type a. Some additional pertinent syntax includes the expression of a list in the form x: [xs] , where x is the first element of the list (called the 'head'), and xs is the remainder of the list (called the ' ta i l ' ) . For ex-ample, [1,2,3] = 1:[2,3] = 1:2:3: []. This notation is tailored to facilitate recursive list definitions and computations. As well, the op-eration (++) : : [a] -> [a] -> [a] is defined as the concatenation of the two input lists. W i t h this, we claim that the list type constructor, which we denote as L, forms a monad when combined with the following maps: r e t u r n :: a -> [a] r e t u r n a = [a] ( » = ) : : [a] -> (a -> [b]) -> [b] [] » = f = [] x :x s » = f = f x ++ (xs » = f ) Here, r e t u r n maps an element x of type a to the list that contains the (single) element x. Note that the instance definition of ( » = ) for this proposed monad in terms of concatenation leads us to assume that f x is finite. W i t h this definition, the computational interpretation of the expression x: xs >>= f begins by passing the first element of the list x: xs (namely, x) to the function f : : a -> [b], which outputs a list of elements of type b. This list f x is to be concatenated with the list xs » = f, which must be recursively simplified according to the previous description until the final concatenation of some list with the empty list occurs (that is, once [] » = f = [] is computed in the recursion). 48 Chapter 3. Wadler's Monads Let us prove that lists do in fact satisfy (M1)-(M3). For (M l ) , let x : : a and f : : a -> [b]. Then, return x >>= f = [x] » = f defn of return for lists = x: [] » = f defn of (: ) = f x ++ ([] » = f) defn of ( » = ) for lists = f x ++ [] defn of ( » = ) for lists = f x, defn of (++) as required. For (M2), we let m = x:xs be a list with n + 1 elements and induct over the length of m. Taking m to be the empty list as the base case, we have [] » = return = []. Now, assume that (M2) is true for a list xs of length n; that is, assume xs >>= return = xs. Then, x:xs >>= return = (return x) ++ (xs >>= return) = [x] ++ xs = x:xs. Thus, by induction (M2) holds for lists. Before proving (M3), we first prove the following small proposition, which states that ( » = ) is right distributive over list concatenation (++). Proposition 3.1.1. Given a finite list 1 : : [a], a list j : : [a] and a function f : : a -> [b], we have (1 ++ j) » = f = (1 » = f) ++ (j » = f). Proof. To show that the proposition holds for 1 = x: xs of arbitrary, finite length, we induct over the length of 1 and let j be arbitrary. In the base case, we have ( • ++ j) » = f = j » = f = • ++ (j » = f) = ( • » = f) ++ (j » = f), as desired. Next, assume as the induction hypothesis that (xs ++ j) » = f = (xs » = f) ++ (j » = f), where xs is a list of length n. Then for 1 = x:xs, we have 49 Chapter 3. Wadler's Monads (x:xs ++ j ) » = f = f x ++ ( (xs ++ j ) » = f ) = f x ++ (xs » = f ) ++ ( j » = f ) = (x:xs » = f ) ++ ( j » = f ) , by the associativity of (++). Thus, the proposition holds by mathe-matical induction. • Finally, to prove (M3), let g :: b -> [c ] , and m be as in (M2) above. We have (x:xs » = f ) » = g = (f x ++ (xs » = f ) ) » = g = ( f x >>= g) ++ ( (xs » = f ) » = g) proposition = ( f x » = g) ++ (xs » = (\a -> (f a » = g ) ) ) = x :x s » = (\a -> (f a » = g ) ) , defn of ( » = ) for lists as desired. We have thus shown that (L,return, ( » = ) ) is a monad. This proof is also a nice demonstration of the ease of synatactic ma-nipulation and equational reasoning offered by purely functional lan-guages! Thus far, each monad we have considered has corresponded to a computation type, so it is natural to consider if the same is true for lists. Indeed, we can think of lists as a means to model relations, where a computation of type [a] offers one choice for each element in the list. Thus, modifying a function f : : a -> b to its monadic equivalent f : : a -> [b], entails offering a choice of results for each argument [17]. 50 Chapter 4 Equivalence Thus far, we have examined: i) Moggi's incorporation of category theory into programming semantics via his category-theoretic semantics of com-putations, and ii) Wadler's implementation of Moggi's theoretical work in structuring the particular functional language Haskell. While the theory of i) was motivated using Kleis l i triples, Theorem 2.3.1 gave the explicit con-nection between Kleis l i triples and the "purer" category-theoretic concept of monads. We are now ready to give a similarly explicit connection between ii) , which is centred around the maps r e t u r n and » = , and the standard formulation of monads in category theory. 4.1 Preliminary Connections The first connection is easy to identify. Recall the type signature of r e t u r n for any (Haskell) monad: r e t u r n :: Monad m => a -> m a, where a is any object in Hask . This is exactly analogous to the domain and codomain of the map 77 that must be defined for any (category-theoretic) monad M in a category C: i]A:A-4 MA, where A is an object in C. We denote this analogy by r e t u r n ~ 77. Unfortunately, no such obvious comparison between » = and yx exists. There is, however, a Haskell function called j o i n that is defined in the Monad module. It has the following type declaration: j o i n :: Monad m => m (m a) -> m a, which is indeed analogous to the domain and codomain of H : HA : M2A -> MA. That is, j o i n ~ a.-51 Chapter 4, Equivalence The action of j o i n is to remove one layer of nesting of a monadic value. As is the case for r e t u r n and » = , the definition of j o i n is particular to the monad under consideration. In the case of Maybe, for example, the definition of j o i n is given by: j o i n :: Maybe (Maybe a) -> Maybe a j o i n Noth ing = Noth ing j o i n ( Ju s t Nothing) = Noth ing j o i n ( Jus t ( Jus t x ) ) = Jus t x Since j o i n (along with re tu rn ) is another direct link between Haskell functions and category-theoretic monad maps, if we can display an explicit connection between j o i n and >>=, then we wil l have the desired translation between the Haskell and category-theoretic formulations of monads! Continuing with the Maybe example, recall that one equation in the original instance declaration of the Maybe monad is: Jus t xO » = f = f xO Consider the substitutions XQ = Just x and / = id in the above. We have: Ju s t ( Jus t x) >>= i d = i d ( Jus t x) = Ju s t x = j o i n ( Jus t ( Jus t x ) ) . This gives a first relationship between >>= and j o i n in the case of the Maybe monad. In fact, this relationship is the Maybe-specific case of the following general relation in Haskell. Given a monad m and a monadic element m (m x ) , we have: j o i n m (m x) = (m (m x) ) » = i d . That is, removing one monadic layer using the j o i n operation is exactly the same as extracting the element m x from the (outer level of the)monad and leaving it unchanged. Therefore, for any Haskell monad m defined using the >>= function, we can obtain the definition for j o i n corresponding to m via the above equality. To establish an equivalence between these functions, it remains to pro-vide a definition for >>= in terms of j o i n . There is a small and obvious catch, however. The function >>= accepts two arguments, one of which is a function, whereas j o i n is a function from a double-layered monadic object to a monadic object. Also note that every (category-theoretic) monadic map 52 Chapter 4. Equivalence \i is a natural transformation, which means it is defined on objects and re-turns a function. Clearly, if j o i n is to be used to define a monad, we must integrate functions into its defined behaviour. To do this, we recall the method fmap that was introduced in Section 1.5.1 in conjunction with the Functor type class; specifically fmap is a function that must be defined for any instance of Functor, and it pro-vides a means for functions defined outside a set of functor-type elements to act on functor-type elements. Let us assume a (presently unjustified) consistency between Haskell's class names Functor and Monad, and the category-theoretic definitions of those two terms: namely, that any instance of Monad must also be an instance of Functor. Then, fmap :: a -> b -> f a -> f b can be defined for both functors and monads f. Using fmap with this additional context, we have the following Haskell relation between » = and j o i n : x >>= f = j o i n (fmap f x ) . That is, for a particular monad m, if we are given a definition for j o i n and fmap, then we can obtain the definition for >>=. For example, assume the three equations constituting the Maybe defini-tion of j o i n given above. In addition, assume the following Maybe-definition for fmap: fmap :: a -> b -> Maybe a -> Maybe b fmap _ Noth ing = Noth ing fmap f ( Jus t x) = Jus t f x. We show that these five equations imply those two involving » = given in the original instance declaration of the Maybe monad as follows. Let f : : a -> Maybe b. To show the first equation: Noth ing >>= f = j o i n (fmap f Nothing) = j o i n Nothing = Nothing. For the second equation, since Ju s t x >>= f = j o i n (fmap f ( Jus t x ) ) , 53 Chapter 4. Equivalence we consider the following two cases: Case 1: f x = Noth ing We have, j o i n (fmap f ( Jus t x ) ) = j o i n ( Jus t (Noth ing)) = Noth ing = f x. Case 2: f x = Ju s t y In this case, Therefore, j o i n (fmap f ( Jus t x ) ) — f x, and the definitions for fmap and j o i n are sufficient to provide an instance declaration for Maybe. 4.1.1 Comparative Motivations for >>=, join, and _* We have now given the equivalence between >>= and j o i n . Using this equivalence along with Theorem 2.3.1, we can easily see the relationship between >>= and _*. Let m be a monad, x be a monadic element of type x : : m a, and f be a function of type f : : a -> m b. Then, as we have seen, x » = f = j o i n (fmap f x ) . Recall that a category-theoretic functor is defined on both objects and morphisms, and that Haskell's fmap can be thought of as corresponding to the part of a functor that is defined on mor-phisms. Therefore, if we think of m as a monad M in the category-theoretic sense, we have an analogy between fmap f x and (M(f))(x). Furthermore, given the type signatures of x and f, we see that fmap f x has return type m (m b). Thus, the map j o i n is analogous to pB and we have: where the last equality follows from Theorem 2.3.1. We thus have the fol-lowing relationship between >>= and _*: j o i n (fmap f ( Jus t x ) ) j o i n ( Jus t ( Jus t y ) ) Jus t y f x. j o i n (fmap f x) ~ iMB(Mf(x)) = (pBoMf)(x) = / * ( * ) , X » = f ~ f*{x). 54 Chapter 4. Equivalence Now that we have explicitly established equivalancy relationships be-tween » = , j o i n (or fi), and _*, the question remains as to why these dif-ferent operations were chosen in their respective contexts. We have already seen that Kleis l i triples, with _* as a means of composing operations, were nicely justifiable from a computational standpoint. In fact, the aforemen-tioned let-constructor (Section 2.4) corresponds directly to composition in a given Kleis l i category [10]. The let-constructor similarly provides a motivation for the characteriza-tion of >>=. A n expression of the form x >>= \ a —> y, where x and y are ex-pressions, is computationally described by the sequence of actions: perform computation x, bind a to the resulting value, and then perform computation y. This is analogous to the computational interpretation of the expression let a = x in y [17]. The » = function thus provides a means to implement impure/imperative sequential-style reasoning in a pure functional language. Finally, understanding the connections between these functions with /v, is useful, because the category-theoretic formulation of monads is given solely in terms of functors and natural transformations. This formulation is eas-ier to reason about, and integrate into the established abstract setting of category theory. 4.2 Monad Laws To complete our exploration of the equivalence between monads in Haskell and category theory, it remains to justify the use of fmap as a component in the characterization of » = in terms of j o i n . To do this, we propose a new set of monad laws as well as a definition for fmap in terms of >>=. We then prove the equivalence between the new laws and the original laws (M1)-(M3). 4.2.1 Alternate Laws We offer and discuss the following new set of monad laws involving the polymorphic Haskell functions fmap, i d , r e t u r n , and j o i n , and arbitrary functions f : : a -> b, g : : b -> c [17]: (LI) fmap i d = i d (L2) fmap (f . g) = fmap f . fmap g (L3) fmap f . r e t u r n = r e t u r n . f (L4) fmap f . j o i n = j o i n . fmap (fmap f ) (L5) j o i n . fmap j o i n = j o i n . j o i n 55 Chapter 4. Equivalence (L6) j o i n . fmap r e t u r n = i d (L7) j o i n . r e t u r n = i d The astute reader may immediately notice similarities between these laws and the mathematical relationships pertinent to category-theoretic monads. We have already introduced the functor laws (LI) and (L2) as being anal-ogous to the defining equations for a category-theoretic functor in Section 1.5.1. To make the analogy explicit, let F : C —> C be a functor, M : C —* C be a monad, x 6 Oc, and / : a —> b, g : b —> c € Ac• We have: fmap i d = i d ~ F(idx) = idpx fmap (f . g) = fmap f . fmap g ~ F{f o g) = F(f) o F(g). It is similarly easy to see that (L3) and (L4) correspond to the naturality conditions for rj : I —* M and p, : M2 —* M, respectively; that is, for any objects a, b € Oc, and any map between those objects / : a —> b £ Ac, we have: fmap f . r e t u r n = r e t u r n . f ~ Mf o rja = r/b fmap f . j o i n = j o i n . fmap (fmap f ) ~ (Mf) ° Ma = Mb ° M2f We expect the last three laws to correspond to the category-theoretic monad laws given by the standard commutative diagrams for monads. However, on examining (L5), it looks as though we should have: ? j o i n . fmap j o i n = j o i n . j o i n ~ p o Mp = p o p. Not only does the right-hand side of the similarity fail to correspond to the first category-theoretic monad law, but the composition p o p is not even defined! The apparent inconsistency is actually caused by the polymorphism of j o i n . The function j o i n can accept any object of the form m ( m a ) , in-cluding the case when a itself is a monadic type (for example, if a = m b). Thus, while it is important to mathematically distinguish between the func-tions p and pM, Haskell's polymorphic type system allows the name j o i n to stand for more than one function, each being technically distingusihed by the domain it is defined on. A n exemplary demonstration of (L5) using the list monad L helps to clarify the issue. In Section 1.5.1 we noted that, in the case of lists, fmap is equivalent to map. In Section 3.1 we gave the definition of » = for lists, which we can now use (informally) to recover j o i n as follows. Let 10, 11, 12,... , ln be lists of the same type, and form the list of lists [10, 11,.. . , l n ] £ L 2 . Then, 56 Chapter 4. Equivalence j o i n [10, 11,. . . , In] = [10, 11,. . . , In] » = i d = i d 10 ++ [11,12,..., In] » = i d = 10 ++ (11 ++ (12 ++ (••'• ++ I n ) ) - - - ) . A Haskell expression involving the concatenation of more than two lists is typically written in terms of the operation cone at :: [ [a]] -> [a]. The last equation in the above derivation is equivalent to 10 ++ (11 ++ (• • • ++ In ) ) - • •) = concat (10,12, . . . , l n ) . Thus, the instance of j o i n defined for lists is equivalent to concat. Giv ing the instance (L5) in terms of fmap and j o i n for lists, we have: concat . map concat = concat . concat. Recall that the type signature of map is map : : (a -> b) -> [a] -> [b]. Taken with the type signature of concat, this means that the type signature of the inner function on the left-hand side of the preceding equation is map concat : : [ [ [a] ] ] -> [ [a] ] . The return type of this function matches the input type of concat, so that the type signature of the composed function is concat . map concat :: [ [ [ a ] ] ] -> [a]. For example, the action of the left-hand side function can be demon-strated on the following "list of lists of lists": concat . map concat [ [ [ 1 , 2 ] , [ 1 , 2 ] , [ 3 , 4 , 5 ] ] , [ [ 1 , 3 ] , [ ] ] ] = concat [concat [ [ 1 , 2 ] , [ 1 , 2 ] , [ 3 , 4 , 5 ] ] , c o n c a t [ [ 1 , 3 ] , [ ] ] ] = concat [ [ 1 ,2 ,1 ,2 ,3 ,4 ,5 ] , [ 1 ,3 ] ] = [1 ,2,1,2,3,4,5,1,3] The apparent problem with the similarity for (L5) arose with respect to the composition j o i n , join </> u, o \±M, but we can see in the list example that the " M " — o r L in the case of l i sts—is accounted for in the polymorphism of concat. Explicit ly, a list of lists [ [a] ] 6 L 2 is equivalently a list [b] G L, where b has type [a]. As such, the compiler would recognize an element of [ [ [ a ] ] ] as simply a list and allow the polymorphic function concat to accept such an element as an input with the correct type. Thus, the map concat . concat also has type concat . concat : : [ [ [ a ] ] ] -> [a] and acts on the previously given member of L 3 as follows: concat . concat [ [ [ 1 , 2 ] , [ 1 , 2 ] , [ 3 , 4 , 5 ] ] , [ [ 1 , 3 ] , [ ] ] ] = concat [ [ 1 , 2 ] , [ 1 , 2 ] , [ 3 , 4 , 5 ] , [ 1 , 3 ] , [ ] ] = [ 1 ,2 ,1 ,2 ,3 ,4 ,5 ,1 ,3 ] , 57 Chapter 4. Equivalence which matches the evaluation of concat . map concat on the same list. This reasoning regarding polymorphism for concat generalizes to j o i n and similar reasoning applies to r e t u r n . Thus, the analogies between (L5) -(L7) and the category-theoretic monad laws do, in fact, hold: j o i n . fmap j o i n = j o i n . j o i n ~ fx o Mp — fj, o fiM j o i n . fmap r e t u r n = i d ~ fi o Mr) = id j o i n . r e t u r n = i d ~ /i o 7 7 M = id. 4.2.2 Law Equivalence We now show the equivalence of laws (L1)-(L7) with laws (M1)-(M3), given in Section 3.0.2. First, we assume that laws (L1)-(L7) hold, as well as the previously given definition of » = in terms of j o i n . To prove the laws imply (M l ) , we have: r e t u r n x >>= f = j o i n (fmap f ( r e t u r n x ) ) = j o i n ( r e t u r n (f x ) ) = ( j o i n , r e t u r n ) (f x) = i d (f x) = f x. For (M2), we have: n >>= r e t u r n = j o i n (fmap r e t u r n n) = ( j o i n . fmap r e t u r n ) n = i d n (L6) = n. Finally, we prove (M3), recalling that any single-variable function h can equivalently be expressed with Haskell syntax as either h or \x-> h x. We have: (n » = f ) » = g = ( j o i n (fmap f n)) >>= g = j o i n (fmap g ( j o i n (fmap f n)) = ( j o i n , fmap g . j o i n ) (fmap f n) = ( j o i n . j o i n , fmap (fmap g))( fmap f n) = ( j o i n . j o i n . fmap (fmap g) . fmap f ) n = ( j o i n . j o i n . fmap ((fmap g) . f ) ) n — ( j o i n . j o i n , fmap (\x -> fmap g (f x ) ) ) n = ( j o i n . fmap j o i n . fmap (\x -> fmap g (f x ) ) ) n = ( j o i n , fmap ( j o i n . (\x -> fmap g (f x ) ) ) ) n = ( j o i n , fmap (\x -> j o i n (fmap g (f x ) ) ) ) n (L3) (L7) (L4) (L2) (L5) (L2) 58 Chapter 4. Equivalence = ( j o i n , fmap (\x -> f £d&fcef g>^= in terms of j o i n ) = ( j o i n (fmap (\x -> f x » = g) n) = n » = (\x -> f x » = g). Thus, monad.laws (L1)-(L7) imply monad laws (M1)-(M3). For the converse, we assume laws (M1)-(M3), along with the definition for j o i n in terms of » = . In addition, we assume the following definition for fmap, given a function f : : a -> b and monadic element n : : m a : fmap f n = n >>= r e t u r n . f The proofs of the laws are then as follows: (LI): fmap i d n = n >>= r e t u r n . i d = n >>= r e t u r n = n (M2) fmap (f . g) n = n >>= r e t u r n . f .g = n » = (\x -> r e t u r n f (g x ) ) = n >>= (\x -> r e t u r n . f g x) = n » = (\x -> ( r e t u r n g x » = r e t u r n , f ) ) (M l ) = n >>= (\x -> ( r e t u r n . g x >>= r e t u r n . f ) ) = (n » = r e t u r n . g) » = r e t u r n . f (M3) = (fmap g n) >>= r e t u r n . f = fmap (fmap g n) = (fmap . fmap g) n (L3): fmap f . r e t u r n n = fmap f r e t u r n n = r e t u r n n >>= r e t u r n . f = r e t u r n . f n (M l ) 59 Chapter 4. Equivalence (L4): fmap . join n fmap f (join n) join n » = return . f (n » = id) » = return . f n » = (\x -> (id x » = return, f)) (M3) n » = (\x -> (x » = return, f)) n >>= (\x -> fmap f x) n » = (\x -> id (fmap f x)) n » = (\x -> (return (fmap f x) » = id)) (Ml) (n >>= return . fmap f) >>= id join (n >>= return . fmap f) join (fmap (fmap f) n) join . fmap (fmap f) n (join . fmap join) n = join (fmap join n) = join (n » = return . join) = (n >>= return . join) >>= id = n » = (\x -> (return . join x » = id)) (M3) = n >>= (\x -> (return (join x) » = id)) = n » = (\x -> id (join x)) (Ml) = n >>= (\x -> join x) = n » = (\x -> (x » = id)) = n » = (\x -> (id x » = id)) = (n » = id) » = id = join (n » = id) = join (join n) = j o i n . j o i n n (L6): (join . fmap return) n join (fmap return n) join (n >>= return . return) (n » = return . return) (n >>= return . return) >>= id 60 Chapter 4. Equivalence n » (\x -> ( r e t u r n . r e t u r n x >>= i d ) ) (\x -> ( r e t u r n ( r e t u r n x) » = i d ) ) (\x -> i d ( r e t u r n x ) ) (M3) n » n » (Ml) n » r e t u r n i d n (M2) (L7): ( j o i n r e t u r n ) n = j o i n ( r e t u r n n) = r e t u r n n » = i d = i d n (M l ) Therefore, laws (M1)-(M3) imply laws (L1)-(L7) and the two sets of monad laws are equivalent. Previously, we assumed a consistency between the Haskell class names Functor and Monad with part of the category-theoretic definition of a monad; namely, that every monad is a functor. Since we have shown the monad laws (M1)-(M3) to be equivalent to laws (L1)-(L7), with the latter set including the functor laws (LI) and (L2), we have also shown that our assumption is justified. In fact, we can use laws (M1)-(M3) to prove the definition of >>= in terms of j o i n as follows: n » = f = n » = (\x -> i d (f x ) ) = n » = (\x -> ( r e t u r n (f x) » = i d ) ) = n » = (\x -> ( r e t u r n . f x » = i d ) ) = (n » = r e t u r n . f ) » = i d = j o i n (n >>= r e t u r n . f ) = j o i n (fmap f n) Therefore—at last!—we can provide an alternate class declaration for Monad that looks very similar to the category-theoretic formulation of a monad, with r e t u r n ~ rj and j o i n ~ fi: c l a s s Functor m => Monad m where r e t u r n :: a -> m a j o i n : : m (m a) -> m a. 4.3 Concluding Connections 4.3.1 List in Translation We conclude by using our work with equivalences to tie together our knowledge of monads in Haskell with those in category theory. In Section 61 Chapter 4. Equivalence 3.1, Example 4, we showed that (M1)-(M3) hold for the list type constructor. In examining the alternate law formulations in Section 4.2.1, we saw that for the list monad L, fmap is given by map and j o i n by concat. Notably, the maps of the latter formulation seemed easier to understand and manipulate than the recursive definition of » = for lists. If we begin to translate to category-theoretic terms, we see that L is a functor which, given a Haskell type a, constructs the set of all lists of type a (denoted [a]). In other words, given a set X £ Ha sk , L X is the set of all possible lists that can be formed using elements in X, L2X is the set of all lists of lists, and so on. Further, we recall that r e t u r n for the List monad is given by r e t u r n x = [x], where x 6 X. Thus, given a set X G L, we define rjx by sending x i - > [x] and px by the concatenation of lists in LX. Note that the concatenation of lists does not entail 'discarding' repeated elements (as with, say, a union operation) or 'cancelling' elements in accord with some given relations (as for, say, invertible elements). Comparing this to Example 3, Section 1.3.2, we see that the List monad is none other than the free-forgetful semigroup monad! 4.3.2 Distributive Laws In many applications of monads in Haskell to structuring functional lan-guages, the desired monad is most easily conceived as a combination of simpler monads. For example, we considered using monads to facilitate error handling (the Maybe monad) and to count the number of operations performed during a calculation (state updates). It is easy to see the desir-ability of being able to combine these monads so that if an error occurred during a calculation in which a counter was running, then the error would be handled properly. In general, it is not the case that when endofunctors comprising monads are composed, the result is another monad. However, there is a category-theoretic concept that formalizes the cases when this does happen; the con-cept being that of the distributive laws for monads. A distributive law for monads is a means by which the functorial composition of two monads can be made into a more complex, combined monad. The idea is a similar to viewing the ordinary distributive law of multiplication over addition as a means by which abelian groups and monoids are combined into the more complex structure of rings. Let M i — ( M i , 771, p-i) and M 2 = (M 2,772, ^2) be monads on a category C. A distributive law of M i over M 2 is a natural transformation A : M i o M 2 —> M 2 o M i for which the following diagrams commute [1]: 62 Chapter 4. Equivalence Mx Mirj 2 MXM2 Mx M2Mi M2 T]lM2 MXM2 M2 M2Mi MXM2 M2MXM2 -^U M2MX M i 112 MXM2 112 Mi M2MX 2A,„ MXM2MX M2M\ M(M2 MXM2 M21H M2MX A distributive law A of Mx over M2 gives rise to the composite or com-bined monad defined by A, given by M2MX = (M2Mx,r)M2M\HM2Ml), where the composite maps r / M 2 M l and u.M2Ml are defined by: Mi =-> M 2Mi 7 7 M 1 D M 2 M 2 M 2 ? ? M l 1 M 2Mi M 2 2 Mi M 2Mi Ic r>M2M\ M2MX M2MXM2MX M 2 A M l > M 2 2M 2 M 2Mj p,M2M2 M2M\ M 2Mi The natural question for us to ask is: Can we implement this theoretical definition to combine certain monads in Haskell? The answer is "Yes!" and we show how the distributive laws can be used to define a monad ML, where M is an arbitrary monad and L is the list monad. 63 Chapter 4. Equivalence We begin by using the same essential idea that we explored in Section 4.2.1; namely, we draw analogies between the category-theoretic distributive laws and Haskell code. The difference here, is that while in Section 4.2.1 we had sets of laws from category theory and Haskell, and we justified an analogy between them, in this case we use a set of category-theoretic laws to motivate, v ia analogy, a set of relations between Haskell functions. At this stage, we feel confident enough to blend notations for conve-nience. Thus, we let A be a Haskell function with type signature A : : L (M a) -> M ( L a ) , as well as if : : a -> M a, /xM : : M (M a) -> M a and m M : : (a -> b) -> M a -> M b be the monad maps for M, and rf', / j L and m L denote the monad maps for L. Then the first analogous Haskell relation corresponds to the naturality of A : (DO) A . m L ( m M f ) = m M ( m L f ) . A , where f is an arbitrary function with type signature f : : a -> b. By let-ting M\ and M2 correspond to L and M, respectively, in the diagrams above, we can infer an analogous set of Haskell distributive laws. For example, the equation corresponding to the second diagram given in the definition of a distributive law is A o J]\M2 = M2r)\. TO come up with a corresponding Haskell law, we: (i) let the fmap methods defined for the instances L and M—namely, m L and m M , respectively—replace the functor maps M\ and M2, respectively; (ii) let the r e t u r n methods for L and M—namely, r?L and rf1 , respectively—replace the monad units rji and n2, respectively; (iii) ac-count for Haskell's polymorphic type system (see Section 4.2.1 for a detailed introduction of the manifestation of polymorphism in this sort of context). The Haskell function m M can be thought of as accepting two arguments: a function of type a -> b and a monadic element of type M a. Thus, we convert the expression M2rj\ to the corresponding Haskell function m M nL , where the type signatures of m M : : (a -> b) -> M a -> M b and rf' : : a -> L a imply that m M rf' accepts an argument of type M a and has return type M ( L a ) . For the left-hand side of the distributive law equation under consideration, we convert A o r\\M2 to A . r?L . In the category-theoretic case, we have Ao r ] \M 2 as a map from M2 to M2M\. In the Haskell version, the polymorphism of rf' means that we do not need to explicitly include the inner monad map M2 in the law's formulation; rather, we just note that rf' can accept monadic-typed arguments. Moreover, the type signature of A : : L (M a) -> M (L a) guarantees that we must give nl an argument of type M a, so that its return type wi l l be L (M a) (which corresponds to the input type of A). Thus, the Haskell version of this distributive law equation is A . nL = m M rf" . 64 Chapter 4. Equivalence We can similarly translate the remaining distributive law equations. In summary, the category-theoretic distributive laws give rise to the following relations in Haskell: (DI) A nh - m M (D2) A m L r?M = rf (D3) A m L / / = M M m M A . A (D4) A M L = m M u1 . A . m L It is important to note that to assume that these analogous Haskell laws hold, we must first assume that the Haskell function A exists. What makes the case of L over an arbitrary M special is that such a distributive law function A does indeed exist. Showing this involves working with a so-called Haskell " fo ld" function, and defining a sort of Cartesian product for lists. Interested readers are referred to [7] for details. B y continuing with our stated assumptions, we propose that the follow-ing 3-tuple defines a combined monad defined by A. P r o p o s i t i o n 4.3.1. The triple defined by: unifL = rf . nL fmapKL f = mH ( mL f ) joinML = mH uL . // mH A is a combined monad, ML, in Haskell. Proof. To prove the 3-tuple (ML, e t a M L , jo in M L ) is a monad, we must show that the maps un i t M L , fmap M L , and j o i n M L satisfy (L1)-(L7), given that this same set of laws holds for each of M and L, and that (D0)-(D4) also hold. We have: (LI): fmap 1 ML id m M ( m L id m M ( id ) id (L2): fmap M L ( f . g ) m M ( m L f . g) m M ( m L i . m L g ) m M m L f = fmap M L f . fmap M L g M T m m g ML 65 Chapter 4. Equivalence (L3): fmap M L ( f . un i t M L ) = m > L ( f nL . f 77" = unit 1 ML r ? L ) ) Note that our particular interest in combining the list monad with an ar-bitrary monad is highlighted in the remaining laws, where we assume the existence of A for L over M. (L4): fmap M L . j o i n M L = m M ( m L f ) . m M pL . pK m M A m M ( m L f . fiL ) . fjK . m M A = M M m M ( m M ( m L f . pL ) ) . m M A = A*H m M ( m M ( m L f . ph ) . A ) = M M m M ( m M ( pL . m L ( m L f ) )• A ) = M M m M ( m M pL . m M ( m L ( r n L f ) ) . A ) M M mM ( m H ph ) . m M ( m M ( m L ( m L f ) ) A ) = m M A* L- pH . m M ( m M ( m L ( r n L f ) ) . A ) DO) m M M L - /Jm . m M ( A . m L ( m M ( m L f ) ) ) = M m p" . m M A . m M ( m L ( m M ( m L f ) ) ) = j o i n M L . map M L ( map M L f ) (L6): jo in ML unit ML _ m p . p m M pL . p" = m (D 1) M = m - m M = m M id m M A . r/M nH . A T?L p,L . id . A nL M ,„L p . m ( M L • VL ( i d ) 66 Chapter 4. Equivalence (L7): join ML m id = m u. M T = m \x (D2) „ L — m ur m LI ->ML f ML map"" unit MM m M A . m M ( m L ( rf . r,L ) ) m M ( A . m L ( rf . nL ) ) M M m M m M ( A . m L 77' M m i d ) m M ( 77" . m L ry1- ) m M 77" . m M ( m L nL ( m L r?L ) • • Ml I join . join = m M /vM m M A . m M / / L . M M m M A = m M M L - HH . m M ( A . fi L ) AiM . m M A = . m M ( m" M L ) . m M ( A . fJ,L ). fjK . m M A = m M ( m M / i L . A . u.L ) • // . m M A = i<H . M» m M ( m M ( m M /t L . A . /xL ) ) • m M A = M« . fiK m M ( m M ( m M M L . A • M L ) • A ) (D4) A*M • M M . mM ( m M ( m M m M u.L . A . m L A ) . A ) = . / i M . m M ( m M ( m M M L - m M uL . A ) . m M ( m L A ) . A ) (DO) • M M . mM ( m M ( m M m M M L • A ) A . m L ( m M A ) ) = . m M ( m M ( m M m M u.L ) . m M A . A . m L ( m M A ) ) = M M • M M m M ( m M ( m M u L . m M uL ) ) . m M ( m M A . A . m L m" A ) ) = . m M ( m M u,L . m M u.h ) . / i M . m M ( m M A . A . m L m M A ) ) = . m M ( m M ( . ,, L ) ) • // . m M ( m M A . A . m L ( m M A ) ) = M m . HL ) • M M • M M . m M ( m M A . A . m L ( m M A ) ) = m M ( / / . /vL ) . //" . m M . m M ( m M A . A . m L ( m M A ) ) = m M U L . LIL ) . LIK . m M ( A* M . m M A . A . m L ( m M A ) ) (D3) m M ( M L . LIL ) . /zM • m M ( A . m L M M • m L ( m M A ) ) = m M U L . Ai L ) • M M • m M ( A . m L ( LIK . m M A ) ) = M M . m M ( m M ( u.L . ) ) • m M ( A . m L ( /J* . m M A ) ) = M M . m M ( m M ( M L • M L ) . A . m L ( // . m M A ) ) = M M . m M ( m M ( / U L . m L . A . m L ( M M • m M A ) ) 67 Chapter 4. Equivalence u.H . m M ( m M /xL . m M ( m L fj,L ) . A . m L ( /aM . m M A ) ) =° } M M . m M ( m M u,L • A . m L ( m M M L ) . m L ( M M . m M A ) ) /x" . m M ( m M fiL • A • m L ( m M u.L . u" . m M A ) ) /aM . m M ( m M n l . A ) . m M ( m L ( m M / i L . /xM . m M A ) ) // . m M ( m M fiL ) • m" A . m M ( m L ( j o i n M L ) ) m M u,L . / i M m M A . fmap M L ( j o i n M L ) = j o i n M L . fmap M L ( j o i n M L ) Thus, the 3-tuple (ML, e t a M L , j o i n M L ) is a monad. • 68 Bibl iography M. Barr and C. Wells, Toposes, Triples, and Theories. Springer-Verlag, 1985. M . Barr and C. Wells, Category Theory for Computing Science. Prentice Hal l , 1990. J. Beck, Distributive laws. Lecture Notes in Mathematics, 80:119-140, Springer, 1969. H. Daume III, Yet Another Haskell Tutorial. Ha l Daume, 2002-2006. R. Goldblatt, Topoi: The Categorical Analysis of Logic, Studies in Logic and the Foundations of Mathematics, Volume 98. North-Holland Publishing Company, 1979. P. Hudak, J . Peterson, and J . H. Fasel, A Gentle Introduction to Haskell 98. Paul Hudak, John Peterson and Joseph Fasel, 1999. D. K ing and P. Wadler, Combining Monads. In Glasgow Workshop on Functional Programming, Ayr, July 1992. S. Mac Lane, Categories for the Working Mathematician. Springer-Verlag, 1971. G. Michaelson, An Introduction to Functional Programming Through Lambda Calculus. Addison-Wesley Publishers Ltd., 1989. E. Moggi, Computational lambda-calculus and monads. In Sympasium on Logic in Computer Science, Asilomar, California; I EEE , June 1989. E. Moggi, A n abstract view of programming languages. Course notes, University of Edinburgh, 1989. E. Moggi, Notions of computations and monads. Information and Com-putation, 93:55-92, 1989. 69 Bibliography [13] M . Pierce, Basic Category Theory for Computer Scientists. The M I T Press, 1991. [14] F. Rabhi and G. L&p&lme, Algorithms: A Functional Programming Ap-proach. Pearson Education Limited, 1999. [15] J . C. Reynolds, Using category theory to design implicit ' conversions and generic operators. In N. D. Jones, editor, Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation, number 97 in Lecture Notes in Computer Science. Springer-Verlag, January 1980. [16] P. Wadler, Comprehending Monads. In Conference on Lisp and Func-tional Programming, Nice, France; A C M , June 1990. [17] P: Wadler, Monads for functional programming. In M. Broy, editor, Marktoberdorf Summer School on Program Design Calculi, Springer Verlag, N A T O ASI Series F: Computer and systems sciences, Volume 118, August 1992. [18] P. Wadler, The essence of functional programing (invited talk). In 19'th Symposium on Principles of Programming Languages, Albuquerque, New Mexico; A C M , January 1992. 70
- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Notions of category theory in functional programming
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
Notions of category theory in functional programming Gammon, Shauna C. A. 2007
pdf
Notice for Google Chrome users:
If you are having trouble viewing or searching the PDF with Google Chrome, please download it here instead.
If you are having trouble viewing or searching the PDF with Google Chrome, please download it here instead.
Page Metadata
Item Metadata
Title | Notions of category theory in functional programming |
Creator |
Gammon, Shauna C. A. |
Publisher | University of British Columbia |
Date Issued | 2007 |
Description | We present a detailed examination of applications of category theory to functional programming languages, with a primary focus on monads in Haskell. First, we explore E. Moggi's work in categorical semantics, which provides the theoretical foundation for employing monads in functional languages. In particular, we examine his use of Kleisli triples to model notions of computation. We then study P. Wadler's implementation of Moggi's ideas as a means to mimic side-effects in the purely functional language Haskell. We explicitly demonstrate the connections between Kleisli triples, categorytheoretic monads, and Haskell monads. It is our principal aim to provide a coherent translation between the abstracted concept of monads that exists in category theory, and the formulation of monads as type-constructors that is implemented in Haskell. |
Genre |
Thesis/Dissertation |
Type |
Text |
Language | eng |
Date Available | 2011-02-24 |
Provider | Vancouver : University of British Columbia Library |
Rights | For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
DOI | 10.14288/1.0080357 |
URI | http://hdl.handle.net/2429/31756 |
Degree |
Master of Science - MSc |
Program |
Mathematics |
Affiliation |
Science, Faculty of Mathematics, Department of |
Degree Grantor | University of British Columbia |
Campus |
UBCV |
Scholarly Level | Graduate |
AggregatedSourceRepository | DSpace |
Download
- Media
- 831-ubc_2007-0409.pdf [ 2.96MB ]
- Metadata
- JSON: 831-1.0080357.json
- JSON-LD: 831-1.0080357-ld.json
- RDF/XML (Pretty): 831-1.0080357-rdf.xml
- RDF/JSON: 831-1.0080357-rdf.json
- Turtle: 831-1.0080357-turtle.txt
- N-Triples: 831-1.0080357-rdf-ntriples.txt
- Original Record: 831-1.0080357-source.json
- Full Text
- 831-1.0080357-fulltext.txt
- Citation
- 831-1.0080357.ris
Full Text
Cite
Citation Scheme:
Usage Statistics
Share
Embed
Customize your widget with the following options, then copy and paste the code below into the HTML
of your page to embed this item in your website.
<div id="ubcOpenCollectionsWidgetDisplay">
<script id="ubcOpenCollectionsWidget"
src="{[{embed.src}]}"
data-item="{[{embed.item}]}"
data-collection="{[{embed.collection}]}"
data-metadata="{[{embed.showMetadata}]}"
data-width="{[{embed.width}]}"
data-media="{[{embed.selectedMedia}]}"
async >
</script>
</div>
Our image viewer uses the IIIF 2.0 standard.
To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0080357/manifest