Ok, You wrote But please, let's keep one foot in the real world if possible.
Monads were invented to solve the "how do I do imperative programming in a pure functional language" problem.
This is more than a little revisionist. Monads have been the subject of mathematical study before people had an inkling that they might apply to problems in computer science. Moggi didn't invent them, but noticed that they might have an application to issues of composition in computation. It is really intriguing that they do such a remarkable job of organizing notions of update and were not invented with this application in mind. So, revising history thus would be a real loss. Best wishes, --greg -- L.G. Meredith Managing Partner Biosimilarity LLC 505 N 72nd St Seattle, WA 98103 +1 206.650.3740 http://biosimilarity.blogspot.com
I wrote: But please, let's keep one foot in the real world if possible. Monads were invented to solve the "how do I do imperative programming in a pure functional language" problem. On 2 Aug 2007, at 7:05 pm, Greg Meredith wrote:
This is more than a little revisionist. Monads have been the subject of mathematical study before people had an inkling that they might apply to problems in computer science. Moggi didn't invent them, but noticed that they might have an application to issues of composition in computation. It is really intriguing that they do such a remarkable job of organizing notions of update and were not invented with this application in mind. So, revising history thus would be a real loss.
I apologise for the unclarity of what I wrote. I should have said something like "Monads-in-computing were adopted to solve..." It is considerably more than a little revisionist to identify Haskell monads with Category Theory monads. Quoting the Wikipedia article on monads: "If F and G are a pair of adjoint functors, with F left adjoint to G, then the composition G o F will be a monad. Note that therefore a monad is a functor from a category to itself; and that if F and G were actually inverses as functors the corresponding monad would be the identity functor." So a category theory monad is a functor from some category to itself. How is IO a a functor? Which category does it operate on? What does it do to the points of that category? What does it do to the arrows? Let's turn to the formal definition: "If C is a category, a monad on C consists of a functor T : C → C together with two natural transformations: η : 1 → T (where 1 denotes the identity functor on C) and μ : T2 → T (where T2 is the functor T o T from C to C). These are required to fulfill [some] axioms:" What are the natural transformations for the IO monad? I suppose there is a vague parallel to return and >>=, but that's about all you can claim for it. If we are not to be revisionist, then we must admit that Haskell monads were *inspired* by category theory monads, but went through a couple of rounds of change of notation before becoming the Monad class we know and love today. What we have *was* invented for functional programming and its category theory roots are not only useless to most programmers but quite unintelligible. We cannot (and I do not) expect our students to *care* about monads because of their inspiration in category theory but because they WORK for a problem that had been plaguing the functional programming community for a long time. This is why I say you must consider your audience. One of the unusual things about Haskell is the strength and breadth of its links to theory and the number of people who are *interested* in that theory as an aid to finding ways to make new kinds of programming thinkable. I don't suppose we'd have had Arrows without this kind of background. But few students in most Computer Science departments take category theory, and those people need monads explained in terms they will be able to understand and to grasp the *practical* significance of. Once they catch the Haskell "spirit" they may well become interested in the theory, but that stuff doesn't belong in tutorials.
ok wrote:
It is considerably more than a little revisionist to identify Haskell monads with Category Theory monads.
So a category theory monad is a functor from some category to itself. How is IO a a functor? Which category does it operate on? What does it do to the points of that category? What does it do to the arrows?
IO is a fully paid up Monad in the categorical sense. The category is the category whose objects are types and whose arrows are functions between those types. IO is a functor. The object a maps to IO a. An arrow f::a->b maps to (>>= return . f)::IO a -> IO b and that can be used to make IO an instance of Functor. The natural transforms eta and mu are called return and join. I make no claim that beginners need to know this stuff, but it's useful to understand when you start having to compose monads and create new monads. -- Dan
I asked "How is IO a functor"? On 3 Aug 2007, at 11:50 am, Dan Piponi wrote:
IO is a fully paid up Monad in the categorical sense. The category is the category whose objects are types and whose arrows are functions between those types. IO is a functor. The object a maps to IO a. An arrow f::a->b maps to (>>= return . f)::IO a -> IO b and that can be used to make IO an instance of Functor. The natural transforms eta and mu are called return and join.
Please go over this again, but slowly this time. You have convinced me, but I'd like to understand the details a little better. I see that any type constructor TC :: * -> * is halfway to being a functor on this category of types. It acts on the objects in the obvious way, so the next step is to see about the arrows. If f :: a -> b then we want TC f :: TC a -> TC b such that TC (f . g) = TC f . TC g and TC (id::a->a) = id :: TC a -> TC a Now this is precisely the Haskell Functor class, so TC is the object part and fmap is the arrow part. You say that (>>= return . f) can be used to make [a Monad] an instance of Functor. Try it... by golly it's true. I see: fmap f = (>>= return . f). So why *aren't* Monads already set up using the type class machinery to always *be* Functors in Haskell? Isn't it bound to confuse people if monads are functors but Monads are not Functors? This is especially puzzling because Maybe, [], and IO already *are* Functors, but the way this is done makes it look accidental, not like the fundamental property of Monads it apparently is. (By the way, I note that the on-line documentation for Control.Monad glosses
= as "Sequentially composes two actions...".)
On 8/2/07, ok
I asked "How is IO a functor"?
Please go over this again, but slowly this time. Try it... by golly it's true.
I'm not fibbing. I was surprised as you when I found out about this stuff!
So why *aren't* Monads already set up using the type class machinery to always *be* Functors in Haskell? Isn't it bound to confuse people if monads are functors but Monads are not Functors?
I think it's simply an uncorrected mistake in the prelude. Also, check out Eric Kidd's "lesser known laws" here: http://www.randomhacks.net/articles/2007/03/15/data-set-monad-haskell-macros These follow from the category theory. I personally find the join/return version of the monad laws easier to think about than any other formulation. BTW Natural transformations are particularly nice in the category of types and functions. They're essentially just polymorphic functions of a certain type. But this means that they're candidates for "Theorems for Free!" http://homepages.inf.ed.ac.uk/wadler/topics/parametricity.html so they have good properties. So there's a nice little collection of small but useful theorems about >>=, return, join, fmap and so on that you can deduce from a small amount of category theory. You can deduce them all without the category theory, but I find it useful to see these things in a wider context as they no longer seem like these random identities that hold for no apparent reason. I completely agree with you that beginners don't need to know the category theory. But I highly recommend the first couple of chapters of your favourite CT textbook (up to natural transformations at least, and up to adjoints if you can stand it) to Haskellers with a mathematics background as soon as they are beyond the beginnings. It really does give a bit of insight into a few areas of Haskell. (Oh, that Eric Kidd web page will also answer your earlier question about why Data.Set isn't a Haskell Monad even though the powerset functor is a monad in the category Set.) -- Dan
My category theory is pretty weak, but I'll take a stab (others can correct me if I say something stupid): ok wrote:
It is considerably more than a little revisionist to identify Haskell monads with Category Theory monads.
Quoting the Wikipedia article on monads:
"If F and G are a pair of adjoint functors, with F left adjoint to G, then the composition G o F will be a monad. Note that therefore a monad is a functor from a category to itself; and that if F and G were actually inverses as functors the corresponding monad would be the identity functor."
So a category theory monad is a functor from some category to itself. How is IO a a functor?
It is an endofunctor in the category whose objects are Haskell types and whose arrows are Haskell functions.
Which category does it operate on? What does it do to the points of that category? What does it do to the arrows?
It maps objects (Haskell types) to boxed types (Haskell monads), i.e. sets of values of a certain type to sets of computations resulting in a value of that type. It maps arrows (Haskell functions) to Kleisli arrows, i.e. it maps the set of functions {f : a -> b} into the set of functions {f : a -> m b}.
Let's turn to the formal definition:
"If C is a category, a monad on C consists of a functor T : C → C together with two natural transformations: η : 1 → T (where 1 denotes the identity functor on C) and μ : T2 → T (where T2 is the functor T o T from C to C). These are required to fulfill [some] axioms:"
What are the natural transformations for the IO monad?
η is the unit Kleisli arrow: return :: (Monad m) => a -> m a μ : T2 → T is the join function join :: (Monad m) => m (m a) -> m a
I suppose there is a vague parallel to return and >>=, but that's about all you can claim for it.
There is more than a vague claim. From http://www.haskell.org/haskellwiki/Monads_as_containers: (>>=) :: (Monad m) => m a -> (a -> m b) -> m b xs >>= f = join (fmap f xs) join :: (Monad m) => m (m a) -> m a join xss = xss >>= id
If we are not to be revisionist, then we must admit that Haskell monads were *inspired* by category theory monads, but went through a couple of rounds of change of notation before becoming the Monad class we know and love today.
Apparently only some of use love Haskell monads! :) The notation seems like a pretty straightforward mapping to me.
What we have *was* invented for functional programming and its category theory roots are not only useless to most programmers but quite unintelligible.
I would say "applied" rather than "invented". Clearly "useless" and "unintelligible" are predicates of the programmer.
We cannot (and I do not) expect our students to *care* about monads because of their inspiration in category theory but because they WORK for a problem that had been plaguing the functional programming community for a long time.
Maybe you should raise your expectations?
This is why I say you must consider your audience.
On second thought, maybe I should have considered my audience before replying to your email. The prior probability of persuasion occurring is maybe somewhat small, but I'm a sucker for lost causes... Dan Weston
participants (4)
-
Dan Piponi -
Dan Weston -
Greg Meredith -
ok