Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Haskell do notation

Nathaniel Virgo (Jul 03 2020 at 06:21):

This is a spin off from the Markov categories and enrichment thread. In that thread, Jules used Haskell do notation to give some intuition for a commutative monad:
Jules Hedges said:

Commutativity is equivalent to the fact that the Haskell programs $(a, b) \mapsto \text{do} \{ x \leftarrow a; y \leftarrow b; \text{return} (x, y) \}$ and $(a, b) \mapsto \text{do} \{ y \leftarrow b; x \leftarrow a; \text{return} (x, y) \}$ are equal

So it says that there is no "side channel information flow" beyond what is made explicit in the types

So an example of a noncommutative monad is state, since there is implicit information flow through the state variable

I used to code in Haskell sometimes, years ago, but I didn't know any category theory at the time and have since forgotten most of my Haskell knowledge. But I'm curious about how the do notation relates to monads as I now understand them. Can anyone give a quick explanation of how the do notation in Haskell relates to monads in the category theory sense?

I don't need to know how to use monads in Haskell, necessarily - I'm just interested in the idea of using this notation to reason about category-theoretic monads.

Exequiel Rivas (Jul 03 2020 at 08:14):

Perhalps this helps on how the do notation in Haskell relates to monads in the category theory sense:

A monad in Haskell is usually represented as a type constructor m :: * -> * together with functions:

• return :: forall a . a -> m a,
• bind :: forall a b . m a -> (a -> m b) -> m b (usually written in infix form as >>=).

This data is packed using a type-class called Monad, and it represents the notion of Kleisli triple, which is a categorical notion that's equivalent to monads. Following Wikipedia article, m is $T$, return is $\eta$, >>= is a flipped version of $-^*$.

There's a number of rules that "desugar" from do-notation to these functions. For example, do { y <- b; return y } would desugar into b >>= \y -> return y.

The programs that Jules wrote are: \(a, b) -> do { x <- a; y <- b; return (x, y)} and \(a, b) -> do { y <- b; x <- a; return (x, y) }. These desugar into \(a, b) -> a >>= \x -> b >>= \y -> return (x, y) and \(a, b) -> b >>= \y -> a >>= \x -> return (x, y). These two programs are functions of type (m c, m d) -> m (c, d), and they are the kind of arrows that you need to be equal in order to call a monad commutative: $T c \otimes T d \to T (c \otimes d)$ (here $\otimes$ is product, denoted by tuples (c,d) in Haskell).

Exequiel Rivas (Jul 03 2020 at 08:31):

What's not explicit here is the strength thing. The thing is that we're mixing the exponential object $\left[ A, B \right]$ (i.e. the one that comes from the right adjoint to $A \times -$) with the hom-set $\mathcal{C}(A, B)$. We do this because both the exponential and the hom-set get kind of represented by the same function type a -> b under this view.

Any monad m in Haskell gets strengths "automatically". For example, st :: (a, m b) -> m (a, b): st (a, v) = v >>= \b -> return (a, b).