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 makeObj \text{makeObj} that takes two parameters type\text{type} and value\text{value} and returns a function wrapping that data.

def makeObj type value=λs.(s type value) \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.

def selectFirst=λfirst.λsecond.firstdef type obj=obj selectFirst \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:

def myObj ⟨type⟩ ⟨value⟩=λs.(s ⟨type⟩⟨value⟩) \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.

type myObj=myObj selectFirst=λs.(s ⟨type⟩⟨value⟩) selectFirst=(selectFirst ⟨type⟩⟨value⟩)(by substituting s with selectFirst)=(λfirst.λsecond.first ⟨type⟩ ⟨value⟩)(by definition of selectFirst)=(λsecond.⟨type⟩)(by substituting first with ⟨type⟩)=⟨type⟩ \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:

def selectSecond=λfirst.λsecond.seconddef value obj=obj selectSecond \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:

def boolType=onedef istype t obj=equal (type obj) tdef isbool=istype boolType \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.

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

which expands as:

λvalue.λs(s boolType value) trueλs(s boolType true) \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.