A Running Program

The following example is a program in ATS that prints out (onto the console) the string "Hello, world!" plus a newline before it terminates:

//
val _ = print ("Hello, world!\n")
//
implement main0 () = () // a dummy for [main]
//

The function main0 is a slight variant of another function named main, which is of certain special meaning in ATS. For a programmer who knows the C or Java programming language, I simply point out that the role of main is essentially the same as its counterpart of the same name in C or Java. The keyword implement initiates the implementation of a function whose interface has already been declared elsewhere. Following is the declared interface for main0 in ATS:

fun main0 (): void

Suppose that you have already installed the ATS programming language system. You can issue the following command-line to generate an executable named hello in the current working directory:

atscc -o hello hello.dats

A Template for Single-File Programs

The following code template, which is available on-line, is designed for constructing a single-file program in ATS:

(*
**
** A template for single-file ATS programs
**
*)

(* ****** ****** *)
//
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
//
(* ****** ****** *)

//
// please write your program in this section
//

(* ****** ****** *)

implement main0 () = () // a dummy implementation for [main]

A Makefile Template

The following Makefile template, which is available on-line, is provided to help you construct your own Makefile for compiling ATS programs. If you are not familiar with the make utility, you could readily find plenty resources on-line to help yourself learn it.

######
#
# Note that
# certain installations require the following changes:
#
# atscc -> patscc
# atsopt -> patsopt
# ATSHOME -> PATSHOME
#
######
#
ATSHOMEQ="$(ATSHOME)"
#
######
#
ATSCC=$(ATSHOMEQ)/bin/atscc
ATSOPT=$(ATSHOMEQ)/bin/atsopt
#
######
#
#
# HX: Please uncomment the one you want, or skip it entirely
#
ATSCCFLAGS=
# ATSCCFLAGS=-O2
#
# '-flto' enables link-time optimization such as inlining lib functions
#
# ATSCCFLAGS=-O2 -flto
#
#
######
#
cleanall::
#
######
#
# Please uncomment the following three lines and replace the name [foo]
# with the name of the file you want to compile
#
# foo: foo.dats ; \
#   $(ATSCC) $(ATSCCFLAGS) -o $@ $< || echo $@ ": ERROR!!!"
# cleanall:: ; $(RMF) foo
#
######
#
# You may find these rules useful
#
# %_sats.o: %.sats ; $(ATSCC) $(ATSCCFLAGS) -c $< || echo $@ ": ERROR!!!"
# %_dats.o: %.dats ; $(ATSCC) $(ATSCCFLAGS) -c $< || echo $@ ": ERROR!!!"
#
######
#
RMF=rm -f
#
######
#
clean:: ; $(RMF) *~
clean:: ; $(RMF) *_?ats.o
clean:: ; $(RMF) *_?ats.c
#
cleanall:: clean
#
###### end of [Makefile] ######

Expressions and Values

ATS is both syntax-rich and feature-rich, and its grammar is probably more complex than most existing programming languages. In ATS, there are a large variety of forms of expressions, which I will introduce gradually.

Let us first start with some integer arithmetic expressions (IAEs): 1, ~2, 1+2, 1+2*3-4, (1+2)/(3-4), etc. Note that the negative sign is represented by the tilde symbol (~) in ATS. There is also support for floating point numbers, and some floating point constants are given here: 1.0, ~2.0, 3., 0.12345, 2.71828, 31416E-4, etc. Note that 3. and 31416E-4 are the same as 3.0 and 3.1416, respectively. What I really want to emphasize at this point is that 1 and 1.0 are two distinct numbers in ATS: the former is an integer while the latter is a floating point number (of double precision).

There are also boolean constants: true and false. We can form boolean expressions such as 1 >= 0, not(2-1 >= 2), (1 < 2) andalso (2 < 3) and (~1 > 1) orelse (~1 <= 1), where not, andalso and orelse stand for negation, conjunction and disjunction, respectively. For programmers familiar with C-like syntax, I point out that operators && and || are synonyms for andalso and orelse, respectively.

Other commonly used constant values include characters and strings. For instance, following are some character constants: 'a', 'B', '\n' (newline), '\t' (tab), '\(' (left parenthesis), ')' (right parenthesis), '\{' (left curly brace), '}' (right curly brace), etc; following are some string constants: "My name is Zoe", "Don't call me \"Chloe\"", "this is a newline:\n", etc.

Given a (function) name, say, foo, and an expression exp, the expression foo(exp) is a function application or function call. The parentheses in foo(exp) may be dropped if no ambiguity is created by doing so. For instance, print("Hello") is a function application, which can also be written as print "Hello". If foo is a nullary function, then a function application foo() can be formed. If foo is a binary function, then a function application foo(exp1, exp2) can be formed for expressions exp1 and exp2. Functions of more arguments can be treated accordingly.

Note that we cannot write +(1,2) as the name + has already been given the infix status requiring that it be treated as an infix operator. However, we can write op+(1,2), where op is a keyword in ATS that can be used to temporarily suspend the infix status of any name immediately following it. I will explain in detail the issue of fixity (prefix, infix and postfix) elsewhere.

Values are essentially expressions of certain special forms, which cannot be reduced or simplified further. For instance, integer constants such as 1 and ~2 are values, but the integer expression 1+2 is not a value, which can be reduced to the value 3. Evaluation refers to the computational process that reduces a given expression into a value. However, certain expressions such as 1/0 cannot be reduced to a value, and evaluating such an expression must abort at some point. I will gradually present more information on evaluation.

Names and Bindings

A crucial aspect of a programming language is the mechanism it provides for binding names, which are themselves expressions, to expressions. For instance, a declaration is introduced by the following syntax that declares a binding between the name x, which is also referred to as a variable, and the expression 1+2:

val x = 1 + 2

Note that val is a keyword in ATS, and the declaration is classified as a val-declaration. Conceptually, what happens at run-time in a call-by-value language such as ATS is that the expression 1+2 is first evaluated to the value 3, and then the binding between x and 1+2 is finalized into a binding between x and 3. Essentially, call-by-value means that a binding between a name and an expression needs to be finalized into one between the name and the value of the expression before it can be used in evaluation subsequently. As another example, the following syntax declares three bindings, two of which are formed simultaneously in the first line:

val PI = 3.14 and radius = 10.0
val area = PI * radius * radius

Note that it is unspecified in ATS as to which of the first two bindings (connected by the keyword and) is finalized ahead of the other at run-time. However, it is guaranteed that the third binding is finalized after the first two are done. To see this issue from a different angle, we can try to typecheck the following code:

val x = 0 and y = x + 1

Scopes for Bindings

Each binding is given a fixed scope in which the binding is considered legal or effective. The scope of a toplevel binding in a file starts from the point where the binding is introduced until the very end of the file. The bindings introduced in the following example between the keywords let and in are effective until the keyword end is reached:

val area = let
  val PI = 3.14 and radius = 10.0 in PI * radius * radius
end // end of [let]

Such bindings are referred to as local bindings, and the names such as PI and radius are referred to as local names. This example can also be written in the following style:

val area =
  PI * radius * radius where {
  val PI = 3.14 and radius = 10.0 // simultaneous bindings
} // end of [where] // end of [val]

The keyword where appearing immediately after an expression introduces bindings that are solely effective for evaluating names contained in the expression. Note that expressions formed using the keywords let and where are often referred to as let-expressions and where-expressions, respectively. The former can always be translated into the latter directly and vice versa. Which style is better? I have not formed my opinion yet. The answer seems to entirely depend on the taste of the programmer.

The following example demonstrates an alternative approach to introducing local bindings:

local

val PI = 3.14 and radius = 10.0

in (* in-of-local *)

val area = PI * radius * radius

end // end of [local]

Environments for Evaluation

Evaluation is the computational process that reduces expressions to values. When performing evaluation, we need not only the expression to be evaluated but also a collection of bindings that map names in the expression to values. This collection of bindings, which is just a finite mapping, is often referred to as an environment (for evaluation). For instance, suppose that we want to evaluate the following expression:

let
  val PI = 3.14 and radius2 = 10.0 * 10.0 in PI * radius2
end

Static Semantics

ATS is a programming language equipped with a highly expressive type system rooted in the Applied Type System framework, which also gives ATS its name. I will gradually introduce the type system of ATS, which is probably the most outstanding and interesting part of this book.

It is common to treat a type as the set of values it classifies. However, I find it more approriate to treat a type as a form of meaning. There are formal rules for assigning types to expressions, which are referred to as typing rules. If a type T can be assigned to an expression, then I say that the expression possesses the static meaning (semantics) represented by the type T. Note that an expression may be assigned many distinct static meanings. An expression is well-typed if there exists a type T such that the expression can be assigned the type T.

If there is a binding between a name and an expression and the expression is of some type T, then the name is assumed to be of the type T in the effective scope of the binding. In other words, the name assumes the static meaning of the expression it refers to.

Let exp0 be an expression of some type T, that is, the type T can be assigned to exp0 according to certain typing rules. If we can evaluate exp0 to exp1, then exp1 can also be assigned the type T. In other words, static meaning is an invariant under evaluation. This property is often referred to as type preservation, which is part of the soundness of the type system of ATS. Based on this property, we can readily infer that any value is of the type T if exp0 can be evaluated to it (in multiple steps).

Let exp0 be an expression of some type T. Assume that exp0 is not a value. Then exp0 can always be evaluated one step further to another expression exp1. This property is often referred to as progress, which is another part of the soundness of the type system of ATS.

