# Implementing lists in the simply typed lambda calculus

One of my goals this summer is to re-read Bob Carpenter’s *Type-Logical
Grammar* and to actually do (at least some of) the exercises. If I manage to
follow through with that goal, I’ll write up my solutions (or attempts at
solutions) to some of the more interesting or difficult exercises. I’ll start
that off with the last exercise from Chapter 2, which says to add to the simply
typed lambda calculus the type for lists of objects of type
. First, let me review Chapter 2 to set the stage.

## Review

Chapter 2 deals with the syntax, semantics, and proof theory of the simply typed lambda calculus. I’ll review here the syntax and semantics, but not the proof theory.

### Syntax

Carpenter builds up the set of types inductively from a set
of *basic types*, using just one type constructor: .

**Definition (types).** The set of *types* is the smallest set
such that

- .
- If , then .

A type of the form is called a *functional type*.

For each type , there is a set of variables of type and a set of constants of type . The set of lambda terms of type is defined as follows.

**Definition (terms).** The set of *(lambda) terms* of type is the
smallest set such that

- .
- .
- If and , then .
- If and and , then .

A term of the form , usually abbreviated
or , is a *functional application* of to .
However, a term with a functional type is not
a function per se— is (the result of) a *syntactic*
operation more akin to term concatenation than functional application.
Nevertheless, is called functional (it has a functional type)
because of how it is *interpreted semantically* (model theoretically).

### Semantics

In the model theory, functional terms denote functions in the normal mathematical sense. Before defining denotations, I need to define frames and models.

**Definition (frame).** A *frame* for the set is a
collection () of *basic domains*.

**Definition (model).** A *model* is a pair
in which is a frame, and is the *interpretation
function* mapping constants to the appropriate domain, i.e. if .

**Definition (denotation).** Given a model and a variable assignment , the
*denotation* of a term with
respect to and is given by:

- If , then .
- If , then .
- , assuming and are appropriately typed.
- such that , where is that variable assignment such that and for each .

Note that the left-hand side of the equality statement in (3) involves term
concatenation (function*al* application), whereas the right-hand side involves
real function application in the strict sense.

In other words, of type is a lambda term whose denotation is a function that maps (elements of the domain of) -type things to (elements of the domain of) -type things.

Carpenter goes on to give the usual axioms for the simply typed lamda calculus (-, -, and -reduction schemata) and the usual rules of inference (reflexivity, transitivity, congruence, and equivalence) and to prove that the resulting system is both sound and complete.

### Product and Sum Types

The latter part of the chapter adds product and sum types to the system. Product types allow functional terms to take multiple arguments at one time (in a certain sense), while sum types introduce functional terms that can act polymorphically.

## Exercise: List Types

Let me now turn to the actual exercise.

Consider adding for lists of objects of type . What would the terms look like in this scheme and how are they interpreted and treated proof-theoretically? Is there any gain in expressive power by admitting arbitrary lists? What might we do to interpret infinite sequences?

In this post, I’ll only address the first two questions: what do list terms look like, and how are they interpreted. For my answer, I’ll be borrowing from the functional programming language Haskell.

### Lists in Haskell

In Haskell, lists are things like `[3, 5, 0]`

, `["hello", "world"]`

, etc. The
order of list elements is important, and list elements can repeat. In that
sense, lists are more like tuples (sequences) than sets, except that whereas a
tuple (both in Haskell and in Carpenter’s section on product types) can contain
objects of all different types, list elements must all be of the *same* type.
For example, in Haskell, `(3, "hello")`

is a possible pair, consisting of an
integer and a string, but `[3, "hello"]`

is not a possible list.

In Haskell, the list type is written as `[a]`

, where `a`

is any type. For
example, `[3, 5, 0]`

has type `[Int]`

, while `["hello", "world"]`

has type
`[String]`

. (NB: In Haskell a string is itself a list of characters, i.e.
`String`

is just a type synonym for `[Char]`

.)

Note that Haskell overloads the symbols `[]`

: they are used to construct both
terms (Haskell expressions) and types.

I’ll follow Haskell’s lead by writing instead of Carpenter’s for the type of lists containing -type objects, and I’ll similarly overload the symbols .

### Syntax

I begin by adding to . I do so by adding the following clause to the definition of types:

- If , then .

So is a unary type constructor (it takes a single type and returns a new type), whereas is a binary type constructor (it takes two types and returns a new type).

As for terms, I assume that for each list type there is a set of variables of type and a set of constants of type . We now need a way to construct arbitrary list terms (similar to how abstraction lets us construct functional terms).

#### Haskell Detour

In Haskell, there are two list constructors: `[]`

, or *nil* (the empty list),
and `(:)`

, or *cons*. The cons operator has the following type signature:

```
(:) :: a -> [a] -> [a]
```

This means it takes something of type `a`

and something of type `[a]`

and
returns something of type `[a]`

. More precisely, it takes an `a`

-type
object—call it `x`

— and a list of `a`

-type objects—call it `list`

—and
it returns a new list, `list'`

