Introduction to Programming in ATS:
<<< Previous	Datatype Refinement	Next >>>

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_cons (x, xs) => list_cons (x, list_append (xs, ys))
  | list_nil () => 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_cons (x, xs) =>
      list_reverse_append (xs, list_cons (x, ys))
  | list_nil () => 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 (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_cons (x, xs) => list_cons (f x, list_map (xs, f))
  | list_nil () => list_nil ()
// 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_cons (x, xs),
     list_cons (y, ys)) => list_cons ((x, y), list_zip (xs, ys))
  | (list_nil (), list_nil ()) => list_nil ()
// 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_cons (x, xs), list_cons (y, ys)) =>
      list_cons (f (x, y), list_zipwith (xs, ys, f))
  | (list_nil (), list_nil ()) => list_nil ()
// 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.

<<< Previous	Home	Next >>>
Datatype Refinement	Up	Example: Mergesort on Lists (Redux)