# Example: Function Templates on Lists (Redux)

I have presented previously implementation of some commonly used function templates on lists formed with the constructors list0_nil and list0_cons. This time, I present as follows implementation of the corresponding function templates on lists formed with the constructors list_nil and list_cons, which make it possible to assign more accurate types to these templates.

Please find the entire code in this section plus some additional code for testing on-line.

## Appending: list_append

Given two lists xs and ys of the types list(T, I1) and list(T, I2) for some type T and integers I1 and I2, list_append(xs, ys) returns a list of the type list(T,I1+I2) that is the concatenation of xs and ys:

```fun
{a:t@ype}
list_append
{m,n:nat} .<m>.
(
xs: list(a, m)
, ys: list(a, n)
) : list(a, m+n) =
(
case+ xs of
| list_nil() => ys
| list_cons(x, xs) => list_cons(x, list_append<a>(xs, ys))
) (* end of [list_append] *)
```

Clearly, this implementation of list_append is not tail-recursive.

## Reverse Appending: list_reverse_append

Given two lists xs and ys of the type list(T, I1) and list(T, I2) for some type T and integers I1 and I2, list_reverse_append(xs, ys) returns a list of the type list(T, I1+I2) that is the concatenation of the reverse of xs and ys:

```fun
{a:t@ype}
list_reverse_append
{m,n:nat} .<m>.
(
xs: list(a, m)
, ys: list(a, n)
) : list(a, m+n) =
(
case+ xs of
| list_nil() => ys
| list_cons(x, xs) =>
list_reverse_append<a>(xs, list_cons(x, ys))
) (* end of [list_reverse_append] *)
```

Clearly, this implementation of list_reverse_append is tail-recursive.

## Reversing: list_reverse

Given a list xs, list_reverse(xs) returns the reverse of xs, which is of the same length as xs:

```fun
{a:t@ype}
list_reverse{n:nat} .<>. // defined non-recursively
(xs: list(a, n)): list(a, n) = list_reverse_append<a>(xs, list_nil())
// end of [list_reverse]
```

## Mapping: list_map

Given a list xs of the type list(T1, I) for some type T1 and integer I and a closure function f of the type T1 -<cloref1> T2 for some T2, list_map(xs) returns a list ys of the type list(T2, I):

```fun{
a:t@ype}
{b:t@ype
} list_map
{n:nat} .<n>.
(
xs: list(a, n), f: a -<cloref1> b
) : list(b, n) =
(
case+ xs of
| list_nil() => list_nil()
| list_cons(x, xs) => list_cons(f(x), list_map<a>(xs, f))
) (* end of [list_map] *)
```

Each element y in ys equals f(x), where x is the corresponding element in xs. Clearly, this implementation of list_map is not tail-recursive.

## Zipping: list_zip

Given two lists xs and ys of the types list(T1, I) and list(T2, I) for some types T1 and T2 and integer I, respectively, list_zip(xs, ys) returns a list zs of the type list((T1,T2), I).

```fun{
a,b:t@ype
} list_zip
{n:nat} .<n>.
(
xs: list(a, n)
, ys: list(b, n)
) : list((a, b), n) =
(
case+ (xs, ys) of
| (
list_nil()
, list_nil()
) => list_nil((*void*))
| (
list_cons(x, xs)
, list_cons(y, ys)
) => list_cons((x, y), list_zip<a,b>(xs, ys))
) (* end of [list_zip] *)
```

Each element z in zs equals the pair (x, y), where x and y are the corresponding elements in xs and ys, respectively. Clearly, this implementation of list_zip is not tail-recursive.

## Zipping with: list_zipwith

Given two lists xs and ys of the types list(T1, I) and list(T2, I) for some types T1 and T2 and integer I, respectively, and a closure function f of the type (T1, T2) -<cloref1> T3 for some type T3, list_zipwith(xs, ys, f) returns a list zs of the type list(T3, I):

```fun{
a,b:t@ype
}{c:t@ype
} list_zipwith
{n:nat} .<n>.
(
xs: list(a, n)
, ys: list(b, n)
, f: (a, b) -<cloref1> c
) : list(c, n) =
(
case+ (xs, ys) of
| (
list_nil()
, list_nil()
) => list_nil((*void*))
| (
list_cons(x, xs)
, list_cons(y, ys)
) =>
list_cons(f(x, y), list_zipwith<a,b><c>(xs, ys, f))
// end of (list_cons, list_cons)
) (* end of [list_zipwith] *)
```

Each element z in zs equals f(x, y), where x and y are the corresponding elements in xs and ys, respectively. Clearly, this implementation of list_zipwith is not tail-recursive.