Introduction to Programming in ATS:
PrevChapter 10. Datatype RefinementNext

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.

PrevHomeNext
Datatype RefinementUpExample: Mergesort on Lists (Redux)