# Maybe in λ-calculus

Read along as I implement the Maybe type and some useful functions for working on Maybe values 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:

### 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:

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`

:

`Just`

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

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 `Maybe`

s».

Perhaps the simplest example is to use `bind`

with the `Just`

function^{1}. 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^{2}.

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:

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:

We'll define an `isEven`

predicate for the purpose of testing our filter function:

And here's the definition of `not`

:

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

^{1}

This is in fact the right identity law for monads.

^{2}

In Haskell, this operation is known as `fmap`

and is part of the `Functor`

type class.