Monad in Haskell programming vs. Monad in category theory

Question

I have a question about concept of monad used in Haskell programming and category theory in math.

Recall in Haskell a monad consists of following components:

• A type constructor that defines for each underlying type how the corresponding monad type is to be obtained. The name of this type constructor is often used synonymously with the whole monad. If $M$ is the name of the monad and $t$ is arbitrary fixed data type, then $M t$ is the corresponding monadic type

• A unit function that maps a value of the underlying type to the value of the corresponding monad type. The result is the "simplest" value in the corresponding type that can be obtained from the original value. In Haskell this function is called return. The unit function has the polymorphic type $t → M t$

• At least one further operation, which describes the combination of monadic operations.

On the other hand in category theory a monad is a triple $(T, \eta, \mu)$ of a category $C$ where

• $T: C \to C$ is a functor

• $\eta: 1_K \to T$ a natural transformation in sense of category theory

• $\mu: T^2 \to T$ a natural transformation

and these objects should satisfy following diagrams: https://en.wikipedia.org/wiki/Monad_(category_theory)

Question: How are these monads from Haskell and abstract category theory related? Does the monad structure in Haskell have natural "monad structure" in sense of category theory, ie we can canonically associate to $M$ a canonical triple as described above?

Answer 1

A monad in Haskell is intended to be a monad on the category of types, when the category theory is done internally to the type theory. The capabilities of Haskell and similar languages are somewhat limited, so there are a lot of basic constructions in category theory that cannot be done, but there are plenty of structures that can be encoded reasonably.

• M :: * → * is the object mapping of the functor, which you have instead named $T$ later.
• The arrow mapping part of the functor is given by fmap
• $η$ is the unit function, which Haskell calls return (or pure, which is a little more general)
• $μ$ is given by join.

The requirements expected of Monad instances are equivalent to the ones to be a monad in category theory.

Essentially, this is not much different than speaking specifically about monads on the category $\mathsf{Set}$, aside from the earlier mention of Haskell/etc. missing some constructions that set theory has (there are things that act enough like (co)products, but not like pullbacks/pushouts). You could do a lot only thinking about monads on $\mathsf{Set}$, because many structures in abstract/universal algebra give rise to one, and are presentable that way.

One might quibble that types in various programming languages do not technically form a category with good properties/structure, but you could instead imagine that you are using them as a means to talk about something better behaved, like System $F_ω$, and it wouldn't really change the answer in an interesting way.

• leftaroundabout: BTW, the notation * → * means simply Type → Type (which is actually the preferred way to write it in modern Haskell, because * can also be an infix operator).
• user267839: sorry for probably foolish question, but what do you precisely mean by "system" $F_{\omega}$? What kind of system?
• Isaac van Bakel: @katalaveino System $F_\omega$ is a formal type system for the lambda calculus. System F and its extensions have an intimate history with Haskell and other strongly-typed functional languages.
• Mario Carneiro: "One might quibble that types in various programming languages do not technically form a category with good properties/structure" Obligatory link: Hask is not a category