Lists : a general sequence of elements

Sometimes in life, we want to do a series of tasks in a certain order, or sort objects in a sequence. In mathematical disciplines, lists play a similar semantic role, allowing us to express sequences of related elements.

The elements of a sequence

The simplest kind of list is either an empty list, or a list containing one element, followed by another list. Given a type of elements, we can define lists of type in the following context :

Armed with this context, defining the usual constructors for the List type and its members becomes easy :

The list recursor, , has type . We can now start to define non-trivial combinators that work on lists, such as “map” and “append” :

List combinators

list_map has type .

list_append has the type .