Effective ATS:
Functional Programming with Combinators

Generally speaking (or by convention), the name combinator refers to a relatively small function for processing tree-like data (including lists). By a combinator-based style of programming, I mostly mean a style that puts a particular emphasis on making use of combinators in program construction.

A great strength in functional programming lies in its support for programming with combinators. In this article, I would like to present some code that makes extensive use of sequence-processing combinators, where a sequence may refer to either a list or a stream (that is, a lazy list) in ATS.

Listing Permutations

The first example I use for illustration is about listing all of the permutations of a given list. The following function permute is declared for this purpose:

//
extern
fun{
a:t@ype
} permute
  {n:nat}
(
xs: list(a, n)
) : list(list(a, n), fact(n))
//
Essentially, the type assigned to permute states that permute is a function taking a list of length N and returning a list of length fact(N) in which each element is itself a list of length N, where fact refers to the factorial function on natural numbers. Before implementing permute, I would like to first implement the following declared function permute0:
//
extern
fun{
a:t@ype
} permute0(xs: list0(a)): list0(list0(a))
//
where list0 is just an un-indexed version of list. Note that permute and permute0 do the same at run-time but the latter is given a simplied type when compared to the former. The implementation of permute0 given as follows can be said of typical combinator-based style:
//
implement
{a}(*tmp*)
permute0(xs) =
case+ xs of
| list0_nil() =>
  list0_sing
  (
     list0_nil()
  )
| list0_cons _ =>
  list0_concat
  (
    list0_map<(a, list0(a))><list0(list0(a))>
      (choose_1_rest(xs), lam(@(x, xs)) => list0_mapcons(x, permute0(xs)))
  )
//
The function list0_sing forms a singleton list, and the function list0_map forms a list by applying its second argument, which is a closure-function, to each element in its first argument, which is a list. The function list0_concat takes a list xss of lists and returns the concatenation of all of the lists in xss. As for list0_mapcons, it takes an element and a list of lists and then forms another list by putting the element to the front of each list in the list of lists. Finally, the function choose_1_rest takes a list xs and returns a list of pairs such that each pair consists of an element x and the list obtained from removing x from xs, where x ranges over all of the elements in xs. Please find as follows an implementation of choose_1_rest:
//
extern
fun
{a:t@ype}
choose_1_rest(xs: list0(INV(a))): list0(@(a, list0(a)))
//
implement
{a}(*tmp*)
choose_1_rest(xs) =
(
case+ xs of
| list0_nil() =>
  list0_nil()
| list0_cons(x1, xs2) =>
  list0_cons
  (
    (x1, xs2)
  , list0_map<(a, list0(a))><(a, list0(a))>
      (choose_1_rest(xs2), lam(xxs) => (xxs.0, list0_cons(x1, xxs.1)))
    // list0_map
  )
)
//
Please click here to try a completed program that prints out all of the permutations of (1, 2, 3).

The above implementation of permute0 can be readily turned into the following one for permute:

implement
{a}(*tmp*)
permute
{n}(xs) = let
//
extern
praxi
lemma_fact_0(): [fact(0)==1] void
extern
praxi
lemma_fact_1{n:pos}(): [fact(n)==n*fact(n-1)] void
//
in
//
case+ xs of
| nil() =>
  mylist_sing(nil()) where
  {
    prval () = lemma_fact_0()
  } (* end of [nil] *)
| cons _ => let
    prval () = lemma_fact_1{n}()
  in
  //
  mylist_concat
  (
    mylist_map<(a, list(a, n-1))><list(list(a, n), fact(n-1))>
      (mychoose_1_rest(xs), lam(@(x, xs)) => mylist_mapcons(x, permute(xs)))
  )
  //
  end // end of [cons]
//
end // end of [permute]
where the involved combinators are assigned the following types:
extern
fun
{a:t@ype}
mylist_sing(x: a): list(a, 1)
extern
fun
{a:t@ype}
mylist_concat{m,n:int}(list(list(INV(a), n), m)): list(a, m*n)
extern
fun
{a:t@ype}
mylist_mapcons{m,n:int}(a, list(list(INV(a), n), m)): list(list(a, n+1), m)
extern
fun
{a:t@ype}
{b:t@ype}
mylist_map{n:int}(list(INV(a), n), a -<cloref1> b): list(b, n)
extern
fun
{a:t@ype}
mychoose_1_rest{n:int}(xs: list(INV(a), n)): list(@(a, list(a, n-1)), n)

Depth-First Search

As another example of programming with combinators, I present a high-level implementation of tree-based depth-first search. In the following declaration, node is introduced as an abstract type (for nodes in a given tree to be searched) and nodes as an alias for the type list0(node), which is for lists of nodes:

abstype node
typedef nodes = list0(node)
Let us further assume the availability of a function of the name node_get_children for obtaining the children of a given node:
//
extern
fun
node_get_children(nx: node): nodes
//
overload .children with node_get_children
//
With the dot-notation overloading, one can write nx.children() for node_get_children(nx).

The following declared function depth_first_search essentially pre-orderly lists all of the nodes in each tree rooted at one of given nodes:

//
extern
fun
depth_first_search(nxs: nodes): nodes
//
A specification-like implementation for depth_first_search is given as follows:
//
implement
depth_first_search
  (nxs) =
