loading...

Is bind (monadic composition) really functional?

ingun37 profile image Ingun 전인건 Updated on ・6 min read

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.

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:

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).

(a,mb)m(a,b) (a, m b) \rightarrow m(a, b)

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

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

Alt Text

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

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

Alt Text

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

Alt Text

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 f:y(x,y)f : y \rightarrow (x, y) into g:ym(x,y)g:y \rightarrow m (x, y) by simply composing return after it.

g=returnf g = \text{return} \cdot f

Alt Text

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

Alt Text

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:

bind:ma×(amb)mb \text{bind} : m a \times (a \rightarrow m b) \rightarrow m b

and can compute mbm b from the given mam a and amba \rightarrow mb . They are all familiar aren't they? If so, can we go one step further and construct a 3-way bind something like this?:

bind3:ma×(amb)×(abmc)mc \text{bind3} : m a \times (a \rightarrow m b) \times (a \rightarrow b \rightarrow mc) \rightarrow m c
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

Let's define a general morphism plant using currying.

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

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

Remeber embrace? we can turn a f:a(a,mb)f:a\rightarrow (a, mb) into g:am(a,b)g : a \rightarrow m(a, b) by composing embrace after it.

g=embracef g = \text{embrace} \cdot f

Alt Text

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

Alt Text

Uncurry the abmca \rightarrow b \rightarrow mc .

Alt Text

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 binds 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

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.

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

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

That is, in equation

ti=(a,b,c,d)iTn=1intiS0=maSn+1=bind(Sn,embraceplantuncurry(Tntn+1)) 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}) )

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

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
mama [1..]
amba \rightarrow mb \z -> [1..z]
abmca \rightarrow b \rightarrow mc \z -> .. \x -> [x..z]
abcmda \rightarrow b \rightarrow c \rightarrow md \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.

Posted on by:

ingun37 profile

Ingun 전인건

@ingun37

🇰🇷Developer/Mathematics Enthusiast

Discussion

markdown guide