On Monday 02 July 2007, Andrew Coppin wrote:
What were monads like before they became a Haskell language construct?
Is Haskell's idea of a "monad" actually anywhere close to the original mathematical formalism?
Just being randomly curiose...
Curiosity can be a dangerous thing . . . Short answer: they're equivalent, or rather, Haskell monads are equivalent to what Haskellers would naturally write when translating mathematical monads into Haskell. If you really want to know the details (it's a fascinating subject once you start understanding it), go read a couple or three good books on category theory; I'm sure someone else here can give you a better reading list than I can off the top of my head. Building up to the idea of a monad in category theory, with proper examples and whatnot, requires a full textbook; in particular, /Toposes, Triples, and Theories/, where I learned the concept and which wants to actually do something interesting with them, is required to compress the categorical preliminaries to a point where I needed constant reference to other books just to understand the basic concepts. Nevertheless, if you really want the high points: Monads come from a branch of abstract mathematics called /category theory/, which was invented, originally, to provide a mathematical characterization of polymorphic functions (or, rather, of the uniform nature of certain functions, which FPers would characterize as a form of polymorphism). A category is a 6-tuple (objects, arrows, domain, codomain, id, compose) where objects and arrrows are arbitrary classes, domain and codomain are mappings from arrows to objects, id is a mapping from objects to arrows such that domain (id alpha) = alpha codomain (id alpha) = alpha and compose is an associative partial binary operator on arrows with the images of id as units, such that compose f g is defined whenever domain f = codomain g, and domain (compose f g) = domain g codomain (compose f g) = codomain f Following standard practice, I will write f : alpha -> beta for domain f = alpha codomain f = beta and f . g for compose f g. (Standard practice in category theory is I believe to write composition as juxtaposition (like application in Haskell, but associative), but I'm not going that far to make the notation look more Haskell-like). Given that A and B are categories, a /functor/ F from A to B is a pair of mappings (F_objects, F_arrows) (both generally written F in practice) from objects of A to objects of B and arrows of A to arrows of B, respectively, such that domain (F a) = F (domain a) codomain (F a) = F (codomain a) compose (F a) (F b) = F (compose a b) id (F a) = F (id a) Given two functors, F, G : A -> B, a natural transformation h : F -> G is a mapping h from objects of A to arrows of B such that h alpha : F alpha -> G alpha h beta . F f = F f . h alpha (forall f : alpha -> beta) Given a category C, a monad in C is a triple (F, eta, mu) of a functor F : C -> C, a natural transformation eta : Id -> F, where Id is the identity functor, and a natural transformation mu : F . F -> F, where composition of functors is defined component-wise, satisfying the additional laws mu . F mu = mu . mu mu . eta = id = mu . F eta When translating category theory into Haskell, objects are taken to be types and arrows functions; domain, codomain, id, and compose are defined the way you would expect. A functor is represented by class Functor in the standard prelude; an instance consists of a data type constructor F, which is the only mapping on types supported by Haskell, and a function fmap :: (alpha -> beta) -> (F alpha -> F beta) (remember currying!) corresponding to the arrow map. A natural transformation is a polymorphic function f :: F alpha -> G alpha such that fmap g . f = f . fmap g for all functions g. This is (at least sometimes) provable for arbitrary polymorphic functions (as long as they don't use seq!), but I'm not sure of the details of this. At any rate, doing so isn't certainly isn't necessary. Translating the definition of a monad into Haskell using this terminology would give us class Functor m => Monad m where return :: alpha -> m alpha join :: m (m alpha) -> m alpha (join, by the way, is one of the most under-appreciated of Haskell library functions; learning it is necessary both for true mastery of Haskell monads). The complete collection of class laws (including the natural transformation laws) is fmap g . return = return . g fmap g . join = join . fmap (fmap g) join . fmap join = join . join join . return = id = join . fmap return (Note the essential similarity of these laws to those given above). Haskell, of course, actually gives us class Monad m where return :: alpha -> m alpha (>>=) :: m alpha -> (alpha -> m beta) -> m beta The relationship between these two signatures is given by the set of equations fmap f a = a >>= return . f join a = a >>= id a >>= f = join (fmap f a) and the monad laws in Haskell are return x >>= f = f x a >>= return = a (a >>= f) >>= g = a >>= \ x -> f x >>= g We can take the relationship given above as definitional, in either direction, and derive the appropriate set of laws. Taking fmap and join as primitive, we get return x >>= f = join (fmap f (return x)) = join (return (f x)) = f x a >>= return = join (fmap return a) = a (a >>= f) >>= g = join (fmap g (join (fmap f a))) = join (join (fmap (fmap g) (fmap f a))) = join (fmap join (fmap (fmap g) (fmap f a))) = join (fmap (join . fmap g . f) a) = a >>= join . fmap g . f = a >>= \ x -> join (fmap g (f x)) = a >>= \ x -> f x >>= g Taking (>>=) as primitive, we get fmap f (return x) = return x >>= return . f = return (f x) fmap f (join a) = (a >>= id) >>= return . f = a >>= \ x -> id x >>= return . f = a >>= \ x -> x >>= return . f = a >>= fmap f = a >>= \ x -> id (fmap f x) = a >>= \ x -> return (fmap f x) >>= id = (a >>= return . fmap f) >>= id = join (fmap (fmap f) a) join (join a) = (a >>= id) >>= id = a >>= \ x -> x >>= id = a >>= \ x -> join x = a >>= \ x -> return (join x) >>= id = (a >>= return . join) >>= id = join (fmap join a) join (return a) = return a >>= id = id a = a join (fmap return a) = (a >>= return . return) >>= id = a >>= \ x -> return (return x) >>= id = a >>= \ x -> return x = a >>= return = a This is less general than the category theory version, and seq creates problems with some of these equations (or at least with proving that any of them hold for real programs!), but using the normal methods of Haskell equational reasoning (assume all values are total and finite, all functions preserve totality and finiteness, and the context preserves totality and finiteness, and using = on functions to mean equality on total and finite arguments), it works; Haskell monads are just an alternative formulation for a (not-quite-semantics-preseving) transliteration of category theory monads into the Haskell setting. Jonathan Cast http://sourceforge.net/projects/fid-core http://sourceforge.net/projects/fid-emacs