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.

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:

Clearly, this implementation of list_append is not tail-recursive.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:

Clearly, this implementation of list_reverse_append is tail-recursive.Given a list xs, list_reverse(xs) returns the reverse of xs, which is of the same length as xs:

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):

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.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).

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.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] *)