The Haskell Programmer's Guide to the IO Monad --- Don't Panic

The Haskell Programmer's Guide to the IO Monad - Don't Panic. Stefan Klinger.

Why do I need a monad for IO in Haskell? The standard explanation is, that the IO monad hides the non-functional IO actions ---which do have side effects--- from the functional world of Haskell. But how does this "hiding" work, apart from having IO actions disappearing beyond the borders of my knowledge?

This report scratches the surface of category theory, an abstract branch of algebra, just deep enough to find the monad structure. On the way we discuss the relations to the purely functional programming language Haskell. Finally it should become clear how the IO monad keeps Haskell pure.

It's hard for me to judge how successful this tutorial is going to be with beginners, but it seems well written.

The target audience isn't porgrammers trying to learn about monads as a programming construct, but rather programmers that want to get a taste of theory.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Ah, I'm definitely getting mileage out of this one.

But I'm confused as to what the right target audience is. It's nominally about I/O, but I'm so far just gotten to the section on natural transformations, and what I'm finding is that it's giving me the intuitions about the application of category theory that I've felt other, more rigorous presentations lack. For example:

A natural transformation is intended to transform from one structure to another, without effecting, or being influenced by, the objects in the structure.

I mean, I'm sure this is not as perfectly general as the rigorous definitions are, but I can definitely see how it applies to what I do; for example, a functional combinator I was writing recently to fold an n-ary tree structure "as if" it were a binary tree (duplicating the parent node value for each branch) is implicitly doing a natural transformation (apart from folding the binary tree, that is), and I bet that after working through the definitions there, I could sit down and prove it.

no kidding!

This's so much clearer than the other category-theory things I've been reading. I think that target audience is well stated -- "what's under the hood with all this weird stuff?" being the driving question for the audience.

Connecting Haskell practice to CT practice

I read all of this paper but very quickly/skimmingly and it doesn't seem particularly interesting. It seems to provide little intuition or motivation for monads or even why you should care about their theoretical underpinnings nor does it show how monads are used in Haskell have much to do with monads in CT. It's far from alone in the second category.

I've been wanting to write an article probably to stick on HaWiki, or maybe if I'm able for The Monad Reader, on how they do connect and about some things that are often debated over.

One of the things in the former case is in CT one of the main uses of monads is for algebras as one would come across in universal algebra. Most of the monads in Haskell are free algebras. For programming the most nature thing that corresponds to the term algebra in universal algebra is an AST. One interesting example is the Tree monad, another implementation of a non-determinism monad. In Haskell a binary tree data type looks like
data Tree a = Empty | Leaf a | Branch (Tree a) (Tree a)
consider this more computation-oriented renaming.
data NonDet a
= Fail | Value a | Amb (NonDet a) (NonDet a)
Further the implementation of the monad operations comes directly from the free monad construction. That many Haskell monads are free algebras is, in my opinion, why the MonadsAsContainers often works well; I personally find this approach misleading.

An example of the latter is the issue of monads and sequencing. Are monads "about" sequencing? If one states monads "express" sequencing meaning that they enforce it then the answer is a resounding "No!". However, they do allow you (require you rather) to express the sequencing though it may have no actual bearing on the computation. But is this directly what monads are about? First, looking from the 2-categorical perspective, the level at which monads naturally reside, monads are quite clearly the CT version of closure operators a la Category Theory as Coherently Constructive Lattice Theory. So, in its "most general" form monads can be said to be about closure. However, typically we are talking about monads in the 2-category Cat (the 2-category of (1-)categories). This adds the functor and natural transformation structure. One of the more CS intuitions about monads (in Cat from now on) is that they (particularly the Kleisli Category) are about substitution. Look at join and think expressions and substitution. Sequencing in part comes out of this due to the non-commutativity (in general) of substitutions.

