Is bind (monadic composition) really functional?
Ingun 전인건
Posted on May 1, 2020
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
andreturn
- 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).
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
into
by simply composing return
after it.
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:
and can compute from the given and . They are all familiar aren't they? If so, can we go one step further and construct a 3-way bind something like this?:
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.
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
into
by composing embrace
after it.
Now we can bind it with the m a
and get m(a, b)
.
Uncurry the .
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
.
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.
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
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 |
---|---|
[1..] |
|
\z -> [1..z] |
|
\z -> .. \x -> [x..z] |
|
\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 May 1, 2020
Join Our Newsletter. No Spam, Only the good stuff.
Sign up to receive the latest update from our blog.