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:

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

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.