(
if iseqz(nxs)
  then list0_nil()
  else let
    val nx0 = nxs.head()
  in
    list0_cons(nx0, depth_first_search(nx0.children() + nxs.tail()))
  end // end of [else]
) (* end of [depth_first_search] *)
//
where the symbol + is overloaded with list0_append for concatenating two given list0-values.

The use of list0 in the above implementation of depth_first_search can result in great inefficiency both time-wise and memory-wise. For instance, by calling depth_first_search on a given node, one generates a list containing all of the nodes in the tree rooted at the given node; this generated list can potentially be of great size, requiring long time to compute as well as large memory to store.

By replacing list0 with stream_vt (for linear streams) in the definition of nodelst, I give as follows another implementation of depth_first_search that can be seen as a close variant of the above one:

//
implement
depth_first_search
  (nxs) = $ldelay(
//
(
case+ !nxs of
| ~stream_vt_nil() =>
    stream_vt_nil((*void*))
| ~stream_vt_cons(nx0, nxs) =>
    stream_vt_cons(nx0, depth_first_search(nx0.children() + nxs))
)
,
~(nxs) // HX: for freeing the stream!
//
) (* end of [depth_first_search] *)
//
Due to the very nature of lazy-evaluation, each node in the stream returned by a call to depth_first_search is computed only if it is needed subsequently. For instance, if one only needs to find the first node in the stream satisfying some property, then no following nodes are ever computed. Additionally, linear lazy-evaluation (stream_vt) means that only the latest computed node needs to be kept at any point during evaluation, saving the memory that would otherwise be needed for storing all of the previously computed nodes.

Breadth-First Search

A specification-like implementation of tree-based breadth-first search is given as follows:

//
extern
fun
breadth_first_search
  (nxs: nodes): nodes
//
implement
breadth_first_search
  (nxs) =
(
if iseqz(nxs)
  then list0_nil()
  else let
    val nx0 = nxs.head()
  in
    list0_cons(nx0, breadth_first_search(nxs.tail() + nx0.children()))
  end // end of [else]
) (* end of [breadth_first_search] *)
//
While this implementation is functionally correct, its can be impractical. Clearly, processing one node involves evaluating the code nxs.tail() + nx0.children(), which can be both time-consuming and memory-consuming as the list nxs.tail() can be exponentially long (in terms of tree-height). One method for addressing this issue is to replace the list-based sequence representation with one that can support efficient concatenation (for instance, one based on finger-trees). I leave it as an exercise for the interested reader to experiment with such a method.

As in the case of depth-first search, another implementation of breadth_first_search can be given as follows where list0 in the definition of nodelst is replaced with stream_vt:

//
implement
breadth_first_search
  (nxs) = $ldelay(
//
(
case+ !nxs of
| ~stream_vt_nil() =>
    stream_vt_nil((*void*))
| ~stream_vt_cons(nx0, nxs) =>
    stream_vt_cons(nx0, breadth_first_search(nxs + nx0.children()))
)
,
~(nxs) // HX: for freeing the stream!
//
) (* end of [breadth_first_search] *)
//
When the objective is to find one node satisfying certain property, this stream-based implementation of breadth-first search can actually be quite attractive.

Queen Puzzle

The famous 8-queen puzzle asks the player to find ways to put eight queen pieces on a chess board such that no queen piece can attack any other ones. In other words, no two queen pieces can be put on the same row, the same column, or the same diagnal. This puzzle can be readily solved with a tree-based search. Let a node be represented by a list xs of integers:

assume node = list0(int)
For each valid index i, the integer xs[i] stands for the column number of the queen piece on row n-1-i, where n refers to the length of xs. More precisely, a given integer list of length n represents a partial configuration of chess board containing n queen pieces with no piece being able to attack any other ones. As for node_get_children, we can implement it as follows:
implement
node_get_children
  (nx) = let
//
#define N 8
//  
fn
test
// testing whether putting a queen piece
// at position i on the next row is safe
(
  i: int, nx: node
) = (nx).iforall()(lam (d, j) => (i != j) && (abs(i-j) != d+1))
//
in
  ((N).stream_vt_map(TYPE{node})(lam(i) => list0_cons(i, nx))).filter()(lam nx => test(nx.head(), nx.tail()))
end // end of [node_get_children]
Calling node_get_children on a given node returns all of the nodes that extend the given one with one more queen piece. A solution to the 8-queen puzzle is just a node containing 8 integers, and the following (linear) stream theSolution consists of all of such nodes:
//
val
theSolutions =
(depth_first_search(stream_vt_make_sing(list0_nil()))).filter()(lam nx => length(nx) = N)
//

Please click here to try a completed program that prints out the first two solutions to the 8-queen puzzle.

Compiling and Testing

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

permute.dats // listing permutations
depth-first.dats // dfs using list-based sequence representation
depth-first-2.dats // dfs using stream-based sequence representation
breadth-first.dats // bfs using list-based sequence representation
breadth-first-2.dats // bfs using stream-based sequence representation
queen-puzzle-dfs-2.dats // solving 8-queen puzzle with depth-first-2
In addition, there is an accompanying Makefile for compiling and testing the code.


This article is written by Hongwei Xi.