Effective ATS:
List-folding Combinators

A list-folding combinator is a (higher-order) function that traverses a given list to process the elements contained in the list. In this very light article (based on a lecture of mine on introductory functional programming), I present some code implementing 3 list-folding combinators as well as several examples making use of these combinators.

List_fold_left

The function list_fold_left of the following interface folds a given list from left to right: 

fun
{a,b:t@ype}
list_fold_left
(
  xs: List(a)
, init: b, fopr: (b, a) -<cloref1> b
) : b // end-of-function
Applied to a list of n elements (x1, ..., xn), list_fold_left essentially returns the value of the following (informal) expression: fopr(...fopr(init, x1), ..., xn). The following code gives a typical implementation of list_fold_left: 
implement
{a,b}(*tmp*)
list_fold_left
  (xs, init, fopr) = let
//
fun
auxmain
{n:nat} .<n>.
(
  init: b, xs: list(a, n)
) : b = (
//
case+ xs of
| list_nil() => init
| list_cons(x, xs) =>
    auxmain(fopr(init, x), xs)
  // end of [list_cons]
//
) (* auxmain *)
//
prval () = lemma_list_param(xs)
//
in
  auxmain(init, xs)
end // end of [list_fold_left]
Note that auxmain is tail-recursive.

As an example, the list-length function can be implemented with a direct call to list_fold_left: 

fun
{a:t@ype}
list_length
(
  xs: List(a)
) : int =
(
//
list_fold_left<a,int>
  (xs, 0, lam(xs, x) => xs + 1)
//
) (* list_length *)
However, it should be noted that this implementation of list_length cannot be assigned the following interface: 
fun
{a:t@ype}
list_length{n:nat}(list(a, n)): int(n)
In order to do so, a more accurate interface needs to be given to list_fold_left.

As another example, the list-reverse function can be implemented with a direct call to list_fold_left as follows: 
fun
{a:t@ype}
list_reverse
(
  xs: List(a)
) : List0(a) =
(
//
list_fold_left<a,List0(a)>
  (xs, list_nil(), lam(xs, x) => list_cons(x, xs))
//
) (* list_reverse *)
Note that the type constructor List0 is defined as follows: 
typedef List0(a:t@ype) = [n:nat] List(a)

List_fold_right

The function list_fold_right of the following interface folds a given list from right to left: 

fun
{a,b:t@ype}
list_fold_right
(
  xs: List(a)
, fopr: (a, b) -<cloref1> b, sink: b
) : b // end-of-function
Applied to a list of n elements (x1, ..., xn), list_fold_right essentially returns the value of the followng (informal) expression: fopr(x1,...fopr(xn, sink)...). The following code gives a typical implementation of list_fold_right: 
implement
{a,b}(*tmp*)
list_fold_right
  (xs, fopr, sink) = let
//
fun
auxmain
{n:nat} .<n>.
(
  xs: list(a, n)
) : b = (
//
case+ xs of
| list_nil() => sink
| list_cons(x, xs) => fopr(x, auxmain(xs))
//
) (* auxmain *)
//
prval () = lemma_list_param(xs)
//
in
  auxmain(xs)
end // end of [list_fold_right]
Note that auxmain is recursive but not tail-recursive.

As an example, the list-length function can be implemented with a direct call to list_fold_right: 

fun
{a:t@ype}
list_length
(
  xs: List(a)
) : int =
(
//
list_fold_right<a,int>
  (xs, lam(x, xs) => xs + 1, 0)
//
) (* list_length *)
Compared to the implementation of list_length based on list_fold_left, this one is much less attractive as it is not tail-recursive and thus may cause a call-stack overflow when applied to a long list (for instance, one containing 1 million elements).

As another example, the list-append function (for concatenating two given lists) can be implemented with a direct call to list_fold_right as follows: 
fun
{a:t@ype}
list_append
(
  xs: List(a), ys: List(a)
) : List0(a) = let
//
prval () = lemma_list_param(ys)
//
in
//
list_fold_right<a,List0(a)>
  (xs, lam(x, xs) => list_cons(x, xs), ys)
//
end (* list_append *)
In practice, it is not uncommon to see an implementation of the list-reverse function (for reversing a given list) of the following style (usually by a novice functional programmer): 
fun
{a:t@ype}
list_reverse
(
  xs: List(a)
) : List0(a) =
(
//
list_fold_right<a,List0(a)>
( xs
, lam(x, xs) =>
  list_append<a>(xs, list_cons(x, list_nil()))
, list_nil((*void*))
) (* end of [list_fold_right] *)
//
) (* list_reverse *)
This is a terribly inefficient implementation of O(n2)-complexity both time-wise and memory-wise, and any programmer who writes this kind of code is surely in need of solidifying his/her own understanding of the call-by-value semantics.

