I’ve been programming Haskell for several years now, and I have not yet partaken in the rite of passage: writing a monad tutorial. Well, finally I can come of age, for I am giving a monads tutorial talk to the CU ACM group next Thursday.

I’m thinking of starting with the IO monad, since that was the motivation for adding monads to Haskell in the first place. It also gives people something concrete to think about before I segue into more abstract monads. But I don’t want to use GHC’s IO monad as an example:

newtype IO a = IO (RealWorld -> (a, RealWorld))

Because it’s too “low-level”. I barely want to talk about laziness, so a construction which is just there to force evaluation order seems kind of hacky. If you don’t think of it as a construction to force evaluation order, then it is too abstract: what do you mean a function which takes the whole world as an argument? Also, it uses a function as its primary data structure, and the talk will be given to people who are still a little uncomfortable with first-class functions (it will have to introduce them at some point though, but I want to ease into it).

My current plan is to eventually get to the GADT form:

data IO a where PutChar :: Char -> IO () GetChar :: IO Char Bind :: IO a -> (a -> IO b) -> IO b Return :: a -> IO a

And then focus on Bind and Return as a segue into the idea of a monad. But yes, you heard me right, to explain an advanced feature, I’m going to use an *even more* advanced feature! That’s only because I find GADTs very intuitive; in fact, when I was first learning Haskell on the Pugs project, seeing a GADT helped me to understand normal ADTs.

But of course I must ground this GADT. Bind is a weird-looking function, how the hell did I come up with that? I want to arrive at it by necessity, so I’m going to start with a simpler ADT form. I’ll introduce purely-functional IO as a data structure, initially looking like this:

data IOTree = PutChar Char | IOTree `Then` IOTree | NoOp

And then realize that we have no way to do input. At this point I expected to have to switch to the polymorphic variant to handle input, but then this hit me:

data IOTree = PutChar Char | IOTree `Then` IOTree | NoOp| GetChar (Char -> IOTree)

To my surprise, with this I was capable of writing all the IO functions that I could using the polymorphic variant, but with some slightly strange-looking type signatures.

getLine :: (String -> IOTree) -> IOTree getLine f = getLine' id where getLine' s = GetChar $ \ch -> case ch of '\n' -> f (s "") _ -> getLine' (s . (ch :))

And then I saw it. That type signature looks awfully familar. If I replace the types with variables it’s completely obvious: `(a -> r) -> r`. I’m working *explicitly* in the continuation monad. Sure enough, I can build a monad out of IOTree.

newtype IO a = IO { runIO :: (a -> IOTree) -> IOTree } instance Monad IO where return x = IO ($ x) IO m >>= f = IO $ \c -> m (\a -> runIO (f a) c)

That’s a unique presentation of the IO monad that I’ve never seen before. It feels “smooth”, there are no huge leaps anywhere except for where the hell we came up with the idea of a monad. But that reason is enough for me not to want to use it. Another reason against it is that the implementation of `>>=` was not at all obvious to *me* (it took some typechecker runs), so how are FP noobs going to understand it?

So I’m still not sure how I’m going to motivate the polymorphic form. Probably something like introducing the idea of IO “holding” a value, and then we need a variable for the type of value it holds. That would also allow me to introduce Functors, which I want to do as a “monad indicator”; i.e. functors are pretty easy to intuitively spot, and there’s a decent chance that if you have a functor, you have a monad.

Stepping away from pedagogy for a moment, I find it very interesting what continuation passing style did to this example. It seems that CPS is a nice way to build up data structures “procedurally” without hand-crafting a different monad for each one. For instance, Writer can be naturally specified as:

type Writer w a = Cont w a tell :: (Monoid w) => w -> Writer w () tell w = Cont $ \c -> w `mappend` c ()

Anyway, I’d love to hear any advice anyone has about presenting the IO monad, or monads in general. The focus is not so much “so you’re trying to learn Haskell but are perpexed by monads, here’s how to understand them”, but more “you’ve barely heard of Haskell, here’s why monads are awesome”. I plan to talk about IO, List, Suspend^{[1]}, and close with STM (where Haskell rocks everyone else’s world).

^{[1]}The Suspend monad is what Fregl‘s Event monad is built on. It’s a type of coroutine which only consumes values:

data Suspend v a = Return a | Suspend (v -> Suspend v a)

