## DEV Community is a community of 715,952 amazing developers

We're a place where coders share, stay up-to-date and grow their careers.

Ingun 전인건

Posted on • Updated on

# 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

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

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

$(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). Every type of Pair entails two trivial morphisms, first and second, which selects the first and second element respectively. 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. Bear with me. Compose Currying and make it into a single-parameter function. We've got a x from the first. Compose them. 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 \rightarrow (x, y)$ into $g:y \rightarrow m (x, y)$ by simply composing return after it.

$g = \text{return} \cdot f$ We can finally compose the m y to it monadically using bind. 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:

$\text{bind} : m a \times (a \rightarrow m b) \rightarrow m b$

and can compute $m b$ from the given $m a$ and $a \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?:

$\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. Let's define a general morphism plant using currying.

\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. Remeber embrace? we can turn a $f:a\rightarrow (a, mb)$ into $g : a \rightarrow m(a, b)$ by composing embrace after it.

$g = \text{embrace} \cdot f$ Now we can bind it with the m a and get m(a, b). Uncurry the $a \rightarrow b \rightarrow mc$ . 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. 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.

\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. That is, in equation

$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
$ma$ [1..]
$a \rightarrow mb$ \z -> [1..z]
$a \rightarrow b \rightarrow mc$ \z -> .. \x -> [x..z]
$a \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.