Is bind (monadic composition) really functional?
Tags: functional, monad, haskell, math
Published: 2020-05-01 17:07:03

---
title: Is bind (monadic composition) really functional?
published: true
description: 
tags: functional, monad, haskell, math
---

# Motivation

Have you ever suspected that monadic compositions are really functional? For example, lets say we are generating right integer triangles(triangles all of whose sides have lengths of integer and an angle of 90-degree). We can do it elegantly using List Monad in any functional language, but for now, Haskell.

```haskell
naturalTriangles :: [(Int, Int, Int)]
naturalTriangles = do
    z <- [1..]
    x <- [1..z]
    y <- [x..z]
    if x^2 + y^2 == z^2 then return (x, y, z)
                        else []

-- (3,4,5),(6,8,10),(5,12,13),(9,12,15),(8,15,17) ...
```

The code calls `bind`, a monadic composition, recursively. We can remove the syntactic sugars and demonstrate the recursive bindings better:

```haskell
naturalTriangles2 :: [(Int, Int, Int)]
naturalTriangles2 =
    [1..] >>= \z ->
        [1..z] >>= \x ->
            [x..z] >>= \y ->
                if x^2 + y^2 == z^2 then [(x, y, z)]
                                    else []
```

Well, it's ubiquitous, clean, short and simple. There seems to be absolutely no problem. But can I say it's functional with confidence? The inner functions seem to have context because they are dependent to the other variables that are defined outside. In other words, changes in `z` affect `x` and `y`. That's not very functional.

Why do functional programming languages tolerate such codes? Is it some kind of compromise on semantics in exchange for a little convenience?

No it's not. In fact, recursive bind works little complicated under the hood but is indeed a 100% functional model. Let me explain.

# Prerequisite

* Basic knowledge about Monad, especially `bind` and `return`
* Currying and Uncurrying
* Basic knowledge about Functor

# embrace : (a, m b) -> m(a, b)

First of all, we need to understand the following general morphism(transformation).

{% katex %}
(a, m b) \rightarrow m(a, b)
{% endkatex %}

where `m b` is a type `b` lifted by a monad `m`, and `(x, y)` is a Pair (or 2-tuple) of type `x` and `y`. This morphism takes a Pair of types, one of which is a monad `m`, and somehow takes off the monad from the type and put it back onto the entire Pair. For example, `(String, [Int])` would be transformed into `[(String, Int)]` by this morphism. Let me explain how to construct one. Let's start from the `(x, m y)`.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/ai4e4zxs6bxpy6c35x15.jpeg)

Every type of Pair entails two trivial morphisms, `first` and `second`, which selects the first and second element respectively.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/u3kuidkc738tke7vt1td.jpeg)

There's another entailing trivial morphism, the construction function, which construct a Pair with given two types. In mathematics, we denote the domain of a function that accepts 2 parameters as a cartesian products of the parameter types.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/bhahqf1qwl9tz7gil7fx.jpeg)

Bear with me. Compose Currying and make it into a single-parameter function.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/fa3znglhw17kdijdmx85.jpeg)

We've got a `x` from the `first`. Compose them.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/3kk8mtp2qq89p9ukxxv8.jpeg)

We now have a function that accepts `y`. But we've only got `m y` from the `second`. No problem. `m` is a monad therefore the `return : a -> m a` function must exist. We can turn a {% katex inline %} f : y \rightarrow (x, y){% endkatex%} into {% katex inline %}g:y \rightarrow m (x, y){% endkatex %} by simply composing `return` after it.

{% katex %}
g = \text{return} \cdot f
{% endkatex %}

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/otxut39s5g1lop0chdk0.jpeg)

We can finally compose the `m y` to it monadically using `bind`.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/12zrv64qnvc1ecpwpu8u.jpeg)

We now have constructed a general transformation from `(x, m y)` to `m(x, y)`. We will call it `embrace` from now on because the monad container now "embraces" not only `y` but `x` as well.

# General Functional Model

We are now ready to present the recursive `bind` scheme in a functional model.

We all know `bind` of a monad `m` has a signature like this:

{% katex %}
\text{bind} : m a \times (a \rightarrow m b) \rightarrow m b
{% endkatex %}

