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.