Lists

An list is an inductively defined type that we can think of as sequences of elements from type . The inductive rules defining lists are:

In ML, the empty list is denoted by either nil or []. Lists are constructed using the infix . constructor: a.l. The selectors for lists are the functions hd, which retrieves the first part of the list: hd a.l = a; and tl, which retrieves the rest of the list: tl a.l = l.

Notice that lists are very similar to natural numbers in that they have inductive structure.

The rules defining lists are somewhat similar to the rules defining the natural numbers.

1. is an list.
2. If and then is an list.
3. There is nothing else.

similarly to the natural numbers.

Lists also have their own version of primitive recursive functions.

f(nil,y)	=	g(y)
f(cons(a,l),y)	=	h(a,l,f(l,y),y)

[Note: The Constable &Howe paper uses a linear form of recursion on lists. As an exercise, write recursion for in the linear form.]