Primitive Types

The simplest types in ATS are primitive types, which are used to classify primitive values. For instance, we have the primitive types int and double, which classify integers (in a fixed range) and floating point numbers (of double precision), respectively.

In the current implementation of ATS (Postiats), a program in ATS is first compiled into one in C (conforming to the C99 standard), which can then be compiled to object code by a compiler for C such as gcc. In the compilation from ATS to C, each of the types int, double and void in ATS is translated to the type of the same name in C.

There are many other primitive types in ATS, and I will introduce them gradually. Some commonly used primitive types are listed as follows:

• bool: This type is for boolean values true and false, and it is translated into the int type in C.

• char: This type is translated into the type in C for characters.

• schar: This type is translated into the type in C for signed characters.

• uchar: This type is translated into the type in C for unsigned characters.

• float: This type is translated into the type in C for floating point numbers of single precision.

• uint: This type is translated into the type in C for unsigned integers.

• lint: This type is translated into the type in C for long integers.

• ulint: This type is translated into the type in C for unsigned long integers.

• llint: This type is translated into the type in C for long long integers.

• ullint: This type is translated into the type in C for unsigned long long integers.

• size_t: This type is translated into the type in C of the same name, which is for unsigned integers of certain precision. Usually, the type size_t can be treated as the type ulint and vice versa.

• ssize_t: This type is translated into the type in C of the same name, which is for signed integers of certain precision. Usually, the type ssize_t can be treated as the type lint and vice versa.

• sint: This type is translated into the type in C for short integers.

• usint: This type is translated into the type in C for unsigned short integers.

• string: This type is for strings, and its translation in C is the type for pointers. I will explain this translation elsewhere.

Tuples and Tuple Types

Given two types T1 and T2, we can form a tuple type (T1, T2), which can also be written as @(T1, T2). Assume that exp1 and exp2 are two expressions of the types T1 and T2, respectively. Then the expression (exp1, exp2), which can also be written as @(exp1, exp2), refers to a tuple of the tuple type (T1, T2). Accordingly, we can form tuples and tuple types of more components. In order for a tuple type to be assigned to a tuple, the tuple and the tuple type must have the equal number of components.

When evaluating a tuple expression, we evaluate all of its components sequentially. Suppose that the expression contains n components, then the value of the expression is the tuple consisting of the n values of the n components listed in the order as the components themselves.

A tuple of length n for n >= 2 is just a record of field names ranging from 0 until n-1, inclusive. Given an expression exp of some tuple type (T1, T2), we can form expressions (exp).0 and (exp).1, which are of types T1 and T2, respectively. Note that the expression exp does not have to be a tuple expression. For instance, exp may be a name or a function application. If exp evaluates to a tuple of two values, then exp.0 evaluates to the first value and exp.1 the second value. Clearly, if the tuple type of exp contains more components, what is stated can be generalized accordingly.

In the following example, we first construct a tuple of length 3 and then introduce bindings between 3 names and all of the 3 components of the tuple:

val xyz = ('A', 1, 2.0)
val x = xyz.0 and y = xyz.1 and z = xyz.2

val xyz = ('A', 1, 2.0)
val (x, y, z) = xyz // x = 'A'; y = 1; z = 2.0

The tuples introduced above are often referred to as flat tuples, native tuples or unboxed tuples. There is another kind of tuples supported in ATS, which are called boxed tuples. A boxed tuple is essentially a pointer pointing to some heap location where a flat tuple is stored.

Assume that exp1 and exp2 are two expressions of the types T1 and T2, respectively. Then the expression '(exp1, exp2), refers to a tuple of the tuple type '(T1, T2). Accordingly, we can form boxed tuples and boxed tuple types of fewer or more components. What should be noted immediately is that every boxed tuple is of the size of a pointer, and can thus be stored in any place where a pointer can. Using boxed tuples is rather similar to using unboxed ones. For instance, the meaning of the following code should be evident:

val xyz = '( 'A', 1, 2.0 )
val x = xyz.0 and y = xyz.1 and z = xyz.2

Given the availability of flat and boxed tuples, one naturally wants to know whether there is a simple way to determine which kind is preferred over the other. Unfortunately, there is no simple way to do this as far as I can tell. In order to be certain, some kind of profiling is often needed. However, if we want to run code with no support of garbage collection (GC), then we should definitely avoid using boxed tuples.

Records and Record Types

A record is just like a tuple except that each field name of the record is chosen by the programmer (instead of being fixed). Similarly, a record type is just like a tuple type. For instance, a record type point2D is defined as follows:

typedef
point2D = @{ x= double, y= double }

val theOrigin = @{ x= 0.0, y= 0.0 } : point2D

We can use the standard dot notation to extract out a selected component in a record, and this is shown in the next line of code:

val theOrigin_x = theOrigin.x and theOrigin_y = theOrigin.y

val @{ x= theOrigin_x, y= theOrigin_y } = theOrigin

val @{ x= theOrigin_x, ... } = theOrigin // the x-component only 
val @{ y= theOrigin_y, ... } = theOrigin // the y-component only 

