How is IO a monad?

Question

I am learning the Haskell programming language. From what I am reading, Input/Ouput (IO) raises challenges for Haskell's purity, since by definition we are interacting with the outside world. From Wikipedia:

In a purely functional language, such as Haskell, functions cannot have any externally visible side effects as part of the function semantics. Although a function cannot directly cause a side effect, it can construct a value describing a desired side effect, that the caller should apply at a convenient time.

In the Haskell notation, a value of type IO a represents an action that, when performed, produces a value of type a.

Soon, I learned that IO is an example of a Haskell monad. Although we don't get a lot of explanation of what monads are. From Functors, Applicatives, And Monads In Pictures

How to learn about Monads:

1. Get a PhD in computer science.
2. Throw it away because you don’t need it for this section!

By now, I have read various definitions of - that they add context or create smaller programming languages inside a big one around a specific concept. Still trying to get a sense of what monads and how those ideas apply.

In Haskell, monad is another typeclass, with basically only one rule defining it. And IO is an instance of that.

class Monad m where    
    (>>=) :: m a -> (a -> m b) -> m b  

https://stackoverflow.com/questions/44965/what-is-a-monad

Is there something algebraic going on here? What is so algebraic about IO?

---

I apologize for being language specific. My hope is that most of this discussion applies to all functional programming languages. Any errors in my discussion represent my own limited understanding of this area.

There is another definition of monad I found in nLab that is not even specific to programming languages.

In a separate question, I would like to understand how the category theory notion of monad matches with the CS definition in the case of Haskell.

Answer 1

TLDR: Haskell types and functions form a category and from that we notice that things with >>= and return satisfy the rules for monads.

In order to consider what it means for some type to be part of a monad triplet we must first consider what a category means in the Haskell sense.

We let our category Hask be defined with objects as Haskell types and arrows to be functions. Each identity arrow is an instance of id and composition is the normal .. It's trivial to see that these satisfy the normal coherence conditions.

We can now look at endofunctors in Hask. The contain two parts, a map from types to types, and a map from functions to functions so that

• map g . map f = map (g . f)
• map id = id

Functors are therefore type constructors (which map types to types) paired with a function map which lifts arrows a -> b to arrows F a -> F b. We can also define natural transformations between them as something which "slides" a member of F a to a member of G a satisfying the normal coherence conditions

• nat . fmap f = fmap f . nat

So we can conclude that a natural transformation is something with the type

nat :: forall a. F a -> G a

Finally we take note that the identity type constructor

type Id a = a

is a functor with its map given by identity.

We're now prepared to discuss monads! A monad is a triplet of 3 things,

• A functor, F
• A natural transformation return between Id and F
• A natural transformation join between F x F and F

With the coherence conditions that join . fmap join = join . join and join . fmap return = join . return = id.

where the x means the product of two functors which is just defined by composition of type constructors.

The IO monad has a return :: a -> IO a $\equiv$ Id a -> IO a. That's our first natural transformation. Our second isn't quite as easy, but we can define join as

join :: IO (IO a) -> IO a
join = (>>= id)

We can view join as a sequencing operation. It takes all the actions stored in the structure of the outer IO and sticks them in front of all the actions in the inner IO, returning a bigger but flat IO a.

So in essence, we have this abstract notion of monads in category theory and since Haskell types can be viewed as a category, we can apply normal category theoretic notions like monads and get common patterns out of them. That's it. There's no secret category theory juice lending higher meaning to monads beyond those coherence conditions.

This is actually quite a common pattern. Whenever we view something with categories, be it logic, semantics, or type systems, we can blindly apply the last 100 years of research to our new category and discover "new" abstractions.