, whose elements are `x`

followed by the elements
of `list`

. In other words, cons prepends its first argument (an object of type
`a`

) to the beginning of its second argument (a list of objects of type `a`

).
(Of course, in Haskell a pure function always returns a new object; it doesn’t
modify objects given as arguments, so cons does not *literally* prepend
anything to a given list, unlike, say, `list.insert(0, x)`

in Python.)

For example, to construct a list of integers (objects of type `Int`

), we start
with `[]`

of type `[Int]`

, and using `(:)`

we add to the front of `[]`

an
integer like `0`

to obtain `(:) 0 []`

, or using infix notation, `0 : []`

. The
result is of type `[Int]`

and is normally written as `[0]`

, which hides the
cons operator. From `[0]`

we can obtain `5 : [0]`

, written `[5, 0]`

, and from
that we can obtain `3 : [5, 0]`

, or `[3, 5, 0]`

, and so on.

More generally, `[x1, x2, ..., xN]`

is syntactic sugar for ```
x1 : ( x2 : ( ... (
xN : [] ) ... ) )
```

.

#### Back to Terms

Returning to our lambda terms, we want, for each type , a nil term of type , and a term constructor for adding an object of type to a list of type to produce a new such list. I do so by adding the following clauses to the definition of the set of terms of type .

- If , then .
- If and and , then .

Like functional application, is a binary term contructor: it takes two terms to produce a new term.

Following Haskell, I make the following conventions:

- .
- .

The latter schema can be applied recursively for any list of arbitrary length. For example

Since there is a one-to-one correspondence between -looking things and -looking things, one might wonder if we can instead reformulate (6) as follows (in two steps).

- If and , then .
- If and and , then .

(In other words, we can construct a singleton list from a single object, and a 2-element list from two objects.)

The problem is that (7) cannot be applied recursively. For example, from we can obtain by appyling (6), and from and we can obtain by applying (7). But we cannot apply (7) to, say, and to obtain because, although is of type , is not a term of any kind, let alone one of type .

For this reason, and for the sake of making cons explicit, I’ll stick with the first formulation of (6) above.

### Semantics

Now that I’ve added list types and list terms to the syntax, I need to add their denotations to the model theory, and this is where I’m a bit stuck, primarily because there are several options and I don’t know which is best/normal, or which one Carpenter has in mind.

If is of a list type, say , then the denotation of is in , but what precisely is the structure of ?

For example, functional terms denote functions, so the denotation of of type is a member of , i.e. a function from to . Product terms denote pairs (and more generally, tuples), so the denotation of of type is a member of . But what does/should a list of type denote, set theoretically? A flat set, i.e. a member of the power set of ? Probably not, because sets don’t care about order or repetition, whereas lists (as I’ve defined them) do. What about tuples, i.e. members of ? Maybe, but product terms already do that. Something else? I’m not sure.

A concrete example might help decide. Suppose we have the type
for individuals and that . Then we can create a list of these individuals,
, which is of type
. Suppose also that in some model ,
denotes , denotes , and
denotes , where .
Then what should the list of these three individuals denote? Probably *not* the
flat set , because then
and and would all denote the same set (at least if we
apply the most obvious denotation mapping), which is probably undesirable. One
reason for introducing lists in the first place is, I assume, so they can serve
as meaning representations for natural language expressions that care about
order and repetition.

Assuming, then, that we want these three lists to denote different things, the
only reasonable possibility I can think of is to map lists to tuples. For
example, will denote , which is an element of . In this way, list terms are essentially like product
terms, but with two main differences: (i) both products and lists denote
tuples, but lists are composed of objects of the *same* type, meaning that the
tuples they denote will contain objects from the *same* domain; and (ii) empty
and singleton lists are possible, whereas empty and singleton tuples are in
general (at least for Carpenter) not, as far as I can tell.

The following clauses get added to the definition of denotation.

- If and , then .
- , assuming and are appropriately typed.

Continuing the example above, denotes . And denotes . Rewriting tuples in the usual way (analogous to lists above), where , the latter denotation becomes .

So what is the structure of ? It’s a set whose members are tuples, of varying size, consisting of individuals (except the last tuple member, which is always except in the case of the empty tuple).

More generally, is a set whose members are tuples, of varying size, consisting of elements from .

This is different from the case of products: the domain of intepretation for, say, a pair of terms is , which contains only pairs, not tuples of any other size; and the domain of interpretation for, say, a triple of terms is , which contains only triples, not tuples of any other size. Hence, whereas, say, and have denotations in the same domain, and do not.

I’ll conclude by mentioning that it’s kind of weird to use in the denotation of lists, but this is necessary because the denotation function is a total function, and since the empty list, , is a term, it requires a denotation. If is of type , it doesn’t make sense for its denotation to include anything from , so we’re stuck with having it denote something like .

One way to avoid this would be to redefine lists: empty lists are simply not possible terms (objects). The smallest list would then be a singleton list, which would denote a -tuple, so would denote rather than , and would denote rather than .