(I'll probably make some edits and extensions to this later)

If you can wade through that...

... then it's no surprise that you're not impressed w/ the other paper. For at least some of us neophytes, however, the Lattice-theoretic treatment is opaque as obsidian.

That wasn't my suggestion

It was not my intent that anyone, let alone "neophytes!", should read that particular thesis (however, it is interesting if you are interested). If I ever do write that article, the only mention of the thesis would probably be in a footnote or just a reference in the bibliography, and the target audience, for that section at least, would not be "beginners".



My main complaint with this paper, especially given the degree it emphasizes the category theory, is that it is just: "we all know monads come from category theory, but let's prove it... okay, now that that's outta the way, where were we...". It, and most of the more "theoretical" introductions/tutorials/etc., are like that. They build up this foundation, then immediately ignore it. Now that you now explicitly know how the definitions mesh (pretty much trivially) what are you going to do with it? Nothing! My point is that is does not need to be this way; that there is potential benefit in understanding, manipulation, and implementation that can be derived from the category theory. It is not necessary that all of the formalism be introduced or used in such an introduction, but the resulting ideas and intuitions should be there. But if you're not going to do this, don't bother providing the formalism at all. I have no issue with "practical" introductions that essentially ignore the CT.



Finally I should note, many of the theoretical papers are not like this, and, in my opinion, if you are interested in the theory they make much better and more useful introductions or resources. E.g. Moggi's original Notions of Computation and Monads.



As an example, the monad for free algebras, and a free (finitary) algebra construction in Haskell (unfortunately untested):

data FreeMonad sig a 
  = Return a 
  | Expr (sig (FreeMonad sig a))

foldFM ret expr (Return a) = ret a
foldFM ret expr (Expr e)
  = expr (fmap (foldFM ret expr) e)

instance Functor sig => Functor (FreeMonad sig) where
    fmap f = foldFM (Return . f) Expr

instance Functor sig => Monad (FreeMonad sig) where
    return = Return
    fm >>= f = foldFM f Expr fm

-- examples

-- Maybe is
data MaybeSig x = Nothing

-- Tree (NonDet) is
data NonDetSig x = Fail | Amb x x

-- Either s is
data EitherSig s x = Error s

Already this is a simple example of what I was talking about. We have three monads completely defined with no effort. We can clearly see the relations, and there is an intuitive base for the ideas. It interesting to note that I have never seen this anywhere for Haskell despite that most of the ideas (e.g. "signatures") are used and understood in other contexts (e.g. fold algebras). Incidentally, I should point out that this isn't some deep insight, but the most obvious first thing to do.

Why walk when you can take the tube?

Why walk when you can take the tube? PDF an incomprehensible little paper that uses exactly this free monad construction.

Link doesn't work

It gives me 403 Forbidden.

Indeed, Conor's entire site

Indeed, Conor's entire site is giving a 403 now for some reason. Here's the surprisingly readable google cache HTML version of the paper. (Or just google "Why walk when you can take the tube".)

And more

Unimo has some interesting work in this line.

Also at the end of the Haskell Workshop talk, Beauty in the Beast: A Functional Semantics of the Awkward Squad, there was an excellent question and an excellent answer. Someone asked why a free term representation was being used. The answer was, since free constructions are left adjoints (a well known fact in category theory) and all left adjoints are cocontinuous (preserve colimits and thus specifically coproducts/sums, another well known fact in category theory) this implied that the coproduct of (way of combining) two free monads is just the free monad on the coproduct of term algebras, but this latter coproduct is easily directly represented in Haskell.

Monads and free algebras

Ralf Hinze, in "Deriving Backtracking Monad Transformers", uses exactly this free algebra approach when deriving exception and backtracking monads and monad transformers. His explanations and derivations are lucid, understandable and enjoyable. BTW, he credits the free algebra approach to John Hughes. Ralf Hinze also demonstrates, in the same paper, a dual, more efficient approach.

None of the examples before dealt with a state monad however. If we insist on 'bind' to be represented by a dedicated term (rather being ``distributed''), it is a bit tricky. Please see messages `Initial (term) algebra for a state monad' posted on the Haskell-Cafe in January 2005:

http://www.haskell.org/pipermail/haskell-cafe/2005-January/008241.html
http://www.haskell.org/pipermail/haskell-cafe/2005-January/008258.html
http://www.haskell.org/pipermail/haskell-cafe/2005-January/008259.html

Question

I'm a bit slow starting to read this paper, and I have a nitpick question.

In Section 3.2, the author claims that Haskell's id corresponds to (this is not clear) the identity morphisms of the objects.

However, it is stated earlier that each object (such as Int for Haskell) must have a unique identity morphism. This could be any function with the signature f :: Int -> Int, but since we picked Haskell's function composition as the category composition, it needs to be

f :: Int -> Int

f x = x

. A similar, but unique function, g, must exist as the identity morphism of the Char object, and so on.

So, I don't think Haskell's id has anything to do with the category's identity function. Actually, the presence of id itself as a morphism (since it's a unary function as well) confuses me because I don't know what (concrete) object its source is.


PS: This thread is less than a month old. Why did it disappear from the "Discussions" link?

Parametricity

However, it is stated earlier that each object (such as Int for Haskell) must have a unique identity morphism.

Note that id is parameterized over all types. The simplest way to think about this is to consider it a family of functions (morphisms) with the same name, one for each type (each object of the Haskell category).

Another way to think about it is to consider id to include an implicit functor application that maps the type of its argument to the appropriate identity morphism for that object before applying it.

id has a hidden parameter

In categorical notation, the identity morphism for an object A can be written idA. Thus, "id" can be thought of as an operation that maps an object (A) to its identity morphism (idA).

In Haskell, the full type of id is ∀a.a→a. This can be interpreted as saying that id takes two arguments, a type, a, and a value of type a. In lower-level languages like System F (used internally by GHC) and the lambda cube (used by JHC), this can be written λa:★. λx:a. x (where ★ is the kind of types). In those languages, id Int corresponds to idInt.

id

id must further have the property that for all other arrows, id . f = f and f . id = f. No other choice will accomplish this.

Neutrality

Since you brought this up, I remembered my other nitpick question.

When we choose Haskell functions as the morphisms of the set MH, is it the abstract syntax of the functions that we use as elements?

If so, then id . f and f have different abstract syntaxes for any f. So by itself, . cannot be the category composition function. Maybe something like a big-step evaluator is needed? But then, what would happen to repeat?

Semantics

The Haskell syntax is (implicitly) being interpreted via, say, a denotational semantics (big step semantics), so that A -f-> B is more like [[A]] -[[f]]-> [[B]]. So we only need id and (.) to be appropriate in the semantic domain, i.e. id and (.) are the set identity function and composition which does satisfy the laws. Incidentally, id being unique is a result not an assumption (axiom), id must be unique if it and (.) satisfy the category theory axioms. What the semantics is is irrelevant. Except, insofar as we are using Haskell syntax to specify arrows, [[id]] must interpret as id. We don't need to worry about (the categorical) (.) since it isn't an arrow.

Need help

Could someone please explain the meaning of an upside down A, a sideways E (both curvy right pointing and square left pointing), and an underlined sideways U? Is there something like

+ --> plus
- --> minus
* --> times
/ --> divided by

in other words
<symbol> --> <english>

for this stuff?

Forgive my ignorance. I went to a public school.

You could use the HTML

You could use the HTML special characters to write the notation. Here's a couple of them based on your descriptions.

∀ → For All
∃ → Exists
∈ → Element of

One missed

I think rather than element he meant:
⊆ → is a (not necessarily proper) subset of

wp math symbols

There's a pretty good collection of these on Wikipedia.

dead link -> good link

The paper no longer appears to be at the address given. I found it here.