Frank Atanassow wrote:
G Murali wrote (on 09-03-01 00:43 +0000):
I'm new to this monads stuff.. can you tell me what it is simply ? an example would be highly appreciated.. i want it is very very simple terms please..
A monad on category C is a monoid in the category of endofunctors on C.
Is that simple enough? ;)
No? Then see "Using Monads" at http://haskell.org/bookshelf/
(Sorry, I just couldn't resist!)
Uh-oh. I'm a junior categorist and toposopher and I confess that all my few attempts to understand what Haskell's monads have to do with the categorical notion of a monad have failed more or less miserably. Can someone point me to a relevant paper, or give a quick explanation? Thanks in advance, and sorry for the dumb question, Eduardo Ochs http://angg.twu.net/ edrx@inx.com.br
Eduardo Ochs wrote:
Frank Atanassow wrote:
G Murali wrote (on 09-03-01 00:43 +0000):
I'm new to this monads stuff.. can you tell me what it is simply ? A monad on category C is a monoid in the category of endofunctors on C. Is that simple enough? ;)
Uh-oh. I'm a junior categorist and toposopher and I confess that all my few attempts to understand what Haskell's monads have to do with the categorical notion of a monad have failed more or less miserably. Can someone point me to a relevant paper, or give a quick explanation?
The relevant category for Haskell is the one in which objects are types and arrows are functions. The identity arrow for object 't' is 'id' instantiated at type 'id :: t -> t', and composition of arrows is function composition. Single-argument type constructors like '[]', Maybe, etc., map types to types (objects to objects). If equipped with a suitable function 'fmap :: (a -> b) -> (T a -> T b)' (i.e., taking arrows to arrows), they form a categorical functor (specifically, an endofunctor), and can be made instances of the Haskell Functor class. Polymorphic functions are natural transformations: a function 'f :: forall a. F a -> G a' gives, for each object (type) 't' an arrow from 'F t' to 'G t'. One of the definitions of a monad is: a functor M equipped with two natural transformations: eta : Id -> M and mu : MM -> M (obeying certain laws). Translating this into Haskell, this is a type constructor M along with polymorphic functions 'return :: forall a. a -> M a' and 'join :: forall a. M (M a) -> M a' (again obeying certain laws). The 'join' function makes intuitive sense for "container-like" monads like List (join = concat :: [[a]] -> [a]) and Maybe (join (Just (Just x)) = Just x ; join Just Nothing = join Nothing = Nothing). For other monads like state transformers, parsers, and IO it's less intuitive, so it's more common to define Haskell Monads in terms of the "bind" operation ">>=", (>>=) :: (M a) -> (a -> M b) -> M b which is a close relative of the Kleisli composition operator. Join, bind, and Kleisli composition are all interdefinable: (>>=) :: (M a) -> (a -> M b) -> M b join :: M (M a) -> M a o :: (b -> M c) -> (a -> M b) -> (a -> M c) m >>= k = join (fmap k m) join mm = mm >>= id f `o` g = join . fmap f . g Wadler's "Comprehending Monads" gives a very good presentation using the fmap/return/join formulation (called map/unit/join in that paper). "The Essense of Functional Programming" is another very good presentation using the return/>>= formulation (there called "unitM/bindM"). See <URL: http://cm.bell-labs.com/cm/cs/who/wadler/topics/monads.html > --Joe English jenglish@flightlab.com
From: Joe English <jenglish@flightlab.com> Date: Sat, 10 Mar 2001 09:34:28 -0800
The relevant category for Haskell is the one in which objects are types and arrows are functions. The identity arrow for object 't' is 'id' instantiated at type 'id :: t -> t', and composition of arrows is function composition.
Single-argument type constructors like '[]', Maybe, etc., map types to types (objects to objects). If equipped with a suitable function 'fmap :: (a -> b) -> (T a -> T b)' (i.e., taking arrows to arrows), they form a categorical functor (specifically, an endofunctor), and can be made instances of the Haskell Functor class.
Polymorphic functions are natural transformations: a function 'f :: forall a. F a -> G a' gives, for each object (type) 't' an arrow from 'F t' to 'G t'.
One of the definitions of a monad is: a functor M equipped with two natural transformations: eta : Id -> M and mu : MM -> M (obeying certain laws). Translating this into Haskell, this is a type constructor M along with polymorphic functions 'return :: forall a. a -> M a' and 'join :: forall a. M (M a) -> M a' (again obeying certain laws).
However, in some expositions of category theory, the usefulness of monads is justified because they 'belong' to a certain adjunction. In Haskell you can't express the adjunction, only the monad, which may take a little getting used to. But how about the related concept of an M-algebra? That is, a type T and a function 'xi :: M T -> T' so that these laws hold: xi . eta === id xi . (fmap xi) === xi . mu As it is, the List monad expresses the idea of the free monoid over a set. A List-algebra is of course a general monoid: e :: T e = xi [] (#) :: T -> T -> T (#) = \x y.xi [x y] (And 'M a' is an M-algebra for any a, using xi = join). And what you do every time you write 'foldl 0 +' in a program is to give the xi of the additive monoid structure on the Num types. Would it be useful to have functions that were polymorphic over List-algebras? (Not that I have any idea how that might be possible to express in Haskell). Lars Mathiesen (U of Copenhagen CS Dep) <thorinn@diku.dk> (Humour NOT marked)
Lars Henrik Mathiesen wrote (on 10-03-01 20:35 -0000):
However, in some expositions of category theory, the usefulness of monads is justified because they 'belong' to a certain adjunction.
You can regard a monad as arising from a particular adjunction but, although every adjunction determines a unique monad, the converse is not true. In fact, the collection of resolutions for a monad forms a category with adjunctions as objects and certain functors as arrows. The adjunction which gives rise to the Kleisli category is initial in this category. The terminal object is called the Eilenberg-Moore category and it has as objects M-algebras, like your `xi', and as arrows M-algebra homomorphisms.
In Haskell you can't express the adjunction, only the monad, which may take a little getting used to.
I've been looking at this recently to find some canonical way to express how to `deconstruct' monadic terms (i.e., how to run them). The idea is that you build up monadic terms in the Kleisli category, somehow describe a resolution, then use the initiality property of the Kleisli category to map the terms to the category of the resolution, where you can use the adjunction to destructure them.
But how about the related concept of an M-algebra? That is, a type T and a function 'xi :: M T -> T' so that these laws hold: xi . eta === id xi . (fmap xi) === xi . mu
If you reverse the sense of the last equation and regard the monad primitives as constructors: xi (Eta x) = x xi (Mu m) = xi (fmap xi m) then this starts to look like a pattern-matching definition for folding a monad regarded as an algebra. In fact, you can express the operators this way in Haskell if you use are willing to use a nested datatype: data M a = Eta a | Mu (M (M a))
Would it be useful to have functions that were polymorphic over List-algebras? (Not that I have any idea how that might be possible to express in Haskell).
I dunno if it is useful for List-algebras, but if you take your monad M as the substitution monad generated by a term signature, then the the resolutions of the monad can be regarded as a way of factoring M into a composition of signatures which (I think) represent the values and redexes of the term language. The Kleisli and E-M categories are extremal cases. In the Kleisli category the redex functor is trivial; I think this is this is why you can use it to pass around computations. In the E-M category, the value functor is trivial, but I'm not sure what this means precisely yet. For intermediate cases, you get a particular choice of normal forms. What I'm thinking is that an M-algebra for a language M gives you a way of extending a denotational description of the normal forms to one for the entire language, which is automatically sound for the equational theory. Which sounds useful to me for writing interpreters. -- Frank Atanassow, Information & Computing Sciences, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-3261 Fax +31 (030) 251-379
Date: Mon, 12 Mar 2001 17:16:29 +0100 From: Frank Atanassow <franka@cs.uu.nl>
Lars Henrik Mathiesen wrote (on 10-03-01 20:35 -0000):
However, in some expositions of category theory, the usefulness of monads is justified because they 'belong' to a certain adjunction.
You can regard a monad as arising from a particular adjunction but, although every adjunction determines a unique monad, the converse is not true. In fact, the collection of resolutions for a monad forms a category with adjunctions as objects and certain functors as arrows. The adjunction which gives rise to the Kleisli category is initial in this category. The terminal object is called the Eilenberg-Moore category and it has as objects M-algebras, like your `xi', and as arrows M-algebra homomorphisms.
Yes, I was aware of that --- I should perhaps have said that there's typically a 'motivating' adjunction, often one involving a forgetful functor. Which is generally different from the one into the Kleisli category. I read the rest of your post with great interest too, though I need to work at it a bit before I think I understand all of it. MacLane is off the shelf, and section IV.7 is scheduled to be worked though come the weekend. My own thoughts were a bit less ambitious, and I found out that Haskell (at least hugs -98 +o) will in fact do what I had in mind:
module Algebra () where
class Monad m => Algebra m a where xi :: m a -> a
instance (Num a) => Algebra [] a where xi = foldl (+) 0
instance Algebra [] [a] where xi = concat
unit :: Algebra [] a => a unit = xi []
(#) :: Algebra [] a => a -> a -> a x # y = xi [x, y]
Prelude> :load Algebra.lhs Reading file "Algebra.lhs": Hugs session for: /usr/local/share/hugs/lib/Prelude.hs Algebra.lhs Algebra> unit :: Int 0 Algebra> unit :: Float 0.0 Algebra> unit :: [Char] "" Algebra> "foo" # "bar" "foobar" Algebra> (1::Int) # 2 # 3 6 But perhaps I'm just easily amused. Lars Mathiesen (U of Copenhagen CS Dep) <thorinn@diku.dk> (Humour NOT marked)
participants (4)
-
edrx＠inx.com.br -
Frank Atanassow -
Joe English -
Lars Henrik Mathiesen