Compared with handling native/flat/unboxed records, the only change needed for handling boxed records is to replace the special symbol @{ with another one: '{, which is a quote followed immediately by a left curly brace.

Conditional Expressions

A conditional expression consists of a test and two branches. For instance, the following expression is conditional:

if (x >= 0) then x else ~x

In order to assign a type T to a conditional expression, we need to assign the type bool to the test and the type T to both of the then-branch and the else-branch. For instance, the type int can be assigned to the above conditional expression if the name x is given the type int.

Suppose that we have a conditional expression that is well-typed. When evaluating it, we first evaluate the test to a value, which is guaranteed to be either true or false; if the value is true, then we continue to evaluate the then-branch; otherwise, we continue to evaluate the else-branch.

It is also allowed to form a conditional expression where the else-branch is missing or truncated. For instance, we can form an expression as follows:

if (x >= 0) then print(x)

if (x >= 0) then print(x) else ()

Sequence Expressions

Assume that exp1 and exp2 are expressions of types T1 and T2 respectively, where T1 is void. Then a sequence expression (exp1; exp2) can be formed that is of the type T2. When evaluating the sequence expression (exp1; exp2), we first evaluate exp1 to the void value and then evaluate exp2 to some value, which is also the value of the sequence expression. When more expressions are sequenced, all of them but the last one need to be of the type void and the type of the last expression is also the type of the sequence expression being formed. Evaluating a sequence of more expressions is analogous to evaluating a sequence of two. The following example is a sequence expression:

(print 'H'; print 'e'; print 'l'; print 'l'; print 'o')

begin
  print 'H'; print 'e'; print 'l'; print 'l'; print 'o'
end // end of [begin]

begin
  print 'H'; print 'e'; print 'l'; print 'l'; print 'o';
end // end of [begin]

let
  val () = print 'H'
  val () = print 'e'
  val () = print 'l'
  val () = print 'l'
  val () = print 'o'
in
  // nothing
end // end of [let]

Comments in Code

ATS currently supports four forms of comments: line comment, block comment of ML-style, block comment of C-style, and rest-of-file comment.

• A line comment starts with the double slash symbol (//) and extends until the end of the current line.

• A block comment of ML-style starts and closes with the tokens (* and *), respectively. Note that nested block comments of ML-style are allowed, that is, one block comment of ML-style can occur within another one of the same style.

• A block comment of C-style starts and closes with the tokens /* and */, respectively. Note that block comments of C-style cannot be nested. The use of block comments of C-style is primarily in code that is supposed to be shared by ATS and C. In other cases, block comments of ML-style should be the preferred choice.

• A rest-of-file comment starts with the quadruple slash symbol (////) and extends until the end of the file. Comments of this style of are primarily useful for developing or debugging programs.

Functions as a Simple Form of Abstraction

Given an expression exp of the type double, we can multiply exp by itself to compute its square. If exp is a complex expression, we may introduce a binding between a name and exp so that exp is only evaluated once. This idea is shown in the following example:

let val x = 3.14 * (10.0 - 1.0 / 1.4142) in x * x end

fn square (x: double): double = x * x

If square is a name, what is the expression it refers to? It turns out that the above function definition can also be written as follows:

val square = lam (x: double): double => x * x

val square = lam (y: double): double => y * y

A lambda-expression is a (function) value. Suppose we have a lambda-expression representing a binary function, that is, a function taking two arguments. In order to assign a type of the form (T1, T2) -> T to the lambda-expression, we need to verify that the body of the function can be given the type T if the two arguments of the function are assumed to have the types T1 and T2. What is stated also applies, mutatis mutandis, to lambda-expressions representing functions of fewer or more arguments. For instance, the lambda-expression lam (x: double): double => x * x can be assigned the function type (double) -> double, which may also be written as double -> double.

Assume that exp is an expression of some function type (T1, T2) -> T. Note that exp is not necessarily a name or a lambda-expression. If expressions exp₁ and exp₂ can be assigned the types T1 and T2, then the function application exp(exp₁, exp₂), which may also be referred to as a function call, can be assigned the type T. Typing a function application of fewer or more arguments is handled similarly.

Let us now see an example that builds on the previously defined function square. The boundary of a ring consists of two circles centered at the same point. If the radii of the outer and inner circles are R and r, respectively, then the area of the ring can be computed by the following function area_of_ring:

fn area_of_ring
  (R: double, r: double): double = 3.1416 * (square(R) - square(r))
// end of [area_of_ring]

Function Arity

The arity of a function is the number of arguments the function takes. Functions of arity 0, 1, 2 and 3 are often called nullary, unary, binary and ternary functions, respectively. For example, the following function sqrsum1 is a binary function such that its two arguments are of the type int:

fn sqrsum1 (x: int, y: int): int = x * x + y * y

//
typedef int2 = (int, int)
//
fn sqrsum2
  (xy: int2): int =
  let val x = xy.0 and y = xy.1 in x * x + y * y end
// end of [sqrsum2]

Many functional languages (e.g., Haskell and ML) only allow unary functions. A function of multiple arguments is encoded in these languages as a unary function taking a tuple as its only argument or it is curried into a function that takes these arguments sequentially. ATS, however, provides direct support for functions of multiple arguments. There is even some limited support in ATS for variadic functions, that is, functions of indefinite number of arguments (e.g., the famous printf function in C). This is a topic I will cover elsewhere.

Function Interface

The interface for a function specifies the type assigned to the function. Given a binary function foo of the type (T1, T2) -> T3, its interface can be written as follows:

fun foo (arg1: T1, arg2: T2): T3

fun succ_int (x: int): int // successor
fun pred_int (x: int): int // predecessor

fun add_int_int (x: int, y: int): int // +
fun sub_int_int (x: int, y: int): int // -
fun mul_int_int (x: int, y: int): int // *
fun div_int_int (x: int, y: int): int // /

fun mod_int_int (x: int, y: int): int // modulo
fun gcd_int_int (x: int, y: int): int // greatest common divisor

fun lt_int_int (x: int, y: int): bool // <
fun lte_int_int (x: int, y: int): bool // <=
fun gt_int_int (x: int, y: int): bool // >
fun gte_int_int (x: int, y: int): bool // >=
fun eq_int_int (x: int, y: int): bool // =
fun neq_int_int (x: int, y: int): bool // <>

fun max_int_int (x: int, y: int): int // maximum
fun min_int_int (x: int, y: int): int // minimum

fun print_int (x: int): void
fun tostring_int (x: int): string

Evaluation of Function Calls

Evaluating a function call is straightforward. Assume that we are to evaluate the function call abs(0.0 - 1.0) under some environment ENV0, where the function abs is defined as follows:

fn abs (x: double): double = if x >= 0.0 then x else ~x

Recursive Functions

A recursive function is one that may make calls to itself in its body. In ATS, the keyword fun is used to initiate the definition of a recursive function. Clearly, a non-recursive function is just a special kind of recursive function: the kind that does not make any calls to itself in its body. If one prefers, one can use fun (instead of fn) to initiate the definition of a non-recursive function.

I consider recursion the most enabling feature a programming language can provide. With recursion, we are enabled to do problem-solving based on a strategy of reduction: In order to solve a problem to which a solution is difficult to find immediately, we reduce the problem to problems that are similar but simpler, and we repeat this reduction process if needed until solutions become apparent. Let us now see some concrete examples of problem-solving that make use of this reduction strategy.

Suppose that we want to sum up all the integers ranging from 1 to n, where n is a given integer. This can be readily done by implementing the following recursive function sum1:

fun sum1
  (n: int): int =
  if n >= 1 then sum1 (n-1) + n else 0
// end of [sum1]

We can also solve the problem by implementing the following recursive function sum2 that sums up all the integers in a given range:

fun sum2
  (m: int, n: int): int =
  if m <= n then m + sum2 (m+1, n) else 0
// end of [sum2]

Given integers m and n, there is another strategy for summing up all the integers from m to n: If m does not exceed n, we can find the sum of all the integers from m to (m+n)/2-1 and then the sum of all the integers from (m+n)/2+1 to n and then sum up these two sums and (m+n)/2. The following recursive function sum3 is implemented precisely according to this strategy:

fun sum3
  (m: int, n: int): int =
  if m <= n
    then let
      val mn2 = (m+n)/2
    in
      sum3 (m, mn2-1) + mn2 + sum3 (mn2+1, n)
    end // end of [then]
    else 0 // end of [else]
// end of [sum3]

Evaluation of Recursive Function Calls

Evaluating a call to a recursive function is not much different from evaluating one to a non-recursive function. Let fib be the following defined function for computing the Fibonacci numbers:

fun fib
  (n: int): int =
  if n >= 2 then fib(n-1) + fib(n-2) else n
// end of [fib]

Let us now evaluate fib(3) under ENV0; we extend ENV0 to ENV2 with a binding between n and 3, and start to evaluate the body of fib under ENV2; we then reach the evaluation of fib(n-1) + fib(n-2) under ENV2; evaluating fib(n-1) under ENV2 leads to the evaluation of fib(2) under ENV2, which eventually returns 1; evaluating fib(n-2) under ENV2 leads to the evaluation of fib(1) under ENV2, which eventually returns 1; therefore, evaluating fib(3) under ENV0 returns 2 (as the result of 1+1).

Example: Coin Changes for Fun

Let S be a finite set of positive numbers. The problem we want to solve is to find out the number of distinct ways for a given integer x to be expressed as the sum of multiples of the positive numbers chosen from S. If we interpret each number in S as the denomination of a coin, then the problem asks how many distinct ways there exist for a given value x to be expressed as the sum of a set of coins. If we use cc(S, x) for this number, then we have the following properties on the function cc:

• cc(S, 0) = 1 for any S.

• If x < 0, then cc(S, x) = 0 for any S.

• If S is empty and x > 0, then cc(S, x) = 0.

• If S contains a number c, then cc(S, x) = cc(S₁, x) + cc(S, x-c), where S₁ is the set formed by removing c from S.

//
typedef
int4 = (int, int, int, int)
//
val theCoins = (1, 5, 10, 25): int4
//
fun coin_get
  (n: int): int =
(
  if n = 0 then theCoins.0
  else if n = 1 then theCoins.1
  else if n = 2 then theCoins.2
  else if n = 3 then theCoins.3
  else ~1 (* erroneous value *)
) (* end of [coin_get] *)
//
fun coin_change
  (sum: int): int = let
  fun aux (sum: int, n: int): int =
    if sum > 0 then
     (if n >= 0 then aux (sum, n-1) + aux (sum-coin_get(n), n) else 0)
    else (if sum < 0 then 0 else 1)
  // end of [aux]
in
  aux (sum, 3)
end // end of [coin_change]
//

Note that the entire code in this section plus some additional code for testing is available on-line.

Tail-Call and Tail-Recursion

Suppose that a function foo makes a call in its body to a function bar, where foo and bar may be the same function. If the return value of the call to bar is also the return value of foo, then this call to bar is a tail-call. If foo and bar are the same, then this is a (recursive) self tail-call. For instance, there are two recursive calls in the body of the function f91 defined as follows:

fun f91 (n: int): int =
  if n >= 101 then n - 10 else f91(f91(n+11))

If each recursive call in the body of a function is a tail-call, then this function is a tail-recursive function. For instance, the following function sum_iter is tail-recursive:

fun sum_iter
  (n: int, res: int): int =
  if n > 0 then sum_iter(n-1, n+res) else (res)
// end of [sum_iter]

In ATS, the single most important optimization is probably the one that turns a self tail-call into a local jump. This optimization effectively turns every tail-recursive function into the equivalent of a loop. Although ATS provides direct syntactic support for constructing for-loops and while-loops, the preferred approach to loop construction in ATS is in general through the use of tail-recursive functions. This is the case primarily due to the fact that the syntax for writing tail-recursive functions is compatible with the syntax for other programming features in ATS while the syntax for loops is much less so.

Example: The Eight-Queens Puzzle

The eight-queens puzzle is the problem of positioning on a 8x8 chessboard 8 queen pieces so that none of them can capture any other pieces using the standard chess moves defined for a queen piece. I will present as follows a solution to this puzzle in ATS, reviewing some of the programming features that have been covered so far. In particular, please note that every recursive function implemented in this solution is tail-recursive.

First, let us introduce a name for the integer constant 8 as follows:

#define N 8

typedef int8 =
(
  int, int, int, int, int, int, int, int
) // end of [int8]

In order to print out a board configuration, we define the following functions:

fun print_dots (i: int): void =
  if i > 0 then (print ". "; print_dots (i-1)) else ()
// end of [print_dots]

fun print_row (i: int): void =
(
  print_dots (i); print "Q "; print_dots (N-i-1); print "\n";
) // end of [print_row]

fun print_board (bd: int8): void =
(
  print_row (bd.0); print_row (bd.1); print_row (bd.2); print_row (bd.3);
  print_row (bd.4); print_row (bd.5); print_row (bd.6); print_row (bd.7);
  print_newline ()
) // end of [print_board]

As an example, if print_board is called on the board configuration represented by @(0, 1, 2, 3, 4, 5, 6, 7), then the following 8 lines are printed out:

Q . . . . . . . 
. Q . . . . . . 
. . Q . . . . . 
. . . Q . . . . 
. . . . Q . . . 
. . . . . Q . . 
. . . . . . Q . 
. . . . . . . Q 

Given a board and the row number of a queen piece on the board, the following function board_get returns the column number of the piece:

fun board_get
  (bd: int8, i: int): int =
  if i = 0 then bd.0
  else if i = 1 then bd.1
  else if i = 2 then bd.2
  else if i = 3 then bd.3
  else if i = 4 then bd.4
  else if i = 5 then bd.5
  else if i = 6 then bd.6
  else if i = 7 then bd.7
  else ~1 // end of [if]
// end of [board_get]

Given a board, a row number i and a column number j, the following function board_set returns a new board that are the same as the original board except for j being the column number of the queen piece on row i:

fun board_set
  (bd: int8, i: int, j:int): int8 = let
  val (x0, x1, x2, x3, x4, x5, x6, x7) = bd
in
  if i = 0 then let
    val x0 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else if i = 1 then let
    val x1 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else if i = 2 then let
    val x2 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else if i = 3 then let
    val x3 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else if i = 4 then let
    val x4 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else if i = 5 then let
    val x5 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else if i = 6 then let
    val x6 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else if i = 7 then let
    val x7 = j in (x0, x1, x2, x3, x4, x5, x6, x7)
  end else bd // end of [if]
end // end of [board_set]

Let us now implement two testing functions safety_test1 and safety_test2 as follows:

fun safety_test1
(
  i0: int, j0: int, i1: int, j1: int
) : bool =
(*
** [abs]: the absolute value function
*)
  j0 != j1 andalso abs (i0 - i1) != abs (j0 - j1)
// end of [safety_test1]

fun safety_test2
(
  i0: int, j0: int, bd: int8, i: int
) : bool =
  if i >= 0 then
    if safety_test1 (i0, j0, i, board_get (bd, i))
      then safety_test2 (i0, j0, bd, i-1) else false
    // end of [if]
  else true // end of [if]
// end of [safety_test2]

• The function safety_test1 tests whether a queen piece on row i0 and column j0 can capture another one on row i and column j.

• The function safety_test2 tests whether a queen piece on row i0 and column j0 can capture any other pieces on a given board with a row number less than or equal to i.

We are now ready to implement the following function search based on a standard depth-first search (DFS) algorithm:

fun search
(
  bd: int8, i: int, j: int, nsol: int
) : int = (
//
if
(j < N)
then let
  val test = safety_test2 (i, j, bd, i-1)
in
  if test
    then let
      val bd1 = board_set (bd, i, j)
    in
      if i+1 = N
        then let
          val () = print! ("Solution #", nsol+1, ":\n\n")
          val () = print_board (bd1)
        in
          search (bd, i, j+1, nsol+1)
        end // end of [then]
        else (
          search (bd1, i+1, 0(*j*), nsol) // positioning next piece
        ) (* end of [else] *)
      // end of [if]
    end // end of [then]
    else search (bd, i, j+1, nsol)
  // end of [if]
end // end of [then]
else (
  if i > 0
    then search (bd, i-1, board_get (bd, i-1) + 1, nsol) else nsol
  // end of [if]
) (* end of [else] *)
//
) (* end of [search] *)

Q . . . . . . . 
. . . . Q . . . 
. . . . . . . Q 
. . . . . Q . . 
. . Q . . . . . 
. . . . . . Q . 
. Q . . . . . . 
. . . Q . . . . 

Note that the entire code in this section plus some additional code for testing is available on-line.

Mutually Recursive Functions

A collection of functions are defined mutually recursively if each function can make calls in its body to any functions in this collection. Mutually recursive functions are commonly encountered in practice.

As an example, let P be a function on natural numbers defined as follows:

• P(0) = 1

• P(n+1) = 1 + the sum of the products of i and P(i) for i ranging from 1 to n

• P(0) = 1

• P(n+1) = 1 + Q(n)

• Q(0) = 0

• Q(n+1) = Q(n) + (n+1) * P(n+1)

fun P (n:int): int = if n > 0 then 1 + Q(n-1) else 1
and Q (n:int): int = if n > 0 then Q(n-1) + n * P(n) else 0

Mutually Defined Tail-Recursion

Suppose that foo and bar are two mutually defined recursive functions. In the body of foo or bar, a tail-call to foo or bar is a mutually recursive tail-call. For instance, the following two functions isevn and isodd are mutually recursive:

//
fun
isevn (n: int): bool = if n > 0 then isodd (n-1) else true
//
and
isodd (n: int): bool = if n > 0 then isevn (n-1) else false
//

//
fnx
isevn (n: int): bool = if n > 0 then isodd (n-1) else true
//
and
isodd (n: int): bool = if n > 0 then isevn (n-1) else false
//

When writing code corresponding to embedded loops in an imperative programming language such as C or Java, we often need to make sure that mutually recursive tail-calls are compiled into local jumps. The following function print_multable is implemented to print out a standard multiplication table for nonzero digits:

fun
print_multable
  ((*void*)) = let
//
#define N 9
//
fnx
loop1
  (i: int): void =
  if i <= N then loop2 (i, 1) else ()
//
and
loop2
  (i: int, j: int): void =
  if j <= i
    then let
      val () = if j >= 2 then print " "
      val () = $extfcall(void, "printf", "%dx%d=%2.2d", j, i, j*i)
    in
      loop2 (i, j+1) 
    end // end of [then]
    else let
      val () = print_newline () in loop1 (i+1)
    end // end of [else]
  // end of [if]
//
in
  loop1 (1)
end // end of [print_multable]

When called, the function print_multable prints out the following multiplication table:

1x1=01
1x2=02 2x2=04
1x3=03 2x3=06 3x3=09
1x4=04 2x4=08 3x4=12 4x4=16
1x5=05 2x5=10 3x5=15 4x5=20 5x5=25
1x6=06 2x6=12 3x6=18 4x6=24 5x6=30 6x6=36
1x7=07 2x7=14 3x7=21 4x7=28 5x7=35 6x7=42 7x7=49
1x8=08 2x8=16 3x8=24 4x8=32 5x8=40 6x8=48 7x8=56 8x8=64
1x9=09 2x9=18 3x9=27 4x9=36 5x9=45 6x9=54 7x9=63 8x9=72 9x9=81

In summary, the very ability to turn mutually recursive tail-calls into local jumps makes it possible to implement embedded loops as mutually tail-recursive functions. This ability is indispensable for advocating the practice of replacing loops with recursive functions in ATS.

Envless Functions and Closure-Functions

I use envless as a shorthand for environmentless, which is not a legal word but I suppose that you have no problem figuring out what it means.

An envless function is represented by a pointer pointing to some place in a code segment where the object code for executing a call to this function is located. Every function in the programming language C is envless. A closure-function is also represented by a pointer, but the pointer points to some place in a heap where a tuple is allocated (at run-time). Usually, the first component of this tuple is a pointer representing an envless function and the rest of the components represent some bindings. A tuple as such is often referred to as a closure-function or simply closure, which can be thought of as an envless function paired with an environment. It is possible that the environment of a closure-function is empty, but this does not equate a closure-function with an envless function. Every function in functional languages such as ML and Haskell is a closure-function.

In the following example, the function sum, which is assigned the type (int) -> int, sums up all the integers between 1 and a given natural number:

fun sum
  (n: int): int = let
  fun loop
  (
    i: int, res: int
  ) :<cloref1> int =
    if i <= n then loop (i+1, res+i) else res
  // end of [loop]
in
  loop (1(*i*), 0(*res*))
end // end of [sum]

If the syntax :<cloref1> is replaced with the colon symbol : alone, the code can still pass typechecking but its compilation may eventually lead to a warning or even an error indicating that loop cannot be compiled into a toplevel function in C. The reason for this warning/error is due to the body of loop containing a variable n that is neither at toplevel nor a part of the arguments of loop itself. It is straightforward to make loop an envless function by including n as an argument in addition to the original ones:

fun sum
  (n: int): int = let
  fun loop
  (
    n:int, i: int, res: int
  ) : int =
    if i <= n then loop (n, i+1, res+i) else res
  // end of [loop]
in
  loop (n, 1(*i*), 0(*res*))
end // end of [sum]

The need for creating closures often appears when a function is not directly applied. For instance, the return value of a function call may also be a function. In the following code, the defined function addx returns another function when applied to a given integer x, and the returned function is a closure-function, which always adds the integer x to its own argument:

//
fun addx (x: int): int -<cloref1> int = lam y => x + y
//
val plus1 = addx (1) // [plus1] is of the type int -<cloref1> int
val plus2 = addx (2) // [plus2] is of the type int -<cloref1> int
//

Closures are often passed as arguments to functions that are referred to as higher-order functions. It is also fairly common for closures to be embedded in data structures.

Higher-Order Functions

A higher-order function is a function that take another function as its argument. For instance, the following defined function rtfind is a higher-order one:

fun rtfind
  (f: int -> int): int = let
  fun loop (
    f: int -> int, n: int
  ) : int =
    if f(n) = 0 then n else loop (f, n+1)
  // end of [loop]
in
  loop (f, 0)
end // end of [rtfind]

Higher-order functions can greatly facilitate code reuse, and I now present a simple example to illustrate this point. The following defined functions sum and prod compute the sum and product of the integers ranging from 1 to a given natural number, respectively:

fun sum (n: int): int = if n > 0 then sum (n-1) + n else 0
fun prod (n: int): int = if n > 0 then prod (n-1) * n else 1

//
fun ifold
  (n: int, f: (int, int) -> int, ini: int): int =
  if n > 0 then f (ifold (n-1, f, ini), n) else ini
//
fun sum (n: int): int = ifold (n, lam (res, x) => res + x, 0)
fun prod (n: int): int = ifold (n, lam (res, x) => res * x, 1)
//

fun sqrsum (n: int): int = ifold (n, lam (res, x) => res + x * x, 0)

fun sqrmodsum
  (n: int, d: int): int =
  ifold (n, lam (res, x) => if x mod d = 0 then res + x * x else res, 0)
// end of [sqrmodsum]

//
fun
ifold2
(
  n: int, f: (int, int) -<cloref1> int, ini: int
) : int =
  if n > 0 then f (ifold2 (n-1, f, ini), n) else ini
// end of [ifold2]
//
fun
sqrmodsum (n: int, d: int): int =
  ifold2 (n, lam (res, x) => if x mod d then res + x * x else res, 0)
// end of [sqrmodsum]
//

As more features of ATS are introduced, higher-order functions will become even more effective in facilitating code reuse.

Example: Binary Search for Fun

While binary search is often performed on an ordered array to check whether a given element is stored in that array, it can also be employed to compute the inverse of an increasing or decreasing function on integers. In the following code, the defined function bsearch_fun returns an integer i0 such that f(i) <= x0 holds for i ranging from lb to i0, inclusive, and x0 < f(i) holds for i ranging from i0+1 to ub, inclusive:

//
// The type [uint] is for unsigned integers
//
fun bsearch_fun
(
  f: int -<cloref1> uint
, x0: uint, lb: int, ub: int
) : int =
  if lb <= ub then let
    val mid = lb + (ub - lb) / 2
  in
    if x0 < f (mid) then
      bsearch_fun (f, x0, lb, mid-1)
    else
      bsearch_fun (f, x0, mid+1, ub)
    // end of [if]
  end else ub // end of [if]
// end of [bsearch_fun]

//
// Assuming that [uint] is of 32 bits
//
val
ISQRT_MAX = (1 << 16) - 1 // = 65535
//
fun isqrt
  (x: uint): int =
  bsearch_fun (lam i => square(g0i2u(i)), x, 0, ISQRT_MAX)
// end of [isqrt]

Please find on-line the entire code in this section plus some additional code for testing.

Example: A Higher-Order Fun Puzzle

Let us first introduce a type definition as follows:

typedef I(a:t@ype) = (a) -<cloref1> a

fn{a:t0p}
twice (f: I(a)):<cloref> I(a) = lam (x) => f (f (x))

//
typedef I0 = int
typedef I1 = I(I0)
typedef I2 = I(I1)
typedef I3 = I(I2)
//
val Z = 0
val S = lam (x: int): int =<cloref> x + 1
val ans0 = twice<I0>(S)(Z)
val ans1 = twice<I1>(twice<I0>)(S)(Z)
val ans2 = twice<I2>(twice<I1>)(twice<I0>)(S)(Z)
val ans3 = twice<I3>(twice<I2>)(twice<I1>)(twice<I0>)(S)(Z)
//

Obviously, Z stands for the integer 0 and S for the successor function on integers. Also, ans0 equals 2 as it is the result of applying S to Z twice. Let S2 be the function that applies S twice. It is clear that ans1 is the result of applying S2 to Z twice and thus equals 4. With a bit more effort, one should be able to figure out that the value of ans2 is 16. What is the value of ans3? In general, what is the nth value in the sequence of ans0, ans1, ans2, etc.? I leave these questions as exercises for the interested reader.

Please find on-line the entire code in this section plus some additional code for testing.

Currying and Uncurrying

Currying, which is named after the logician Haskell Curry, means to turn a function taking multiple arguments simultaneously into a function of the same body (modulo corresponding recursive function calls being changed accordingly) that takes these arguments sequentially. Uncurrying means precisely the opposite of currying. In the following code, both of the defined functions acker1 and acker2 implement the Ackermann's function (which is famous for being recursive but not primitive recursive):

fun acker1
  (m: int, n: int): int =
(
  if m > 0 then
    if n > 0 then acker1 (m-1, acker1 (m, n-1)) else acker1 (m-1, 1)
  else n+1 // end of [if]
)

fun acker2
  (m: int) (n: int): int =
(
  if m > 0 then
    if n > 0 then acker2 (m-1) (acker2 m (n-1)) else acker2 (m-1) 1
  else n+1 // end of [if]
)

In functional languages such as ML and Haskell, a function of multiple arguments needs to be either curried or translated into a corresponding unary function of a single argument that itself is a tuple. In such languages, currying often leads to better performance at run-time and thus is preferred. In ATS, functions of multiple arguments are supported directly. Also, given a function of multiple arguments, a curried version of the function is likely to perform less efficiently at run-time than the function itself (due to the treatment of curried functions by the ATS compiler atsopt). Therefore, the need for currying in ATS is greatly diminished. Unless convincing reasons can be given, currying is in general not a recommended programming style in ATS.

Please find on-line the entire code in this section plus some additional code for testing.

Patterns

Patterns in ATS can be defined inductively as follows:

• Certain constant values such as integers, booleans, chars, floating point numbers, and strings are patterns.

• The void-value () is a pattern.

• The underscore symbol _ represents a special wildcard pattern.

• Variables are patterns.

• A tuple of patterns, either boxed or unboxed, is a pattern.

• A record of patterns, either boxed or unboxed, is a pattern.

• Given a constructor C, a pattern can be formed by applying C to a given list of patterns.

• Given a variable x and a pattern pat, (x as pat) is a reference-pattern, where as is a keyword.

• Some other forms of patterns will be introduced elsewhere.

Pattern-Matching

Pattern matching means matching values against patterns. In the case where a value matches a pattern, a collection of bindings are generated between the variables in the pattern and certain components in the value. Pattern-matching is performed according to the following set of rules:

• A value that matches a constant pattern must be the same constant, and this matching generates no bindings.

• The void-value () only matches the void-pattern (), and this matching generates no bindings.

• Any value can match the wildcard pattern, and this matching generates no bindings.

• Any value can match a variable pattern, and this matching generates a binding between the variable and the value.

• A tuple-value matches a tuple-pattern if they are of the same length and each value component in the former matches the corresponding pattern component in the latter, and this matching generates a collection of bindings that is the union of the bindings generated from matching the value components in the tuple-value against the pattern components in the tuple-pattern.

• A record-value matches a record-pattern if they have the same field names and each value component in the former matches the corresponding pattern component in the latter, and this matching generates a collection of bindings that is the union of the bindings generated from matching the value components in the record-value against the pattern components in the record-pattern.

• Given a pattern formed by applying a constructor C to some pattern arguments, a value matches this pattern if the value is formed by applying C to some value arguments matching the pattern arguments, and this matching generates a collection of bindings that is the union of the bindings generated from matching the value arguments against the pattern arguments.

• Given a referenced pattern (x as pat), a value matches the pattern if it matches pat, and this matching generates a collection of bindings that extends the bindings generated from matching the value against pat with a binding from x to the value.

Matching Clauses and Case-Expressions

Given a pattern pat and an expression exp, (pat => exp) is a matching clause. The pattern pat and the expression exp are referred to as the guard and the body of the matching clause.

Given an expression exp0 and a sequence of matching clauses clseq, a case-expression can be formed as such: (case exp0 of clseq). To evaluate the case-expression under a given environment ENV0, we first evaluate exp0 under ENV0 to a value. If this value does not match the guard of any clause in clseq, then the evaluation of the case-expression aborts. Otherwise, we choose the first clause in clseq such that the value matches the guard of the clause. Let ENV1 be the environment that extends ENV0 with the bindings generated from this matching, and we evaluate the body of the chosen clause under ENV1. The value obtained from this evaluation is the value of the case-expression being evaluated.

Enumerative Datatypes

The simplest form of datatypes is for enumerating a finite number of constants. For instance, the following concrete syntax introduces a datatype of the name wday:

datatype wday =
  | Monday of ()
  | Tuesday of ()
  | Wednesday of ()
  | Thursday of ()
  | Friday of ()
  | Saturday of ()
  | Sunday of ()
// end of [wday]

The following code implements a function that tests whether a given value of the type wday is a weekday or not:

fun isWeekday
  (x: wday): bool = case x of
  | Monday() => true // the first bar (|) is optional
  | Tuesday() => true
  | Wednesday() => true
  | Thursday() => true
  | Friday() => true
  | Saturday() => false
  | Sunday() => false
// end of [isWeekday]

fun isWeekday
  (x: wday): bool = case x of
  | Saturday() => false | Sunday() => false | _ => true
// end of [isWeekday]

Recursively Defined Datatypes

A recursively defined datatype (or recursive datatype for short) is one such that its associated constructors may form values by applying to values of the datatype itself. For instance, the following declared datatype charlst is recursive:

datatype charlst =
  | charlst_nil of ()
  | charlst_cons of (char, charlst)
// end of [charlst]

charlst_cons('a', charlst_cons('b', charlst_cons('c', charlst_nil())))

fun
charlst_length
(
  cs: charlst
) : int =
  case cs of
  | charlst_nil() => 0
  | charlst_cons(_, cs) => 1 + charlst_length(cs)
// end of [charlst_length]

fun
charlst_length
  (cs: charlst): int = let
//
fun loop
  (cs: charlst, n: int): int = case cs of
  | charlst_nil() => n | charlst_cons (_, cs) => loop(cs, n+1)
// end of [loop]
//
in
  loop (cs, 0)
end // end of [charlst_length]

Exhaustiveness of Pattern-Matching

Given a type T and a set of patterns, if for any given value of the type T there is always at least one pattern in the set such that the value matches the pattern, then pattern-matching values of the type T against the set of patterns is exhaustive. Given a case-expression of the form (case exp0 of clseq), where exp0 is assumed to be of some type T, if pattern-matching values of the type T against the guards of the matching clauses in clseq is exhaustive, then the case-expression is said to be pattern-matching-exhaustive.

The following code implements a function that finds the last character in a non-empty character list:

fun
charlst_last
  (cs: charlst): char =
(
  case cs of
  | charlst_cons (c, charlst_nil ()) => c
  | charlst_cons (_, cs1) => charlst_last (cs1)
)
// end of [charlst_last]

The function charlst_last can also be implemented as follows:

fun
charlst_last
  (cs: charlst): char =
(
  case cs of
  | charlst_cons (c, cs1) =>
    (
      case+ cs1 of
      | charlst_nil () => c | charlst_cons _ => charlst_last (cs1)
    ) // end of [charlst_cons]
) // end of [charlst_last]

Suppose we have a case-expression containing only one matching clause, that is, the case-expression is of the form [case exp0 of pat => exp]. Then we can also write this case-expression as a let-expression: (let val pat = exp0 in exp end). For instance, we give another implementation of the function charlst_last as follows:

fun
charlst_last
  (cs: charlst): char = let
  val charlst_cons (c, cs1) = cs in case+ cs1 of
  | charlst_nil () => c | charlst_cons _ => charlst_last (cs1)
end // end of [charlst_last]

As values formed by the constructors charlst_nil and charlst_cons are assigned the same type charlst, it is impossible to rely on typechecking to prevent the function charlst_last from being applied to an empty character list. This is a serious limitation. With dependent types, which allow data to be described much more precisely, we can ensure at the level of types that a function finding the last element of a list can only be applied to a non-empty list.

Example: Binary Search Tree

A binary search tree is a binary tree satisfying the following property: for each node in the tree, the key stored in the node is greater than or equal to every key stored in the left child of the node and less than or equal to every key stored in the right child of the node. In other words, a binary tree is a binary search tree if a pre-order traversal encounters a sequence of keys ordered ascendingly (according to some ordering on keys). In practice, binary search trees are commonly employed to represent sets and maps.

The following declaration introduces a datatype bstree for binary search trees in which the stored keys are strings:

datatype bstree =
  | E of () | B of (bstree, string, bstree)
// end of [bstree]

It should be noted that not every value of the type bstree represents a valid binary search tree as it is certainly possible to construct a value representing a binary tree but not a binary search tree.

The following function [bstree_inord] does a in-order traversal of a given binary tree:

fun
bstree_inord
(
  t0: bstree, fwork: string -<cloref1> void
) : void =
(
case+ t0 of
| E () => ()
| B (t1, k, t2) =>
  {
    val () = bstree_inord (t1, fwork)
    val () = fwork (k)
    val () = bstree_inord (t2, fwork)
  }
) (* end of [bstree_inord] *)

If [t0] is a binary search tree, then the sequence of keys processed by [fwork] are ordered ascendingly.

Given a binary search tree and a key, the following function [bstree_search] checks whether the key is stored inside the tree:

fun
bstree_search
(
  t0: bstree, k0: string
) : bool =
(
//
case+ t0 of
| E () => false
| B (t1, k, t2) => let
    val sgn = compare (k0, k)
  in
    case+ 0 of
    | _ when sgn < 0 => bstree_search (t1, k0)
    | _ when sgn > 0 => bstree_search (t2, k0)
    | _ (*k0 = k*) => true
  end // end of [B]
//
) (* end of [bstree_search] *)

Note that [bstree_search] returns true if the given key is found. Otherwise, it returns false.

Given a binary search tree and a key, the following function [bstree_insert] inserts the key into the tree:

fun
bstree_insert
(
  t0: bstree, k0: string
) : bstree =
(
//
case+ t0 of
| E () => B (E, k0, E)
| B (t1, k, t2) => let
    val sgn = compare (k0, k)
  in
    case+ 0 of
    | _ when sgn < 0 => B (bstree_insert (t1, k0), k, t2)
    | _ when sgn > 0 => B (t1, k, bstree_insert (t2, k0))
    | _ (*k0 = k*) => t0 // [k0] found and no actual insertion
  end // end of [B]
//
) (* end of [bstree_insert] *)

Note that [bstree_insert] inserts the key only if it is not already stored inside the given tree. Also, if inserted, the key is always stored in a newly created leaf node.

Please find on-line the entirety of the code in this section plus some additional code for testing.

Example: Evaluating Integer Expressions

For representing integer expressions, we declare a datatype IEXP as follows:

datatype IEXP =
  | IEXPcst of int // constants
  | IEXPneg of (IEXP) // negative
  | IEXPadd of (IEXP, IEXP) // addition
  | IEXPsub of (IEXP, IEXP) // subtraction
  | IEXPmul of (IEXP, IEXP) // multiplication
  | IEXPdiv of (IEXP, IEXP) // division
// end of [IEXP]

IEXPadd(IEXPneg(IEXPcst(1)), IEXPmul(IEXPsub(IEXPcst(2), IEXPcst(3)), IEXPcst(4)))

fun
eval_iexp
  (e0: IEXP): int =
(
case+ e0 of
| IEXPcst (n) => n
| IEXPneg (e) => ~eval_iexp (e)
| IEXPadd (e1, e2) => eval_iexp (e1) + eval_iexp (e2)
| IEXPsub (e1, e2) => eval_iexp (e1) - eval_iexp (e2)
| IEXPmul (e1, e2) => eval_iexp (e1) * eval_iexp (e2)
| IEXPdiv (e1, e2) => eval_iexp (e1) / eval_iexp (e2)
) (* end of [eval_iexp] *)

Suppose we also allow the construct if-then-else to be use in forming integer expressions. For instance, we may write an integer expression like (if 1+2 <= 3*4 then 5+6 else 7-8). Note that the test (1+2 <= 3*4) is a boolean expression rather than an integer expression. This indicates that we also need to declare a datatype BEXP for representing boolean expressions. Furthermore, IEXP and BEXP should be defined mutually recursively as follows:

datatype IEXP =
  | IEXPcst of int // integer constants
  | IEXPneg of (IEXP) // negative
  | IEXPadd of (IEXP, IEXP) // addition
  | IEXPsub of (IEXP, IEXP) // subtraction
  | IEXPmul of (IEXP, IEXP) // multiplication
  | IEXPdiv of (IEXP, IEXP) // division
  | IEXPif of (BEXP(*test*), IEXP(*then*), IEXP(*else*))
// end of [IEXP]

and BEXP = // [and] for combining datatype declarations
  | BEXPcst of bool // boolean constants
  | BEXPneg of BEXP // negation
  | BEXPconj of (BEXP, BEXP) // conjunction
  | BEXPdisj of (BEXP, BEXP) // disjunction
  | BEXPeq of (IEXP, IEXP) // equal-to
  | BEXPneq of (IEXP, IEXP) // not-equal-to
  | BEXPlt of (IEXP, IEXP) // less-than
  | BEXPlte of (IEXP, IEXP) // less-than-equal-to
  | BEXPgt of (IEXP, IEXP) // greater-than
  | BEXPgte of (IEXP, IEXP) // greater-than-equal-to
// end of [BEXP]

fun
eval_iexp
(
  e0: IEXP
) : int = (
//
case+ e0 of
| IEXPcst n => n
| IEXPneg (e) => ~eval_iexp (e)
| IEXPadd (e1, e2) => eval_iexp (e1) + eval_iexp (e2)
| IEXPsub (e1, e2) => eval_iexp (e1) - eval_iexp (e2)
| IEXPmul (e1, e2) => eval_iexp (e1) * eval_iexp (e2)
| IEXPdiv (e1, e2) => eval_iexp (e1) / eval_iexp (e1)
| IEXPif
  (
    e_test, e_then, e_else
  ) =>
  (
    eval_iexp (if eval_bexp (e_test) then e_then else e_else)
  ) // end of [IEXPif]
//
) (* end of [eval_iexp] *)

and
eval_bexp
(
  e0: BEXP
) : bool = (
//
case+ e0 of
| BEXPcst b => b
| BEXPneg (e) => ~eval_bexp (e)
| BEXPconj (e1, e2) =>
    if eval_bexp (e1) then eval_bexp (e2) else false
| BEXPdisj (e1, e2) =>
    if eval_bexp (e1) then true else eval_bexp (e2)
| BEXPeq (e1, e2) => eval_iexp (e1) = eval_iexp (e2)
| BEXPneq (e1, e2) => eval_iexp (e1) != eval_iexp (e2)
| BEXPlt (e1, e2) => eval_iexp (e1) < eval_iexp (e2)
| BEXPlte (e1, e2) => eval_iexp (e1) <= eval_iexp (e2)
| BEXPgt (e1, e2) => eval_iexp (e1) > eval_iexp (e2)
| BEXPgte (e1, e2) => eval_iexp (e1) >= eval_iexp (e2)
//
) (* end of [eval_bexp] *)

The integer and boolean expressions used in this example are all constant expressions containing no variables. Therefore, there is no need for an environment to evaluate them. I will present a more advanced example elsewhere to demonstrate how an evaluator for a simple call-by-value functional programming language like the core of ATS can be implemented.

Please find on-line the entirety of the code in this section plus some additional code for testing.

Function Templates

A function template is a code template that implements a function. In the following code, two functions are defined to swap values:

//
typedef charint = (char, int)
typedef intchar = (int, char)
//
fun swap_char_int (xy: charint): intchar = (xy.1, xy.0)
fun swap_int_char (xy: intchar): charint = (xy.1, xy.0)
//

//
fun{
a,b:t@ype
} swap (xy: (a, b)): (b, a) = (xy.1, xy.0)
//
fun swap_char_int (xy: charint): intchar = swap<char,int> (xy)
fun swap_int_char (xy: intchar): charint = swap<int,char> (xy)
//

A different style of implementation of swap is given as follows:

fun{a:t@ype}{b:t@ype} swap2 (xy: (a, b)): (b, a) = (xy.1, xy.0)

fun swap_char_int (xy: charint): intchar = swap2<char><int> (xy)
fun swap_int_char (xy: intchar): charint = swap2<int><char> (xy)

As another example, a higher-order function template for composing (closure) functions is given as follows:

//
typedef
cfun (t1:t@ype, t2:t@ype) = t1 -<cloref1> t2
//
fun{
a,b,c:t@ype
} compose (
  f: cfun (a, b), g: cfun (b, c)
) :<cloref1> cfun (a, c) = lam x => g(f(x))
//
val inc_by_1 = lam (x:int): int =<cloref> x+1
val mul_by_2 = lam (x:int): int =<cloref> x*2
//
val f_2x_1 = compose<int,int,int> (mul_by_2, inc_by_1)
val f_2x_2 = compose<int,int,int> (inc_by_1, mul_by_2)
//

In ATS, function templates are typechecked but not compiled to code in C. Instead, they are compiled to an intermediate form. Only instances of function templates are compiled to code in C. Suppose we have a function template foo taking one type parameter and two instances foo<T1> and foo<T2> are used in a program for some types T1 and T2. In general, one function in C is generated for each instance of foo when the program is compiled. However, if T1 and T2 have the same name, then the two instances may share one function in C.

Please note that I may simply use the name function to refer to a function template from now on if no confusion is expected.

Polymorphic Functions

A polymorphic function is rather similar to a function template. However, the former is a first-class value in ATS while the latter is not. As an example, the following defined function swap_boxed is polymorphic:

fun swap_boxed{a,b:type} (xy: (a, b)): (b, a) = (xy.1, xy.0)

val AB = (box("A"), box("B"))
val BA1 = swap_boxed{boxstr,boxstr} (AB)
val BA2 = swap_boxed (AB) // omitting type arguments may be fine

When calling a polymorphic function, we often omit passing static arguments explicitly and expect them to be synthesized by the compiler. However, there are also occasions, which are not uncommon, where static arguments need to be supplied explicitly as either they cannot be successfully synthesized or what is synthesized is not exactly what is expected by the programmer.

It is also possible to pass static arguments sequentially as is shown in the following style of implementation of a polymorphic function:

//
fun swap2_boxed{a:type}{b:type} (xy: (a, b)): (b, a) = (xy.1, xy.0)
//
val AB = (box("A"), box("B"))
val BA1 = swap2_boxed (AB) // both static arguments to be synthesized
val BA2 = swap2_boxed{...} (AB) // both static arguments to be synthesized
val BA3 = swap2_boxed{..}{boxstr} (AB) // 1st static argument to be synthesized
val BA4 = swap2_boxed{boxstr}{..} (AB) // 2nd static argument to be synthesized
val BA5 = swap2_boxed{..}{..} (AB) // both static arguments to be synthesized
val BA6 = swap2_boxed{boxstr}{boxstr} (AB) // both static arguments are provided
//

I have seen two kinds of errors involving polymorphic functions that are extremely common in practice.

• The first kind is depicted in the following example:

  fun swap_boxed{a,b:t@ype} (xy: (a, b)): (b, a) = (xy.1, xy.0)
  

  Notice that the sort for type variables a and b is t@ype (instead of type). While this example can pass typechecking, its compilation results in a compile-time error that may seem mysterious to many programmers. The simple reason for this error is that the compiler cannot figure out the size of a and b when trying to generate code in C as the sort t@ype is for types of unspecified size.

• The second kind is depicted in the following example:

  fun{a,b:type} swap_boxed (xy: (a, b)): (b, a) = (xy.1, xy.0)
  

  Strictly speaking, there is really no error in this case. If defined as such, swap_boxed is a function template instead of a polymorphic function. However, such a function template is severely restricted as it cannot be instantiated with types that are not boxed. While this could be intended, it is very unlikely.

Polymorphic Datatypes

Code sharing also applies to datatype declarations. For instance, a commonly used polymorphic datatype list0 is declared as follows:

datatype
list0 (a:t@ype) =
  | list0_nil (a) of () | list0_cons (a) of (a, list0 a)
// end of [list0]

fun{a:t@ype}
list0_length
  (xs: list0 a): int =
(
  case+ xs of
  | list0_cons (_, xs) => 1 + list0_length<a> (xs) | list0_nil () => 0
) (* end of [list0_length] *)

Another commonly used polymorphic datatype option0 is declared as follows:

datatype
option0 (a:t@ype) =
  | option0_none (a) of () | option0_some (a) of a
// end of [option0]

fun divopt
(
  x: int, y: int
) : option0 (int) =
  if y != 0 then option0_some{int}(x/y) else option0_none((*void*))
// end of [divopt]

fun{
a:t@ype
} list0_last
(
  xs: list0 a
) : option0 (a) = let
//
fun loop
  (x: a, xs: list0 a): a =
(
  case+ xs of
  | list0_nil () => x | list0_cons (x, xs) => loop (x, xs)
) (* end of [loop] *)
//
in
  case+ xs of
  | list0_nil () => option0_none((*void*))
  | list0_cons (x, xs) => option0_some{a}(loop (x, xs))
end // end of [list0_last]

Example: Function Templates on Lists

In functional programming, lists are ubiquitous. We implement as follows some commonly used function templates on lists. It should be noted that these templates are all available in some library of ATS, where they may be implemented in a significantly more efficient manner due to the use of certain programming features (such as linear datatypes) that have not been covered so far.

Please find the entire code in this section plus some additional code for testing on-line.

fun
{a:t@ype}
list0_append
(
xs: list0 a, ys: list0 a
) : list0 a =
(
case+ xs of
| list0_nil() => ys
| list0_cons(x, xs) =>
    list0_cons{a}(x, list0_append<a>(xs, ys))
  // end of [list0_cons]
) (* end of [list0_append] *)

fun
{a:t@ype}
list0_reverse_append
(
xs: list0 a, ys: list0 a
) : list0 a =
(
case+ xs of
| list0_nil() => ys
| list0_cons(x, xs) =>
    list0_reverse_append<a> (xs, list0_cons{a}(x, ys))
  // end of [list0_cons]
) (* end of [list0_reverse_append] *)

fun
{a:t@ype}
list0_reverse
  (xs: list0 a): list0 a = list0_reverse_append<a>(xs, list0_nil)
// end of [list0_reverse]

fun
{a:t@ype}
{b:t@ype}
list0_map
(
  xs: list0 a, f0: a -<cloref1> b
) : list0 b =
(
case+ xs of
| list0_nil() =>
  list0_nil()
| list0_cons(x, xs) =>
  list0_cons{b}(f0(x), list0_map<a><b>(xs, f0))
) (* end of [list0_map] *)

fun
{a:t@ype}
{b:t@ype}
list0_foldleft
(
  ini: a
, xs0: list0(b), f0: (a, b) -<cloref> a
) : a =
(
//
case+ xs0 of
| list0_nil() => ini
| list0_cons(x, xs) =>
  list0_foldleft<a><b> (f0(ini, x), xs, f0)
//
) (* end of [list0_foldleft] *)

fun
{a:t@ype}
{b:t@ype}
list0_foldright
(
  xs0: list0(a)
, res: b, f0: (a, b) -<cloref1> b
) : b =
(
//
case+ xs0 of
| list0_nil() => res
| list0_cons(x, xs) =>
  f0(x, list0_foldright<a><b>(xs, res, f0))
//
)

fun{
a,b:t@ype
} list0_zip
(
xs: list0(a)
,
ys: list0(b)
) : list0@(a, b) = let
//
  typedef ab = @( a, b )
//
in
//
case+ (xs, ys) of
| (list0_cons(x, xs),
   list0_cons(y, ys)
  ) =>
  (
    list0_cons{ab}((x, y), list0_zip<a,b>(xs, ys))
  ) (* (cons,cons) *)
| (_, _) => list0_nil((*void*))
//
end // end of [list0_zip]

fun
{a,
 b:t@ype}
{c:t@ype}
list0_zipwith
(
  xs: list0(a)
, ys: list0(b)
, f0: (a, b) -<cloref1> c
) : list0(c) =
(
case+ (xs, ys) of
| (list0_cons(x, xs),
   list0_cons(y, ys)) =>
  (
    list0_cons{c}(f0(x, y), list0_zipwith<a,b><c> (xs, ys, f0))
  )
| (_, _) => list0_nil((*void*))
) (* end of [list0_zipwith] *)

Example: Mergesort on Lists

Mergesort is a simple sorting algorithm that is guaranteed to be log-linear. It is stable in the sense that the order of two equal elements always stay the same after sorting. I give as follows a typical functional style of implementation of mergesort on lists.

First, let us introduce abbreviations for the list constructors list0_nil and list0_cons:

#define :: list0_cons // writing [::] for list0_cons
#define cons0 list0_cons // writing [cons0] for list0_cons
#define nil0 list0_nil // writing [nil0] for list0_nil

cons0(0, cons0(1, 2 :: 3 :: 4 :: nil0((*void*))))

We next implement a function template merge to merge two given ordered lists into a single ordered one:

//
typedef
lte (a:t@ype) = (a, a) -> bool
//
fun{
a:t@ype
} merge (
  xs: list0 a, ys: list0 a, lte: lte a
) : list0 a =
(
  case+ xs of
  | cons0 (x, xs1) => (
    case+ ys of
    | cons0 (y, ys1) =>
        if x lte y then
          cons0{a}(x, merge<a> (xs1, ys, lte))
        else
          cons0{a}(y, merge<a> (xs, ys1, lte))
        // end of [if]
    | nil0 () => xs
    ) // end of [cons0]
  | nil0 () => ys
) (* end of [merge] *)
//

The following function template mergesort implements the standard mergesort algorithm:

fun{
a:t@ype
} mergesort
(
  xs: list0(a), lte: lte(a)
) : list0 a = let
//
val n = list0_length<a>(xs)
//
fun msort
(
  xs: list0(a), n: int, lte: lte(a)
) : list0 a =
  if n >= 2 then split(xs, n, lte, n/2, nil0) else xs
//
and split
(
  xs: list0(a), n: int, lte: lte(a), i: int, xsf: list0(a)
) : list0 a =
  if i > 0 then let
    val-cons0 (x, xs) = xs
  in
    split (xs, n, lte, i-1, cons0{a}(x, xsf))
  end else let
    val xsf = list0_reverse<a>(xsf) // make sorting stable!
    val xsf = msort (xsf, n/2, lte) and xs = msort (xs, n-n/2, lte)
  in
    merge<a> (xsf, xs, lte)
  end // end of [if]
//
in
  msort (xs, n, lte)
end // end of [mergesort]

Note that the function template merge is not tail-recursive as the call to merge in its body is not a tail-call. This can be a serious problem in practice: It is almost certain that a stack overflow is to occur if the above implementation of mergesort is employed to sort a list that is very long (e.g., containing 1,000,000 elements or more). I will later give a tail-recursive implementation of the merge function in ATS that makes use of linear types.

Please find the entire code in this section plus some additional code for testing on-line.

Exceptions

The exception mechanism provides an efficient means for reporting a special condition encountered during program evaluation. Often such a special condition indicates an error, but it is not uncommon to employ exceptions to address issues that are not related to errors.

The type exn is predefined in ATS. One may think of exn as an extensible datatype for which new constructors can always be declared. For instance, two exception constructors are declared as follows:

exception FatalError0 of ()
exception FatalError1 of (string)

exception DivisionByZero of ()
fun divexn(x: int, y: int): int =
  if y != 0 then x / y else $raise DivisionByZero()
// end of [divexn]

A raise-expression is of the form ($raise exp) for some expression exp. Clearly, if the evaluation of exp returns a value, then the evaluation of ($raise exp) leads to a raised exception. Therefore, the evaluation of a raise-expression can never return a value, and this justifies that a raise-expression can be given any type.

A raised exception can be captured. If it is not captured, the raised exception aborts the program evaluation that issued it in the first place. In ATS, a try-expression (or try-with-expression) is of the form (try exp with clseq), where try is a keyword, exp is an expression, with is also a keyword, and clseq is a sequence of matching clauses. When evaluating such a try-expression, we first evaluate exp. If the evaluation of exp leads to a value, then the value is also the value of the try-expression. If the evaluation of exp leads to a raised exception, then we match the exception against the guards of the matching clauses in clseq. If there is a match, the raised exception is caught and we continue to evaluate the body of the first clause whose guard is matched. If there is no match, the raised exception is uncaught. In a try-expression, the with-part is often referred to as an exception-handler.

Let us now see an example that involves raising and capturing an exception. In the following program, three functions are defined to compute the product of the integers in a given list:

fun listprod1
(
  xs: list0(int)
) : int =
(
  case+ xs of
  | list0_nil() => 1
  | list0_cons(x, xs) => x * listprod1(xs)
) (* end of [listprod1] *)

fun listprod2
(
  xs: list0(int)
) : int =
(
  case+ xs of
  | list0_nil() => 1
  | list0_cons(x, xs) =>
      if x = 0 then 0 else x * listprod2(xs)
    // end of [list0_cons]
) (* end of [listprod2] *)

fun listprod3
(
  xs: list0(int)
) : int = let
  exception ZERO of ()
  fun aux(xs: list0(int)): int =
    case+ xs of
    | list0_nil() => 1
    | list0_cons(x, xs) =>
        if x = 0 then $raise ZERO() else x * aux(xs)
      // end of [list0_cons]
  // end of [aux]
in
  try aux(xs) with ~ZERO() => 0
end // end of [listprod3]

• If the integer 0 occurs in a given list, then the product of the integers in the list is 0 regardless what other integers are.

try 1*(2*(3*(aux([0,4,5,6])))) with ~ZERO() => 0

Exceptions are not a programming feature that is easy to master, and misusing exceptions is abundant in practice. So please be patient when learning the feature and be cautious when using it.

Example: Testing for Braun Trees

Braun trees are special binary trees that can be defined inductively as follows:

• If a binary tree is empty, then it is a Braun tree.

• If both children of a binary tree are Braun trees and the size of the left child minus the size of the right child equals 0 or 1, then the binary tree is a Braun tree.

A polymorphic datatype is declared as follows for representing binary trees:

datatype tree (a:t@ype) =
  | tree_nil of ((*void*))
  | tree_cons of (a, tree(a)(*left*), tree(a)(*right*))
// end of [tree] // end of [datatype]

fun{
a:t@ype
} size
(
t0: tree(a)
) : int =
(
case+ t0 of
| tree_nil() => 0
| tree_cons(_, tl, tr) => 1 + size(tl) + size(tr)
) (* end of [size] *)

fun{
a:t@ype
} brauntest0
(
t0: tree(a)
) : bool =
(
case+ t0 of
| tree_nil() => true
| tree_cons(_, tl, tr) => let
    val test = brauntest0(tl) andalso brauntest0(tr)
  in
    if test
      then let
        val dif = size(tl)-size(tr) in (dif=0) orelse (dif=1)
      end else false
    // end of [if]
  end // end of [tree_cons]
) (* end of [brauntest0] *)

In the following program, the defined function brauntest1 also tests whether a given binary tree is a Braun tree:

fun{
a:t@ype
} brauntest1
(
t0: tree(a)
) : bool = let
//
exception Negative of ()
//
  fun
  aux
  (
  t0: tree(a)
  ) : int =
  (
    case+ t0 of
    | tree_nil() => 0
    | tree_cons
        (_, tl, tr) => let
        val szl = aux(tl)
        and szr = aux(tr)
        val dif = szl - szr
      in
        if (dif=0 orelse dif=1) then 1+szl+szr else $raise Negative()
      end // end of [tree_cons]
  ) (* end of [aux] *)
//
in
  try let
    val _ = aux(t0)
  in
    true // [t] is a Braun tree
  end with
    ~Negative() => false // [t] is not a Braun tree
  // end of [try]
end // end of [brauntest1]

The use of the exception mechanism in the implementation of brauntest1 is a convincing one because the range between the point where an exception is raised and the point where the raised exception is captured can span many function calls. If this range is short (e.g., spanning only one function call) in a case, then the programmer should probably investigate whether it is a sensible use of the exception mechanism. For instance, the use of exception in the following example may seem interesting but it actually leads to very inefficient code:

fun{
a:t@ype
} list0_length
  (xs: list0(a)): int =
  try 1 + list0_length(xs.tail()) with ~ListSubscriptExn() => 0
// end of [list0_length]

Please find the entirety of the code in this section plus some additional code for testing on-line.

References

A reference is just a singleton array, that is, an array containing one element. Given a type T, a reference for storing a value of the type T is given the type ref(T). The following simple program makes use of all the essential functionalities on references:

val intr = ref<int>(0) // create a ref and init. it with 0
val ((*void*)) = !intr := !intr + 1 // increase the integer at [intr] by 1

Various functions and function templates on references are declared in the file reference.sats, which is automatically loaded by atsopt. In particular, it is also possible to read from and write to a reference by using the function templates ref_get_elt and ref_set_elt of the following interfaces, respectively:

fun{a:t@ype} ref_get_elt(r: ref a): a // !r
fun{a:t@ype} ref_set_elt(r: ref a, x: a): void // !r := x

References are often misused in practice, especially, by beginners of functional programming who had some previous exposure to imperative programming languages such C and Java. Such programmers often think that they can just "translate" their programs in C or Java into functional programs. For example, the following defined function sumup is such an example, which sums up all the integers between 1 and a given integer, inclusive:

fun sumup
  (n: int): int = let
  val i = ref<int>(1)
  val res = ref<int>(0)
  fun loop(): void =
    if !i <= n then (!res := !res + !i; !i := !i + 1; loop())
  // end of [loop]
in
  loop(); !res
end // end of [sumup]

I consider references a dangerous feature in functional programming. If you want to run your program without GC, please do not create references in the body of a function (besides many other restrictions). If you find that you are in need of references to "translate" imperative programs into functional ones, then it is most likely that you are lost and you have not learned well to program in a functional style yet.

Example: A Counter Implementation

Let us see as follows the implementation of a counter-like object in the style of object-oriented programming (OOP). The type counter for counters is defined as follows:

typedef
counter = '{
  get= () -<cloref1> int
, inc= () -<cloref1> void
, reset= () -<cloref1> void
} // end of [counter]

fun newCounter
(
// argumentless
) : counter = let
  val count = ref<int>(0)
in '{
  get= lam () => !count
, inc= lam () => !count := !count + 1
, reset= lam () => !count := 0
} end // end of [newCounter]