Lambda calculus is a very simple language. If you take away any syntactic sugar, all you are left with is functions that take arguments and return results. You can use these simple building blocks to construct functions that represent numbers and arithmetic, but there is no way to restrict, for example, arithmetic functions to require numeric operands. This is where types come in. Generally speaking, types allow you to control the use of functions so that only meaningful combinations of inputs and outputs are used.

Since lambda calculus is represented entirely using functions, we have no
choice but to represent typed objects as functions too. The most
straightforward way to do this is representing an object as a tuple with
a `type`

and a `value`

. To do so, we create a new function \( \text{makeObj} \) that takes two parameters \(\text{type}\) and
\(\text{value}\) and returns a function wrapping that data.

$$ \text{def} \ \text{makeObj} \ \text{type} \ \text{value} = \lambda \text{s}.(\text{s}\ \text{type}\ \text{value}) $$

The interesting part here is that the object is wrapped in a function — because that’s all we have in lambda calculus. To access the type, we define a selector function that simply returns the first value of a function.

$$ \begin{aligned} \text{def} \ \text{selectFirst} & = \lambda \text{first} . \lambda \text{second} . \text{first} \cr \text{def} \ \text{type} \ \text{obj} & = \text{obj} \ \text{selectFirst} \end{aligned} $$

Let’s see how we can use these functions to define a (type, value) pair and then access the type. We use angle brackets to define an arbitrary type and value. First, let’s define an object:

$$ \text{def} \ \text{myObj} \ \langle \text{type} \rangle \ \langle \text{value} \rangle = \lambda \text{s}.(\text{s}\ \langle \text{type} \rangle \langle \text{value} \rangle) $$

Now, let’s access the type of the object by applying the `type`

function
I previously defined.

$$ \begin{aligned} \text{type} \ \text{myObj} & = \text{myObj} \ \text{selectFirst} & \cr & = \lambda \text{s}.(\text{s}\ \langle \text{type} \rangle \langle \text{value} \rangle) \ \text{selectFirst} & \cr & = (\text{selectFirst}\ \langle \text{type} \rangle \langle \text{value} \rangle) & (\text{by substituting s with selectFirst}) \cr & = (\lambda \text{first}.\lambda \text{second}.\text{first} \ \langle \text{type} \rangle \ \langle \text{value} \rangle) & (\text{by definition of selectFirst}) \cr & = (\lambda \text{second}.\langle\text{type}\rangle) & (\text{by substituting first with } \langle \text{type} \rangle) \cr & = \langle\text{type}\rangle \end{aligned} $$

The value of an object is accessed similarly, using a selector function that returns the second of two arguments:

Now, we have a method for creating typed objects that are represented as
a `type`

, `value`

tuple. The representation of an object is a function
that accepts a function as a parameter. That parameter, when applied,
selects either the `type`

or the `value`

of the object. Given this base,
we can start looking at how to perform typed operations on such typed
objects. As a concrete example, we can look at how to perform typed
boolean operations.

Types in lambda calculus do not exist. Rather, they are built up from
functions as we have just seen. We can define similar functions for
checking the type of an object. We do this by defining types to be simple
numbers and then using using a new function `istype`

defined in terms of
`equal`

— a function we won’t define here but will assume to exist — to
check for a specific type:

$$ \begin{aligned} \text{def} \ \text{boolType} & = \text{one} \cr \text{def} \ \text{istype} \ \text{t} \ \text{obj} & = \text{equal} \ (\text{type}\ \text{obj})\ \text{t} \cr \text{def} \ \text{isbool} & = \text{istype} \ \text{boolType} \end{aligned} $$

We can then construct a boolean type using our previously defined `makeObj`

function and check that, indeed, the type is correct.

$$ \text{makeObj} \ \text{boolType} \ \text{true} $$

which expands as:

$$ \lambda \text{value}.\lambda\text{s}(\text{s} \ \text{boolType}\ \text{value})\ \text{true} \lambda\text{s}(\text{s} \ \text{boolType}\ \text{true}) $$

which defines an object of type `boolType`

with value `true`

. The type
and value would be extracted using the selector functions previously
defined. From this definition, we can build up larger and larger functions
that depend on typed arguments. Full details are available in the book An
Introduction to Functional Programming Through Lambda
Calculus.