You might be interested in some of the content of this paper, which, among other things, explains two contenders for the IO system early in Haskell’s development: continuations and streams. The former, of course, you’ve come upon yourself, but they’re both inter-expressible (and are both monads, of course).

It also happens that there is a sufficiently powerful monad into which all other monads can be embedded (I believe it was Andrzej Filinski who showed this). The necessary components are continuations and mutable reference cells (or, delimited continuations on their own, I think); given those, you can get the behavior of any other monad (although, IO may be something of an exception, as it’s all about primitive runtime system hooks). Filinksi actually uses this fact in a technique he calls monadic reflection, which allows more convenient use of monads in, say, Standard ML. It allows one to do some reasoning about the effects used in code with monads, but by encoding them in the implicit state/continuation monad that all underlies all SML, one can still write code in direct style, which is rather more convenient than lots of binds and lambda expressions.

I think Representing Monads is the briefer of his two papers I’ve seen on the topic.

Well, historically bind was discovered when Kleisli went looking for an initial object in the category of adjunctions giving rise to a given monad, so it’s not intuitively obvious that one *should* be able to produce bind entirely naturally. Join is IMHO much more natural, and I find it makes much more sense to define bind in terms of join.

[Of course, bind and join are both "natural" in the technical sense, ie they're both natural transformations - and moreover bind is determined by a universal property. But you know what I mean...]

pozorvlak: The bind form is the “obvious” way to do it from the POV of structural proof theory. All strong monads are versions of the lax modality, and bind is the elimination form for it. (Ordinary monads give rise to possibility, and an ordinary comonads give rise to necessity operators.) So I have exactly the opposite intuition about whether bind or join is more “natural”!

What do you think of Brent Yorgey’s monad presentation? He provided background to the monad issue by first highlighting the meaning and consequences of purity. At least a couple of slides were devoted to referential transparency although I didn’t catch him name it as such. On the other hand if your audience is already familiar with such issues, your monadically meatier approach is worth savoring. Since you’re among the rare few with more than a passing acquaintance with comonads, how about mentioning as an oh-and-by-the-way continuations are also comonadic? Get them to invite you again for another talk. Is there a way to record the talk(s) and upload them on video google?

nemo: I liked Brent’s presentation for its practical aspect. It has encouraged me to at least mention XMonad and QuickCheck in my presentation. As far as the presentation of monads in particular, I’m not so keen. When I was first learning Haskell, I remember the “argument” that the IO monad (and thus to my little mind, monads in general) served to separate pure code from impure code. My reaction was “so what?”. “So Haskell’s cool, but it’s not cool enough to do

realthings, so we introduce IO as a hack”. Similar statements propagate among the uninformed about Haskell every now and then.But that is not how I think of monads

at allanymore, not even IO. IO pervades Fregl, my FRP implementation, but it is hidden underneath a stronger abstraction. Instead, monads are an abstraction of imperative control. They capture the notion of “after”, for a suitable definition of time. The IO monad, for example, is an abstraction layer that lets you write effectful code without worrying about how it’s implemented. And STM is an abstraction that lets you write effectful code which is guaranteed to be “well-behaved”. Monads are aboutrevokingprivileges, not granting them (thus allowing you to interpret the new underprivileged code in new ways). That’s how I think about it anyway.And yes, I’ll probably mention comonads, as a hat-tip to a local professor (Dr. Alexander Repenning) whose research is “antiobjects”, which are kind of a pedagogical version of comonads.

On the subject of comonads, can anyone perhaps recommend a paper that does a good job explaining how comonads and continuations are related? I’ve heard it mentioned, but I’ve never found anything that’s really driven the idea home for me.

For one, the comonad related to the CPS monad appears to be, in fact, the CPS monad itself. That is, it’s a comonad in the opposite category that, when translated back into the base category is the same as the monad there.

I also have a paper that argues that modal necessity, which is comonadic, is a better basis for typing delimited continuations (among other things) than monads. However, they go on to define several individual languages whose type systems directly incorporate the modal operator, and it wasn’t particularly obvious to me how (or even if) one could use that information to define the sort of (co)monadic combinator library that would be useful in Haskell, which doesn’t have such an extended type system.

Anyhow, perhaps I’m expecting more out of these things than there actually is, but I’d appreciate any tips people have.

dan:

type Contn a = forall r. (a->r)->r

Coreturn/counit/extract (w :: Contn a) = w id

Cobind is similarly straightforward. That (Contn a) is both (Monad a) and (Comonad a) is folk knowledge and may be gleaned from trawling through haskell-cafe archives. Perhaps what the community needs is really a Continuation Tutorial illustrating both monadic and comonadic usages.

Ah! Now that you mention it, I’ve tried that before, and had even written comonad instance for it. However, I later discarded it, because I couldn’t get callCC to type (as the r from the discarded continuation won’t unify with the one from the duplicated continuation).

At first, this setup seems related to delimited continuations, as one can get reset from either ‘return . coreturn’ or ‘coextend coreturn’, I believe. However, shift runs into typing problems.

`'shift :: ((a -> Contn r) -> Contn r) -> Contn a'`

generates type errors, and though one can instead use:

`shift :: (forall s. (a -> Contn s) -> Contn s) -> Contn a`

this type signature ensures that, 1) the subcontinuation is always called at least once, because the only way to get an appropriate ‘s’ is to invoke it (so abort a = shift (\_ -> return a) is out), and 2) nothing interesting can be done with the result type ‘s’ of the subcontinuation, so for instance, turning a (monadic) fold into a cursor is also out. About the only thing I can think of off hand that this shift would be useful for is invoking the subcontinuation multiple times for its side effects (in conjunction with other monad transformers), but I can’t say I’ve even tried that.