and can compute {% katex inline %}m b{% endkatex %} from the given {% katex inline %}m a{% endkatex %} and {% katex inline %}a \rightarrow mb{% endkatex %}. They are all familiar aren't they? If so, can we go one step further and construct a 3-way bind something like this?:

{% katex %}
\text{bind3} : m a \times (a \rightarrow m b) \times (a \rightarrow b \rightarrow mc) \rightarrow m c
{% endkatex %}

> ###### You can stop reading and try it yourself using pen and paper, drawing dots and arrows. It's quite fun!

Let's start from these three types.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/xjh0mv35krrmp49g8jhx.jpeg)

Let's define a general morphism `plant` using currying.

{% katex %}
\begin{aligned}
&\text{plant} : (a \rightarrow mb) \rightarrow (a \rightarrow (a, mb)) \\\\
&\text{plant}(f)(a) = (a, f(a))
\end{aligned}
{% endkatex %}

This is a trivial transformation. It takes `f : a -> m b` and changes a little so it now returns not only `m b` but the parameter `a` as well via Pair `(a, m b)`. The name is because this new `f'` "plants" 'a' along with `mb`.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/5dj4g5ooa2cysjlfvb0o.jpeg)

Remeber `embrace`? we can turn a {% katex inline %}f:a\rightarrow (a, mb){% endkatex %} into {% katex inline %}g : a \rightarrow m(a, b){% endkatex %} by composing `embrace` after it.

{% katex %}
g = \text{embrace} \cdot f
{% endkatex %}

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/r97auwg2bf3mcz7lmcy9.jpeg)

Now we can bind it with the `m a` and get `m(a, b)`.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/c9fbx265dpjzm86dgnxj.jpeg)

Uncurry the {% katex inline %}a \rightarrow b \rightarrow mc {% endkatex %}.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/jvqdye406x2hmrizv4zx.jpeg)

If you are thinking by now that we are almost done because we can just `bind` and get the `m c` right away, then you are wrong. If we just end it right here then it can only become a 3-way model. What we need is a general model that can be applied to not only a 3-way but a 4-way, 5-way, 6, 7.. etc. because monadic `bind`s can recurse all day. So we are not binding yet. We are composing `plant` and `embrace` first, and then we will finally `bind`.

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/8hq3pxwqnhm5dg1883di.jpeg)

What we've got is `m(a, b, c)` instead of `m c`, but it's alright because all the information we need, which is `m c`, is embedded in the `m(a, b, c)`. All we need is a transformation that picks the last one from a tuple.

{%katex%}
\begin{aligned}
&\text{last}: (a,b, \cdots z) \rightarrow z \\\\
&\text{last}(a,b, \cdots z) = z
\end{aligned}
{%endkatex%}

We can extend it all the way to 4-way, 5-way, 6, 7.. in the exact same way. But let's extend it to only 4-way since that's the model for the integer triangles generator. 

![Alt Text](https://dev-to-uploads.s3.amazonaws.com/i/3mvul632v8ry83rptnhm.jpeg)

That is, in equation

{% katex %}
t_i = (a,b,c,d \dots)_i \newline

T_n = \prod_{\mathclap{1\le i\le n}} t_i \newline

S_0 = m a \newline

S_{n+1} = \text{bind}(S_n, \text{embrace} \circ \text{plant} \circ \text{uncurry} (T_n \rightarrow t_{n+1}) )
{% endkatex %}

Let's fit the problem into this functional model. If we revise the code

```haskell
naturalTriangles2 :: [(Int, Int, Int)]
naturalTriangles2 =
    [1..] >>= \z ->
        [1..z] >>= \x ->
            [x..z] >>= \y ->
                if x^2 + y^2 == z^2 then [(x, y, z)]
                                    else []
```

we can see the corresponding components:

| Model | code |
| --- | --- |
| {%katex inline%} ma {%endkatex%} | `[1..]` |
| {%katex inline%} a \rightarrow mb {%endkatex%} | `\z -> [1..z]` |
| {%katex inline%} a \rightarrow b \rightarrow mc {%endkatex%} | `\z -> .. \x -> [x..z]` |
| {%katex inline%} a \rightarrow b \rightarrow c \rightarrow md {%endkatex%} | `\z -> .. \x -> .. \y -> ... [(x, y, z)]` |

The variables we thought was a context was in fact not a context but a parameters given to the same function!

Now we can say they are functional with confidence.