The following code implements based on list_fold_right a function searching for the rightmost element satisfying a given prediate in a given list: 

fun
{a:t@ype}
list_find_rightmost
(
  xs: List(a), p: (a) -<cloref1> bool
) : Option(a) = let
//
exception Found of (a)
//
in
//
try let
//
val _ =
list_fold_right<a,int>
( xs
, lam(x, xs) =>
  if p(x) then $raise(Found(x)) else (0)
, 0(*nominal*)
)
//
in
  None((*void*))
end with ~Found(x) => Some(x)
//
end (* end of [list_find_rightmost] *)
Note that the fopr argument passed to list_fold_right in this case is a function that raises an exception carrying the element being processed if the element satsifies the given predicate. As the type void may cause difficulty for the generated C code to be compiled properly, the type int is chosen instead for the result returned by the call to list_fold_right.

List_fold_split

Lists are inherently sequential, and traversing a list is mostly likely done in a from-left-to-right or from-right-to-left manner. There are however realistic occasions where one may want to traverse a list in a tree-like manner. For instance, list-mergesort can be implemented by first splitting a given list into two halves and then recursively sorting them and merging the two obtained sorted lists into one. The following function list_fold_split can be seen as a form of abtraction over mergesort: 

fun
{a,b:t@ype}
list_fold_split
(
  xs: List(a)
, fopr: (b, b) -<cloref1> b
, sink0: b, fsink1: (a) -<cloref1> b
) : b // end-of-function
If a given list contains at least two elements, list_fold_split splits it into two halves and then applies recursively to them to yield two results that are subsequently combined together by a call to fopr; if the given list is empty, then sink0 is the result; if the given list is a singleton, the fsink1 is called on the only element to yield the result. The following code gives an implementation of list_fold_split: 
implement
{a,b}(*tmp*)
list_fold_split
  (xs, fopr, sink0, fsink1) = let
//
fun
aux
{ n1,n2:nat
| n1 >= n2 } .<n2>.
(
  xs: list(a, n1), n2: int(n2)
) : b =
(
if
(n2 >= 2)
then let
  val n21 = half(n2)
in
  fopr(aux(xs, n21), aux(list_drop(xs, n21), n2-n21))
end // end of [then]
else (
//
case+ xs of
| list_nil() => sink0
| list_cons(x, _) => fsink1(x)
//
) (* end of [else] *)
//
) (* end of [aux] *)
//
prval () = lemma_list_param(xs)
//
in
  aux(xs, length(xs))
end // end of [list_fold_split]
Given a list and a natural number n less than or equal to the length of the list, list_drop returns another list obtained from removing the first n elements from the given list. Clearly, list_drop is O(n)-time. Assume that fsink1 is O(1)-time. If fopr is O(1)-time, then list_fold_split is O(n(log(n)))-time. If fopr is O(n)-time, then list_fold_split is O(n(log(n)))-time as well.

Unsuprisingly, list-mergesort can be implemented with a direct call to list_fold_split where the fopr argument is the standard function for merging two sorted lists into one: 

local
//
fun{
a:t@ype
} merge
(
  xs0: list0(a)
, ys0: list0(a)
) : list0(a) =
(
case+ (xs0, ys0) of
| (list0_nil(), _) => ys0
| (_, list0_nil()) => xs0
| (list0_cons(x0, xs1), 
   list0_cons(y0, ys1)) => let
    val sgn = gcompare_val_val<a>(x0, y0)
  in
    if sgn <= 0
      then list0_cons(x0, merge(xs1, ys0))
      else list0_cons(y0, merge(xs0, ys1))
  end // end of [cons _, cons _]
)
//
in (* in-of-local *)
//
fun
{a:t@ype}
mergesort(xs: List(a)) =
list_fold_split<a,list0(a)>
( xs
, lam(xs, ys) => merge<a>(xs, ys)
, list0_nil(), lam(x) => list0_sing(x)
)
//
end // end of [local]
As another example, the list-reverse function can be implemented as follows: 
fun
{a:t@ype}
list_reverse
(
  xs: List(a)
) : List0(a) =
(
//
list_fold_split<a,List0(a)>
( xs
, lam(xs, ys) => list_append(ys, xs)
, list_nil, lam(x) => list_cons(x, list_nil)
) (* list_fold_split *)
//
) (* list_reverse *)
Note that this implementation of list_reverse is O(n(log(n)))-time. While it is better than the previous one of O(n2)-time, it is still unacceptably poor as reversing a list can be readily given a tail-recursive implementation of O(n)-time.

Compiling and Testing

Please find in the following files the entirety of the code presented in this article: 

list_fold_left.dats
list_fold_right.dats
list_fold_split.dats
In addition, there is an accompanying Makefile for compiling and testing the code.

This article is written by Hongwei Xi.