principleModerate
Monad in Haskell programming vs. Monad in category theory
Viewed 0 times
theoryprogramminghaskellcategorymonad
Problem
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?
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?
Solution
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.
The requirements expected of
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.
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(orpure, 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.
Context
StackExchange Computer Science Q#131829, answer score: 15
Revisions (0)
No revisions yet.