Maybe in λ-calculus

I'm currently taking a class on Models of Computation. If you're studying at the University of Zurich or ETHZ I highly recommend that you take this class :) You'll get to solve really cool puzzles each week as part of the class.

My favourite model of computation so far is lambda calculus. As a functional programming enthusiast, I may be a bit biased though…

Going forward, I will assume that you have some basic knowledge of lambda calculus.

What is a Maybe?

A Maybe value represents an optional value. It can either be present (which we will call Just) or absent (which we will call Nothing).

Maybe goes by many different names depending on the programming language: Rust calls it Option, Java Optional and Haskell calls it Maybe.

If you're interested in learning more about Maybe then there's an excellent introduction by Mark Seemann targeted at C# developers.

Intuition

The tricky thing with each model of computation is to build up an intuition of how to solve certain problems in the given model.

Let's look at some other data structures first—to build up this intuition. Don't worry, I will not be spoiling any of the exercises from the Models of Computation class ;)

Church Numerals

Church Numerals encode a given natural number n, by applying a function n times.

The first function application needs some starting value (or seed), so each number is a function that takes two arguments:

λf.λx.EXPR

Here are the first four numbers:

λf.λx.x

λf.λx.f x

λf.λx.f (f x)

λf.λx.f (f (f x))

Tuples

Tuples are similar to Church Numerals in that tuple values accept some function that they then apply. In the case of tuples, the function is applied with two arguments: one for the first value of the tuple and one for the second value of the tuple.

So the tuple (X, Y) would correspond with the following λ expression:

λs.s X Y

We can then generalize this to an expression that creates a tuple:

λa b.λs.s a b
# Note that this is equivalent to a function with three arguments:
λa b s.s a b
# ... or three functions with one argument each:
λa.λb.λs.s a b

Picking out the first or second value is easy: We call our tuple value with a function that picks one of its two arguments.

So picking the first value out of a tuple would look something like this:

#              ╭─ This is the «constructor» from above
#       ───────┴──────
     ((λa.λb.λs.s a b) X Y) (λa.λb.a)
#                            ───┬───
#                               ╰─  This function  picks out
#                                   the first of two arguments
->>β (λs.s X Y) (λa.λb.a)
->>β (λa.λb.a) X Y
->>β X

Picking out the second value works analogously.

ℹ️ And now for a word from our sponsor about syntax: I'm using ->>β to indicate β-reduction and ->>δ to indicate δ-reduction (replacing definitions).

Booleans

Booleans can be encoded as expressions that take two arguments: One that is called when the boolean is true and one that is called when the boolean is false:

λt f.t

λt f.f

Let's experiment a bit:

#        ╭─ an expression that accepts a boolean
#        │         ╭─ True
#     ───┴────   ──┴───
     (λb.b X Y) (λt f.t)
#          ┬ ┬
#          │ ╰─ If True, return Y
#          ╰─ If False, return X
->>β (λt f.t) X Y
->>β X

# As you can see, we get X, because the boolean was True.
# Similarly, if we call our expression with False, we will get Y:
     (λb.b X Y)(λt f.f)
->>β (λt f.f) X Y
->>β Y

This looks very promising! Like booleans, Maybe values also have two possible states. Unlike booleans however, one of the states—Just—carries a value.

Implementation

Let's apply our newly gained knowledge to Maybe. Like booleans, our Maybe values are expressions of the form:

λj n.EXPR

The first argument j will be called when the Maybe value is Just
the second argument n will be called when the Maybe value is Nothing.

The Nothing value is very straightforward. It's the same as False:

λj n.n

Just takes an additional first parameter as it has to store a value.

λa.λj n.j a

You can see that Just values call j with the stored value. An instance Just X value would look like this:

λj n.j X

Just like with booleans we can decide what to do based on the state of a Maybe value:

#          ╭─ an expression that accepts a Maybe
#          │                ╭─ Just X
#     ─────┴──────   ───────┴───────
     (λm. m incr 0) ((λa.λj n.j a) X)
#           ─┬── ┬
#            │   ╰─ If Nothing, return 0
#            ╰─ If Just, increment the value
->>β (λm. m incr 0)(λj n.j X)
->>β (λj n.j X) incr 0
->>β incr X

# Similarly, if we pass in a Nothing value, we get 0:
     (λm. m incr 0)(λj n. n)
->>β (λj n. n) incr 0
->>β 0

💭 With a bit of imagination, you could see our Maybe value as an implementation of the Visitor pattern modulo the separate Visitor type.

Writing out these match expressions gets tedious quickly and is not very expressive. To improve on this, we'll implement some useful functions for working with Maybe values.

bind

bind takes a Maybe and function that operates on the value of the Maybe. The function itself return a Maybe. The function is only applied if the Maybe is Just. Otherwise Nothing is returned. You can think of this as a «apply some operation on the value and flatten the nested Maybes».

#   ╭─ a Maybe value
#   │ ╭─ a function that accepts a value and returns a Maybe value
#   ┴ ┴
   λm f.m f Nothing