So, while this CPS type is both a monad and comonad, it doesn’t seem to be useful for introducing the kinds of control effects one typically associates with continuations (unless I’m missing something major, which is quite possible). I’ve toyed briefly with typing some control operators differently (for instance, the type of reset = counit seems to make some sense), but didn’t really get anywhere with that.

Am I way off base, here? Apologies for the long comment.

luke:

Staring at Suspend longer finally yielded (or should I say Return’ed) “Aha! So it’s actually the free monad over exponentiation.” Are your Suspend trees well-founded?

I also find GADTs very intuitive; I think it’s a great way to go about this.

Your formulation of IO as a GADT is very similar to Unimo/Prompt; I think you will find it more intuitive if you split out “bind” and “return” and treat IO as just the operations; for example, in Prompt (see my URL):

`data IOAction a where`

PutChar :: Char -> IOAction ()

GetChar :: IOAction Char

Then you can talk about sequencing and such as a separate thing; for Prompt you can start with a datastructure that looks like this (which is pretty easy to make into a monad):

`data Prompt p a where`

Pure :: a -> Prompt p a

Effect :: p x -> (x -> Prompt p a) -> Prompt p a

-- existentially quantified on x.

`type IO a = Prompt IOAction a`

Another minor comment; Prompt is just a more general form of Suspend which can also output values during the computation:

`data Only v a where Only :: Only v v`

type Suspend v a = Prompt (Only v) a

`suspend :: (v -> Suspend v a) -> Suspend v a`

suspend k = Effect Only k

I thought a monad was a “uni-ball” style gonad. You know, a kind of mono-ball testes. Probably not, eh? ah well, couldn’t help myself.

nemo: I don’t think Contn is actually a continuation monad, because the type forall r. (a -> r) -> r is isomorphic to a, And the implementation of the monad and comonad operations are essentially just those for identity after employing the isomorphism. That explains why it is not possible to write callCC for Contn. It is the universal quantifier which causes this, and it doesn’t arise for a fixed r in Cont r a.

Dan: You are talking way over my head. I wish I could contribute to that discussion, but alas…

Ryan: I don’t think I’ll present it that way, because Prompt essentially represents factoring the monadiness out of a data structure, but that’s precisely what I want to do in the first place by introducing monads, so there’s no need to do it twice. Thanks for pointing that out though; I don’t have much experience with prompt and I’d like to understand it better. The Suspend thing will give me something to study.

evan: Heheh, thanks for pulling this disgusting conversation out of the gutter and bringing it back to more civilized matters. You were always good at that. :-)

luke, dan:

You’re both correct. Contn is not a continuation monad, i.e. cannot be made an instance of MonadCont. What I said about continuations earlier, I really should have called “CPS.” My bad for confusing the two.

luke, dan, nemo: True, Contn is not a continuation monad, but it *is* an attenuation comonad. Fascinating stuff…