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 A Type’A->A of elements, we can define lists of type A A in the following context :

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

'ListList_context.List???"List A"defconstrA'a->List'l->'consList_context.cons(al(.List.cons.nil))!!!"cons a l"defconstr!!'nilList_context.nil!!!"nil"defconstr['List'nil'cons]{export}each

>

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