#         ┬ ───┬───
#         │    ╰─ If Nothing, return Nothing
#         ╰─ If Just, apply the given function

Perhaps the simplest example is to use bind with the Just function¹. We should get out the same Maybe value:

     bind (Just X) Just
#    ─┬──
#     ╰───────╮
#     ────────┴───────
->>δ (λm f.m f Nothing) (Just X) Just
->>β (Just X) Just Nothing
#     ──┬───  ─┬── ───┬───
#       ╰───╮  │      ╰─────────────────╮
#           │  ╰─────────────╮          │
#      ─────┴─────      ─────┴─────   ──┴───
->>δ ((λa.λj n.j a) X) (λa.λj n.j a) (λj n.n)
->>β (λj n.j X) (λa.λj n.j a) (λj n.n)
->>β (λa.λj n.j a) X
->>β (λj n.j X)

As expected, this evaluates to Just X.

While this example may not be that interesting, bind is very useful as a tool for implementing more functions.

map

An operation perhaps more commonly used than bind is map: It applies a function to the value inside the Maybe only if it's present and returns a Maybe containing the new value².

We'll use bind to define map. Remember: bind expects our function to return a Maybe. This is easily satisfied by wrapping the given function in a new function that calls Just with the result:

#   ╭─ a Maybe value
#   │ ╭─ a function that accepts a regular value
#   ┴ ┴
   λm f.bind m (λx. Just (f x))

For example, you have a Maybe containing some number that you want to multiply by two:

     map (Just X) double
#    ─┬─
#     ╰────────────╮
#     ─────────────┴──────────────
->>δ (λm f.bind m (λx. Just (f x))) (Just X) double
#          ─┬──
#           │
#           ╰──────╮
#           ───────┴────────
->>δ (λm f.(λm f.m f Nothing) m (λx. Just (f x))) (Just X) double
#      ┬ ┬                                        ───┬───  ──┬───
#      │ ╰───────────────────────────────────────────┼───────╯
#      ╰─────────────────────────────────────────────╯
->>β (λm f.m f Nothing) (Just X) (λx. Just (double x))
->>β (Just X) (λx. Just (double x)) Nothing
#     ─┬──         ─┬──             ───┬───
#      │            ╰─────────────╮    ╰──────────────────╮
#      ╰───╮                      │                       │
#     ─────┴──────           ─────┴─────               ───┴──
->>δ ((λa.λj n.j a) X) (λx. (λa.λj n.j a) (double x)) (λj n.n)
#       ┬           ┬        ┬             ───┬────
#       ╰───────────╯        ╰────────────────╯
->>β (λj n.j X) (λx. (λj n.j (double x))) (λj n.n)
->>β (λx. (λj n.j (double x))) X
->>β (λj n.j (double X))

This is the same as Just (double X). Hurray it worked ✨
We could do a similar demonstration for Nothing, but I leave that as an exercise to, my dear reader ;)

filter

Another useful operation on Maybe values is filter: It takes a Maybe value and a predicate. If the value inside the Maybe fulfils the predicate then the Maybe value is left unchanged. Otherwise Nothing is returned.

Just like with map, we can use bind as a building block to implement our new function:

#   ╭─ a Maybe value
#   │ ╭─ a predicate (i.e. a function that takes a value
#   │ │                    and returns a boolean)
#   ┴ ┴ 
   λm p.bind m (λx.p x (Just x) Nothing)
#                       ──┬───  ───┬───
#                         │        ╰─ If the predicate does not match,
#                         │           return Nothing
#                         │
#                         ╰─ If the predicate matches,
#                            return Just x

We'll define an isEven predicate for the purpose of testing our filter function:

λn.n not True

And here's the definition of not:

λb.b False True

Let's test:

     filter (Just 3) isEven
#    ──┬───
#      │
#      ╰────────────────╮
#                       │
#     ──────────────────┴──────────────────
->>δ (λm p.bind m (λx.p x (Just x) Nothing)) (Just 3) isEven
->>β bind (Just 3) (λx.isEven x (Just x) Nothing)
#    ─┬──
#     │
#     ╰──────╮
#            │
#     ───────┴────────
->>δ (λm f.m f Nothing) (Just 3) (λx.isEven x (Just x) Nothing)
->>β (Just 3) (λx.isEven x (Just x) Nothing) Nothing
#   ... I'm omitting some tedious intermediate steps for brevity.
->>  isEven 3 (Just 3) Nothing
->>  False (Just 3) Nothing
->>  Nothing

If you were to pass in Just 2 or Just of any other even number, you'd get back the original Maybe value instead of Nothing.

Outlook

One of my favourite properties of lambda calculus is the composable nature of expressions.

We could easily build more complicated structures (trees, linked lists, etc.) from the functions discussed in this post. I might write a follow-up post :)

Thanks

I thank @Mafii for the the many helpful comments. All remaining errors are mine :)