**Table of Contents**- Preface
- I. Basic Tutorial Topics
- 1. Syntax-Coloring for ATS code
- 2. Filename Extensions
- 3. File Inclusion inside ATS Code
- 4. Fixity Declarations
- 5. Static Load
- 6. Dynamic Load
- 7. Bracket Overloading
- 8. Dot-Symbol Overloading
- 9. Recursion
- 10. Datatypes
- 11. Functional Lists
- 12. Functional Sets and Maps
- 13. Exceptions
- 14. References
- 15. Boxed Tuples and Records
- 16. Persistent Arrays
- 17. Persistent Arrays-with-size
- 18. Persistent Matrices
- 19. Persistent Matrices-with-size
- 20. Persistent Hashtables
- 21. Tail-Recursion
- 22. Higher-Order Functions
- 23. Stream-Based Lazy Evaluation
- 24. Linearly Typed Lists

- II. Advanced Tutorial Topics

This tutorial covers a variety of issues that a programmer typically encounters when programming in ATS. It is written mostly in the style of learn-by-examples. Although it is possible to learn programming in ATS by studying the tutorial (if the reader is familiar with ML and C), I consider the book Introduction to Programming in ATS a far more approriate source for someone to acquire a view of ATS in a coherent and systematic manner. Of course, there will also be considerable amount of overlapping between these two books. The primary purpose of the tutorial is to bring more insights into a rich set of programming features in ATS and also demonstrate through concrete examples that these features can be made of effective use in the construction of high-quality programs.

**Table of Contents**- 1. Syntax-Coloring for ATS code
- 2. Filename Extensions
- 3. File Inclusion inside ATS Code
- 4. Fixity Declarations
- 5. Static Load
- 6. Dynamic Load
- 7. Bracket Overloading
- 8. Dot-Symbol Overloading
- 9. Recursion
- 10. Datatypes
- 11. Functional Lists
- 12. Functional Sets and Maps
- 13. Exceptions
- 14. References
- 15. Boxed Tuples and Records
- 16. Persistent Arrays
- 17. Persistent Arrays-with-size
- 18. Persistent Matrices
- 19. Persistent Matrices-with-size
- 20. Persistent Hashtables
- 21. Tail-Recursion
- 22. Higher-Order Functions
- 23. Stream-Based Lazy Evaluation
- 24. Linearly Typed Lists

The syntax of ATS is highly involved, which can be a daunting obstacle for beginners trying to read and write ATS code. In order to alleviate this problem, I may employ colors to differentiate various syntactical entities in ATS code. The convention I adopt for coloring ATS syntax is given as follows:

The keywords in ATS are all colored black (and possibly written in bold face).

The comments in ATS are all colored gray.

The code in the statics of ATS is colored blue.

The code in the dynamics of ATS is colored red unless it represents proofs, for which the color dark green is used.

The external code (in C) is colored deep brown.

Please find an example of ATS code on-line that involves all of the syntax-coloring mentioned above.

In ATS, the filename extensions *.sats* and *.dats*
are reserved to indicate static and dynamic files, respectively. As these
two extensions have some special meaning attached to them, which can be
interpreted by the command **atscc**, they should not be replaced
arbitrarily.

A static file may contain sort definitions, datasort declarations, static
definitions, abstract type declarations, exception declarations, datatype
declarations, macro definitions, interfaces for dynamic values and
functions, etc. In terms of functionality, a static file in ATS is
somewhat similar to a header file (with the extension *.h*) in C
or an interface file (with the extension *.mli*) in OCaml.

A dynamic file may contain everything in a static file. In addition, it may also contain definitions for dynamic values and functions. However, interfaces for functions and values in a dynamic file should follow the keyword extern, which on the other hand should not be present when such interfaces are declared in a static file. For instance, the following syntax declares interfaces (or types) in a static file for a value named pi and a function named area_of_circle:

When the same interfaces are declared in a
As a convention, we often use the filename extension *.cats* to
indicate that a file contains some C code that is supposed to be combined
with ATS code in certain manner. There is also the filename extension
*.hats*, which we occassionally use for a file that should be
included in ATS code stored in another file. However, the use of these two
filename extensions are not mandatory, that is, they can be replaced if
needed or wanted.

As is in C, file inclusion inside ATS code is done through the use of the
directive *#include*. For instance, the following line
indicates that a file named *foobar* is included, that is, this
line is to be replaced with the content of the file *foobar*:

A common use of file inclusion is to keep some constants, flags or parameters being defined consistently across a set of files. For instance, the file prelude/params.hats serves such a purpose. File inclusion can also be used to emulate (in a limited but rather useful manner) functors supported in languages such as SML and OCaml.

Given a function *f*, the standard syntax for applying
*f* to an argument *v* is *f(v)*; for two
arguments *v1* and *v2*, the syntax is
*f(v1, v2)*. Also, it is allowed in ATS to use infix notation
for a binary function application, and prefix/postifix notation for a unary
function application.

Each identifier in ATS can be assigned one of the following fixities:
*prefix*, *infix* and *postfix*. The
fixity declarations for many commonly used identifiers can be found in
prelude/fixity.ats. Often, the
name *operator* is used to refer to an identifier that is
assigned a fixity. For instance, the following syntax declares that
+ and - are infix operators of a precedence value
equal to 50:

The keyword infixl indicates that the declared infix operators are left-associative. For right-associative and non-associative infix operators, please use the keywords infixr and infix, respectively. If the precedence value is omitted in a fixity declaration, it is assumed to be equal to 0.

We can also use the following syntax to declare that iadd, fadd, padd and uadd are left-associative infix operators with a precedence value equal to that of the operator +:

This is useful as it is difficult in practice to remember the precedence values of (a large collection of) declared operators. Sometimes, we may need to specify that the precedence value of one operator in relation to that of another one. For instance, the following syntax declares that opr2 is a left-associative infix operator and its precedence value is that of opr1 plus 10: If the plus sign (+) is changed to the minus sign (-), then the precedence value of opr2 is that of opr1 minus 10.We can also turn an identifier opr into a non-associative infix operator (of precedence value 0) by putting the backslash symbol (\) in front of it. For instance, the expression exp1 \opr exp2 stands for opr (exp1, exp2), where exp1 and exp2 refer to some expressions, either static or dynamic.

The syntax for declaring (unary) prefix and postfix operators are similar. For instance, the following syntax declares that ~ and ? are prefix and postfix operators of precedence values 61 and 69, respectively:

As an example, a postfix operator is involved in the following 3-line program:postfix (imul + 10) !! extern fun !! (x: int): int implement !! (x) = if x >= 2 then x * (x - 2)!! else 1

For a given occurrence of an operator, we can deprive it of its assigned fixity status by simply putting the keyword op in front of it. For instance 1 + 2 - 3 can be writen as op- (op+ (1, 2), 3). It is also possible to (permanently) deprive an operator of its assigned fixity status. For instance, the following syntax does so to the operators iadd, fadd, padd and uadd:

Note that nonfix is a keyword in ATS.Lastly, please note that each fixity declaration is only effective within its own legal scope.

In ATS, static load (or staload for short) refers to the creation of a namespace populated with the declared names in a loaded package.

Suppose that a file named `foo.sats` contains the
following code:

If the file `foo.sats` is staloaded as follows for the second
time:

It is also allowed for `foo.sats` to be staloaded as follows:

Let us suppose that we have the following sequence of declarations:

Does the second occurrence of aValue refer to the one introduced in the first declaration, or it refers to the one declared insideIn ATS, dynamic load (or dynload for short) refers to some form of initialization of a loaded package.

Suppose that a file named `foo.dats` contains the following
code:

// val x = 1000 val y = x + x // = 2000 val z = y * y // = 4000000 // extern fun sum_x_y_z (): int // implement sum_x_y_z () = x + y + z //

staload "./foo.dats" dynload "./foo.dats" // for initialization implement main0 () = { val () = assertloc (4003000 = sum_x_y_z()) } (* end of [main0] *)

The line starting with the keyword dynload is referred to as a
dynload-declaration. If it is deleted from the file `foo2.dats`,
then executing the above command-line leads to link-time reporting of
undefined reference to a variable of certain name ending with the string
*__dynloadflag*. The dynload-declaration for
`foo.dats` introduces this special variable and then makes a
call to a special function associated with `foo.dats` for the
purpose of performing some form of initialization. This special function
is referred as a dynload-function (for `foo.dats`), which is
always idempotent.

There is also a dynload-function generated for `foo2.dats`.
As the function main0, a variant of the special function
main, is implemented in `foo2.dats`, the
dynload-function for `foo2.dats` is automatically called inside
the body of the main function.

If there is a reason to suppress the generation of a dynload-function, one
can set the value of the flag ATS_DYNLOADFLAG to 0. For
instance, no dynload-function for `foo.dats` is generated if the
following line is added into `foo.dats`:

If there is a reason to call the dynload-function for
`foo2.dats` explicitly, one can introduce an alias for it and then
call the alias. For instance, if the following line is added to
`foo2.dats`:

Please find on-line the entirety of the code used in this chapter.

In many programming languages, bracket-notation is commonly associated with array subscripting. For instance, A[i] is a left-value in C that refers to array-cell i in the array referred to by A. There is support in ATS for overloading brackets with multiple function names so that bracket-notation can be employed to call these functions, resulting in code that reads like some form of subscripting. It is expected that this style of calling functions can, sometimes, make the code written in ATS more easily accessible.

Let us now see a simple example of bracket-notation in overloading. In the followng code, a linear abstract type lock is introduced together with two functions:

// absvtype lock(a:vt@ype) // extern fun{a:vt0p} lock_acquire(!lock(a)): a extern fun{a:vt0p} lock_release(!lock(a), a): void //

Suppose that we now introduce the following overloading declarations:

With these declarations, the following code typechecks:// val mylock = $extval(lock(int), "mylock") // val x0 = mylock[] // = lock_acquire (mylock) val () = mylock[] := x0 // = lock_release (mylock, x0) //

In ATS, bracket-notation is already overloaded with functions performing list-subscripting, array-subscripting and matrix-subscripting, and it can also be used to access and update a given reference.

Please find on-line the entirety of the code presented in this chapter.

In many programming languages, the so-called dot-notation is commonly associated with selecting a field from a given tuple-value, record-value or object-value. In ATS, field selection can be done through either pattern matching or the use of dot-notation. For example, the following code constructs a flat tuple and also a boxed one, and then uses dot-notation to select their components:

// val tup_flat = @("a", "b") val tup_boxed = $tup("a", "b") // val-"a" = tup_flat.0 and "b" = tup_flat.1 val-"a" = tup_boxed.0 and "b" = tup_boxed.1 //

As an example of dot-notation in overloading, let us introduce a non-linear abstract type point for points in a 2-dimensional space and also declare some associated functions:

// abstype point = ptr // boxed // extern fun point_make (x: double, y: double): point // extern fun point_get_x (p: point): double and point_get_y (p: point): double // extern fun point_set_x (p: point, x: double): void and point_set_y (p: point, x: double): void //

symintr .x .y overload .x with point_get_x overload .x with point_set_x overload .y with point_get_y overload .y with point_set_y

val p0 = point_make (1.0, ~1.0) val x0 = p0.x() // point_get_x (p0) and y0 = p0.y() // point_get_y (p0) val () = p0.x := y0 // point_set_x (p0, y0) and () = p0.y := x0 // point_set_y (p0, x0)

Let us introduce a linear abstract type counter for counter objects and a few functions associated with it:

// absvtype counter = ptr // extern fun counter_make (): counter extern fun counter_free (counter): void // extern fun counter_get (cntr: !counter): int extern fun counter_incby (cntr: !counter, n: int): void //

Let us introduce the following overloading declarations:

As is expected, one can now call counter_get as follows: Similarly, one can call counter_incby as follows to increase the count stored in c0 by 1: If we revisit the previous example involving (non-linear) points, then we can see that the following code also typechecks:val p0 = point_make (1.0, ~1.0) val x0 = p0.x() // point_get_x (p0) and y0 = p0.y() // point_get_y (p0) val () = p0.x(y0) // point_set_x (p0, y0) and () = p0.y(x0) // point_set_y (p0, x0)

Please find on-line the entirety of the code presented in this chapter plus some testing code.

The notion of recursion is ubiquitous in ATS. For instance, there are
recursively defined sorts (datasorts) and types (datatypes) in the statics,
and there are also recursively defined functions in the dynamics.
Literally, the word *recurse* means "go back". When an entity is
defined recursively, it means that the entity being defined can appear in
its own definition. In the following presentation, I will show several ways
to define (or implement) recursive functions and non-recursive functions,
where the latter is just a special case of the former.

The keyword fun can be used to initiate the definition of a recursive function. For instance, following is the definition of a recursive function:

A non-recursive function is a special kind of recursive function that does make use of itself in its own definition. So one can certainly use fun to initiate the definition of a non-recursive function. However, if there is a need to indicate explicitly that a non-recursive is being defined, then one can use the keyword fn to do so. For instance, the definiton of a non-recursive function is given as follows: which is directly translated by the compiler into the following binding between a name and a lambda-expression: As another example, please note that the two occurrences of the symbol fact in the following code refer to two distinct functions: While the first fact (to the left of the equality symbol) refers to the (non-recursive) function being defined, the second one is supposed to have been declared previously.A recursive function can also be defined as a recursive value. For instance, the recursive function fact defined above can be defined as follows:

where the keyword rec indicates that fact is defined recursively, that is, it is allowed to appear in its own definition. In fact, the former definition of fact is directly translated into the latter one by the compiler. Of course, one may also use a reference to implement recursion:val fact = ref<int->int>($UNSAFE.cast(0)) val () = !fact := ( lam (x:int):int => if x > 0 then x * !fact(x-1) else 1 ) (* end of [val] *)

For defining mutually recursive functions, one can simply use the keyword and to concatenate function definitions. For instance, the following code defines two functions isevn and isodd mutually recursively:

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

val rec isevn : int -> bool = lam (x) => if x > 0 then isodd(x-1) else true and isodd : int -> bool = lam (x) => if x > 0 then isevn(x-1) else false

Even at this point, I have not presented all of the possible ways to define functions in ATS. For instance, one can also define stack-allocated closure-functions in ATS, which may be either recursive or non-recursive. I plan to introduce such functions elsewhere in this tutorial.

Often, the interface (that is, type) for a function is declared at one place and its definition (or implementation) is given at another place. For instance, one may first introduce the following declaration:

Later, one can implement fact according to the above declaration: When implement is used to initiate the definition of a function, any previously declared symbols (including the one that is being defined) can appear in the definition. If it is desirable, one may replace implement with implmnt.Please find on-line the entirety of the code used in this chapter.

Datatypes are a form of user-defined types for classifying data (or values). The support for datatypes and pattern matching in ATS is primarily adopted from ML.

The following code declares a datatype of the name weekday for values representing weekdays:

There are five data constructors associated with weekday, which are Monday, Tuesday, Wednesday, Thursday, and Friday. All of these data constructors are nullary, that is, they take no arguments to form values (of the type weekday).Each nullary constructor is represented as a small integer (e.g., one that is less than 1024). One can use the following function weekday2int to find out the integers reprsenting the constructors associated with weekday:

// staload UN = "prelude/SATS/unsafe.sats" // fun weekday2int (wd: weekday): int = $UN.cast{int}($UN.cast{intptr}(wd)) //

Given a nullary constructor foo, both foo and foo() can be used to refer the value constructed by foo. However, only foo() can be used as the pattern that matches this value. For instance, the following function tests whether a given value of the type weekday is formed with the constructor Friday:

Note that the pattern Friday() cannot be replaced with Friday as the latter is treated as a variable when used as a pattern. On the other hand, both of the following assertions hold at run-time as Friday and Friday() refer to the same value:If there is only one constructor associated with a datatype, then there is no tag in the representation for values of this datatype.

A datatype is list-like if there are two data constructors associated with it such that one is nullary (nil-like) and the other is non-nullary (cons-like). For instance, the datatype ab declared as follows is list-like:

The values of a list-like datatype are represented in a special way. Given a value of the datatype; if it is constructed with the nil-like constructor, then it is represented as the null-pointer; if it is constructed with the cons-like constructor, then it is reprenstend as a heap-allocated tuple containing all of the arguments passed to the constructor. In the above case, the value A() is represented as the null pointer, and the value B(b) for each boolean b is represented as a heap-allocated singleton tuple containing the only component b. This description can be readily verified with the following code:val () = assertloc (iseqz($UN.cast{ptr}(A()))) val () = assertloc (true = $UN.ptr0_get<bool>($UN.cast{ptr}(B(true)))) val () = assertloc (false = $UN.ptr0_get<bool>($UN.cast{ptr}(B(false))))

The following declaration introduces a datatype of the name abc:

The three constructors associated with abc are A, B, and C; A is nullary; B is unary, taking a boolean to form a value (of the type abc); C is binary, taking an integer and a float (of double precision) to form a value (of the type abc).In a general case, if a data constructor is n-ary for some positive n, then each value it constructs is a heap-allocated tuple of n+1 components, where the first one is the tag assigned to the constructor and the rest are the arguments passed to the constructor. For instance, the following function can be called to find out the tags assigned to the constructors associated with abc:

fun abc2tag (x: abc): int = let val p = $UN.cast{intptr}(x) in // case+ 0 of | _ when p < 1024 => $UN.cast{int}(p) | _ (*heap-allocated*) => $UN.ptr0_get<int>($UN.cast{ptr}(p)) // end // end of [abc2tag]

Datatypes can be defined recursively. As an example, the following declaration introduces a recursively defined datatype intexp (for representing arithemetic integer expressions):

datatype intexp = | Int of int | Neg of (intexp) | Add of (intexp, intexp) | Sub of (intexp, intexp)

datatype intexp = | Int of int | Neg of (intexp) | Add of (intexp, intexp) | Sub of (intexp, intexp) | IfThenElse of (boolexp, intexp, intexp) and boolexp = | Bool of bool // constant | Not of (boolexp) // negation | Less of (intexp, intexp) // Less(x, y): x < y | LessEq of (intexp, intexp) // LessEq(x, y): x <= y | Conj of (boolexp, boolexp) // Conj(x, y): x /\ y | Disj of (boolexp, boolexp) // Disj(x, y): x \/ y

// symintr eval // extern fun eval_intexp : intexp -> int extern fun eval_boolexp : boolexp -> bool // overload eval with eval_intexp overload eval with eval_boolexp // (* ****** ****** *) // implement eval_intexp (e0) = ( // case+ e0 of | Int (i) => i | Neg (e) => ~eval(e) | Add (e1, e2) => eval(e1) + eval(e2) | Sub (e1, e2) => eval(e1) - eval(e2) | IfThenElse (e_test, e_then, e_else) => if eval(e_test) then eval(e_then) else eval(e_else) // ) (* end of [eval_intexp] *) // implement eval_boolexp (e0) = ( // case+ e0 of | Bool (b) => b | Not (e) => ~eval(e) | Less (e1, e2) => eval(e1) < eval(e2) | LessEq (e1, e2) => eval(e1) <= eval(e2) | Conj (e1, e2) => eval(e1) && eval(e2) | Disj (e1, e2) => eval(e1) || eval(e2) // ) (* end of [eval_boolexp] *) // (* ****** ****** *)

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

A functional list is just a singly-linked list that is immutable after its construction. The following datatype declaration introduces a type list for functional lists:

// datatype list(a:t@ype, int) = | list_nil(a, 0) of () | {n:nat} list_cons(a, n+1) of (a, list(a, n)) //

There are various functions in ATSLIB for list construction. In practice, a list is usually built by making direct use of the constructors list_nil and list_cons. For instance, the following function fromto builds a list of integers between two given ones:

// fun fromto {m,n:int | m <= n} ( m: int(m), n: int(n) ) : list(int, n-m) = if m < n then list_cons(m, fromto(m+1, n)) else list_nil() //

// fun {a:t@ype} list_length {n:nat} ( xs: list(a, n) ) : int(n) = let // fun loop {i,j:nat} ( xs: list(a, i), j: int(j) ) : int(i+j) = ( case+ xs of | list_nil () => j | list_cons (_, xs) => loop(xs, j+1) ) // in loop (xs, 0) end // end of [list_length] //

// fun {a,b:t@ype} list_foldleft {n:nat} ( f: (a, b) -> a, ini: a, xs: list(b, n) ) : a = if iseqz(xs) then ini else list_foldleft(f, f(ini, xs.head()), xs.tail()) // end of [if] //

// fun {a,b:t@ype} list_foldright {n:nat} ( f: (a, b) -> b, xs: list(a, n), snk: b ) : b = if iseqz(xs) then snk else f(xs.head(), list_foldright(f, xs.tail(), snk)) // end of [if] //

As an application of list_foldleft, the following code implements a function for reversing a given list:

fun {a:t@ype} list_reverse ( xs: List0(a) ) : List0(a) = ( list_foldleft<List0(a),a> (lam (xs, x) => list_cons(x, xs), list_nil, xs) )

fun {a:t@ype} list_reverse {n:nat} ( xs: list(a, n) ) : list(a, n) = let // fun loop{i,j:nat} ( xs: list(a, i), ys: list(a, j) ) : list(a, i+j) = case+ xs of | list_nil () => ys | list_cons (x, xs) => loop (xs, list_cons (x, ys)) // in loop (xs, list_nil) end // end of [list_reverse]

As an application of list_foldright, the following code implements a function for concatenating two given lists:

// fun {a:t@ype} list_append ( xs: List0(a), ys: List0(a) ) : List0(a) = list_foldright<a, List0(a)>(lam (x, xs) => list_cons(x, xs), ys, xs) //

// fun {a:t@ype} list_append {m,n:nat} ( xs: list(a,m), ys: list(a,n) ) : list(a,m+n) = ( case+ xs of | list_nil () => ys | list_cons (x, xs) => list_cons (x, list_append (xs, ys)) ) //

One may think of a functional list as a representation for the finite mapping that maps each natural number i less than the length of the list to element i in the list. The following function list_get_at is for accessing a list element at a given position:

// fun {a:t@ype} list_get_at {n:nat} ( xs: list(a, n), i: natLt(n) ) : a = if i > 0 then list_get_at(xs.tail(), i-1) else xs.head() //

There is no destructive update on a functional list as it is immutable. The following function list_set_at can be called to construct a list that differs from a given one only at a given position:

// fun {a:t@ype} list_set_at {n:nat} ( xs: list(a, n), i: natLt(n), x0: a ) : list(a, n) = if i > 0 then list_cons(xs.head(), list_set_at(xs.tail(), i-1, x0)) else list_cons(x0, xs.tail()) // end of [if] //

Functional lists are by far the most widely used data structure in functional programming. However, one should not attempt to use a functional list like an array as doing so is inefficient both time-wise and memory-wise.

Please find on-line the entirety of the code used in this chapter plus some testing code.

Both (finite) sets and (finite) maps are commonly used data structures. Functional sets and maps are immutable after their construction. Insertion into or removal from a functional set/map results in the construction of a new set/map while the original is kept intact. Usually the newly constructed set/map and the original one share a lot of underlying representation. Note that a functional set/map cannot be safely freed explicitly and the memory for representing it can only be reclaimed through garbage collection (GC).

Suppose that a set is needed for collecting values of type elt_t. The following code essentially sets up an interface for creating and operating on such a set based on a balanced-tree implementation in ATSLIB/libats:

local // typedef elt = elt_t // staload FS = "libats/ML/SATS/funset.sats" implement $FS.compare_elt_elt<elt>(x, y) = compare(x, y) // in (* in-of-local *) #include "libats/ML/HATS/myfunset.hats" end // end of [local]

Assume that elt_t is int. The following line of code creates a functional set (of integers) containing no elements:

The function for inserting an element into a given set is assigned the following type: The dot-symbol .insert is overloaded with the function myfunset_insert. Note that the first argument of myfunset_insert is call-by-reference. If the given element is inserted into the given set, then the newly created set is stored into the call-by-reference argument and false is returned (to indicate no error). Otherwise, true is returned (to indicate a failure). The following few lines of code shows how insertion can be operated on a functional set:// var myset = myset // val-false = myset.insert(0) // inserted val-(true) = myset.insert(0) // not actually inserted val-false = myset.insert(1) // inserted val-(true) = myset.insert(1) // not actually inserted //

val-true = myset.remove(0) // removed val-false = myset.remove(0) // not actually removed val-true = myset.remove(1) // removed val-false = myset.remove(1) // not actually removed

Various common set operations can be found in libats/ML/HATS/myfunset.hats. By following the types assigned to these operations, one should have no difficulty in figuring out how they are supposed to be called. Please find the entirety of the code used in this section on-line.

Suppose that a map is needed for mapping keys of type key_t to items of type itm_t. The following code essentially sets up an interface for creating and operating on such a map based on a balanced-tree implementation in ATSLIB/libats:

local // typedef key = key_t and itm = itm_t // staload FM = "libats/ML/SATS/funmap.sats" implement $FM.compare_key_key<key>(x, y) = compare(x, y) // in (* in-of-local *) #include "libats/ML/HATS/myfunmap.hats" end // end of [local]

Assume that key_t is string and itm_t is int. The following line of code creates an empty functional map:

The following few lines insert some key/item pairs into mymap:// var mymap = mymap // val-~None_vt() = mymap.insert("a", 0) val-~Some_vt(0) = mymap.insert("a", 1) // val-~None_vt() = mymap.insert("b", 1) val-~Some_vt(1) = mymap.insert("b", 2) // val-~None_vt() = mymap.insert("c", 2) val-~Some_vt(2) = mymap.insert("c", 3) //

// val-true = mymap.remove("a") val-false = mymap.remove("a") // val-~Some_vt(2) = mymap.takeout("b") val-~Some_vt(3) = mymap.takeout("c") //

Various common map operations can be found in libats/ML/HATS/myfunmap.hats. By following the types assigned to these operations, one should have no difficulty in figuring out how they are supposed to be called. Please find the entirety of the code used in this section on-line.

While exceptions can be very useful in practice, it is also very common to see code that misuses exceptions.

Generally speaking, there are exceptions that are meant to be raised but not captured for the purpose of aborting program execution, and there are also exceptions (often declared locally) that are meant to be raised and then captured so as to change the flow of program execution. For instance, the exception ArraySubscriptExn is raised when out-of-bounds array subscripting is detected at run-time. Once it is raised, ArraySubscriptExn is usually not meant to be captured. While there is certainly nothing preventing a programer from writing code that captures a raised ArraySubscriptExn, a major concern is that reasoning can become greatly complicated on code that does so. In the following presentation, I will soley focus on exceptions that are meant to be raised and then captured.

Let us now take a look at the following code that implements a function for finding the rightmost element in a list that satisfies a given predicate:

extern fun{a:t@ype} list_find_rightmost (List (a), (a) -<cloref1> bool): Option_vt (a) // implement{a} list_find_rightmost (xs, pred) = let // fun aux ( xs: List(a) ) : Option_vt (a) = case+ xs of | nil () => None_vt () | cons (x, xs) => let val res = aux (xs) in case+ res of | Some_vt _ => res | ~None_vt () => if pred (x) then Some_vt (x) else None_vt () // end of [None] end (* end of [cons] *) // in aux (xs) end // end of [list_find_rightmost]

implement{a} list_find_rightmost (xs, pred) = let // exception Found of (a) // fun aux ( xs: List(a) ) : void = case+ xs of | nil () => () | cons (x, xs) => let val () = aux (xs) in if pred (x) then $raise Found(x) else () end (* end of [cons] *) // in // try let val () = aux (xs) in None_vt () end with | ~Found(x) => Some_vt (x) // end // end of [list_find_rightmost]

The implementation of the run-time support for exceptions in ATS makes use
of the function alloca declared in `alloca.h` and
the functions setjmp and longjmp declared in
`setjmp.h`. If **gcc** or **clang** is used to
compile the C code generated from ATS source, one can pass the flag
-D_GNU_SOURCE so as to make sure that the header file `alloca.h`
is properly included.

Please find on-line the entirety of the code used in this chapter.

A reference is a singleton array, that is, an array of size 1. It is persistent in the sense that the (heap-allocated) memory for storing the content of a reference cannot be freed manually in a type-safe manner. Instead, it can only be reclaimed through garbage collection (GC).

Given a viewtype VT, the type for references to values of viewtype VT is ref(VT). For convenience, the type constructor ref is declared to be abstract in ATS. However, it can be defined as follows:

The interfaces for various functions on references can be found in prelude/SATS/reference.sats.For creating a reference, the function template ref_make_elt of the following interface can be called:

It is also allowed to use the shorthand ref for ref_make_elt. Note that the symbol !wrt indicates that the so-called wrt-effect may occur when ref_make_elt is called.For reading from and writing through a reference, the function templates ref_get_elt and ref_set_elt can be used, respectively, which are assigned the following types:

fun{a:t@ype} ref_get_elt (r: ref a):<!ref> a fun{a:t@ype} ref_set_elt (r: ref a, x: a):<!refwrt> void

A reference is typically employed to record some form of persistent state. For instance, following is such an example:

local // #define BUFSZ 128 // val count = ref<int> (0) // in (* in of [local] *) fun genNewName (prfx: string): string = let val n = !count val () = !count := n + 1 var res = @[byte][BUFSZ]((*void*)) val err = $extfcall ( int, "snprintf", addr@res, BUFSZ, "%s%i", prfx, n ) (* end of [$extfcall] *) in strptr2string(string0_copy($UNSAFE.cast{string}(addr@res))) end // end of [genNewName] end // end of [local]

*Misuse of References*
References are commonly misused in practice. The following program is often
written by a beginner of functional programming who has already learned
(some) imperative programming:

fun fact (n: int): int = let val res = ref<int> (1) fun loop (n: int):<cloref1> void = if n > 0 then (!res := n * !res; loop(n-1)) else () val () = loop (n) in !res end // end of [fact]

fun fact (n: int): int = let fun loop (n: int, res: int): int = if n > 0 then loop (n-1, n * res) else res // end of [loop] in loop (n, 1) end // end of [fact]

Unless strong justification can be given, making extensive use of (dynamically created) references is often a sure sign of poor coding style.

*Statically Allocated References*
Creating a reference by calling ref_make_elt involves dynamic
memory allocation. If this is not desirable or even acceptable, it is
possible to only employ statically allocated memory in a reference creation
as is shown below:

Please find on-line the entirety of the code used in this chapter.

A *boxed* tuple/record is just a reference to
some location in memory where a flat tuple/record is stored.
Often the word *unboxed* is also used to describe a
flat tuple/record.

In the following code, the types abc_tup and abc_rec are for boxed tuples and records, respectively:

typedef abc_tup = '(int, int, string) // for tuples typedef abc_rec = '{a=int, b=int, c=string} // for records

typedef abc_tup = $tup(int, int, string) // for tuples typedef abc_rec = $rec{a=int, b=int, c=string} // for records

The following code demonstrates how tuples and records can be created and their components (i.e., fields) taken out:

// val x_tup = '(0, 1, "2") : abc_tup val x_rec = '{a=0, b=1, c="2"} : abc_rec // val ((*void*)) = assertloc(x_tup.0 = x_rec.a) val ((*void*)) = assertloc(x_tup.1 = x_rec.b) val ((*void*)) = assertloc(x_tup.2 = x_rec.c) //

It should be noted that both x_tup and x_rec are immutable. If one tries to typecheck the following code, then he or she should see error messages reporting that x_tup.0 and x_rec.a are non-left-values:

// val () = x_tup.0 := 100 // *ERROR*: x_tup.0 not a left-value val () = x_rec.a := 100 // *ERROR*: x_tup.0 not a left-value //

In order to have a tuple/record with mutable fields, we can just literally create a reference to a flat tuple/record. In the following code, the types abc_tup_ and abc_rec_ are declcared for flat tuples and records, respectively:

// typedef abc_tup_ = @(int, int, string) // for tuples typedef abc_rec_ = @{a=int, b=int, c=string} // for records //

// typedef abc_tup_r = ref(abc_tup_) // for tuples typedef abc_rec_r = ref(abc_rec_) // for records //

// val x_tup_r = ref<abc_tup_>(@(0, 1, "2")) val x_rec_r = ref<abc_rec_>(@{a=0, b=1, c="2"}) // (* ****** ****** *) // val () = assertloc(x_tup_r->0 = x_rec_r->a) val () = assertloc(x_tup_r->1 = x_rec_r->b) val () = assertloc(x_tup_r->2 = x_rec_r->c) // (* ****** ****** *) // val () = x_tup_r->0 := 100 // *OKAY*: x_tup_r.0 is a left-value val () = x_rec_r->a := 100 // *OKAY*: x_rec_r.a is a left-value //

If we want to have records of a type where certain fields are read-only while the others may be updated, we can do this by making use of the support for abstract types in ATS. In the following example, myrec is declared to be abstract; there are three fields associated with myrec that are of the names a, b, and c; the first two may be updated while the third one is read-only:

(* ****** ****** *) abstype myrec = ptr (* ****** ****** *) // extern fun{} myrec_make ( a: int, b: int, c: string ) : myrec // end-of-function // extern fun{} myrec_get_a : myrec -> int extern fun{} myrec_set_a : (myrec, int) -> void extern fun{} myrec_get_b : myrec -> int extern fun{} myrec_set_b : (myrec, int) -> void extern fun{} myrec_get_c : myrec -> string // overload .a with myrec_get_a overload .a with myrec_set_a overload .b with myrec_get_b overload .b with myrec_set_b overload .c with myrec_get_c // (* ****** ****** *) local // assume myrec = abc_rec_r // in (* in-of-local *) // implement {}(*tmp*) myrec_make (a, b, c) = ref(@{a=a, b=b, c=c}) // implement{} myrec_get_a(x) = x->a implement{} myrec_set_a(x, a) = x->a := a // implement{} myrec_get_b(x) = x->b implement{} myrec_set_b(x, b) = x->b := b // implement{} myrec_get_c(x) = x->c (* // // there is no update for the c-field: // implement{} myrec_set_a(x, c) = x->c := c *) // end // end of [local] (* ****** ****** *)

// val x_abc = myrec_make(0, 1, "2") // val ((*void*)) = assertloc(x_abc.a() = 0) val ((*void*)) = assertloc(x_abc.b() = 1) val ((*void*)) = assertloc(x_abc.c() = "2") // val ((*void*)) = x_abc.a(100) val ((*void*)) = assertloc(x_abc.a() = 100) // val ((*void*)) = x_abc.b(101) val ((*void*)) = assertloc(x_abc.b() = 101) // (* val ((*void*)) = x_abc.c("102") // *ERROR*: unsupported *) //

Please find on-line the entirety of the code used in this chapter plus some testing code.

A persistent array of size n is just n heap-allocated cells (or references) in a row. It is persistent in the sense that the memory allocated for the array cannot be freed manually. Instead, it can only be safely reclaimed through garbage collection (GC).

Given a viewtype VT, the type for persistent arrays containing N values of
viewtype VT is arrayref(VT, N). Note that arrays in ATS are
the same as those in C: There is no size information attached to them. The
interfaces for various functions on persistent arrays can be found in
the SATS file
prelude/SATS/arrayref.sats,
which is automatically loaded by **atsopt**.

There are various functions in ATSLIB for array creation. For instance, the following two are commonly used:

fun{a:t@ype} arrayref_make_elt {n:nat} (asz: size_t n, elt: a):<!wrt> arrayref (a, n) // end of [arrayref_make_elt] fun{a:t@ype} arrayref_make_listlen {n:int} (xs: list (a, n), n: int n):<!wrt> arrayref (a, n) // end of [arrayref_make_listlen]

For reading from and writing to an array, the function templates arrayref_get_at and arrayref_set_at can be used, respectively, which are assigned the following interfaces:

fun{a:t@ype} arrayref_get_at {n:int} (A: arrayref (a, n), i: sizeLt (n)):<!ref> a fun{a:t@ype} arrayref_set_at {n:int} (A: arrayref (a, n), i: sizeLt (n), x: a):<!ref> void

As an example, the following function template reverses the content of a given array:

fun{a:t@ype} arrayref_reverse{n:nat} ( A: arrayref (a, n), n: size_t (n) ) : void = let // fun loop {i: nat | i <= n} .<n-i>. ( A: arrayref (a, n), n: size_t n, i: size_t i ) : void = let val n2 = half (n) in if i < n2 then let val tmp = A[i] val ni = pred(n)-i in A[i] := A[ni]; A[ni] := tmp; loop (A, n, succ(i)) end else () // end of [if] end // end of [loop] // in loop (A, n, i2sz(0)) end // end of [arrayref_reverse]

If the test i < n2 is changed to i <= n2, a type-error is to be reported. Why? The reason is that A[n-1-i] becomes out-of-bounds array subscripting in the case where n and i both equal zero. Given that it is very unlikely to encounter a case where an array of size 0 is involved, a bug like this, if not detected early, can be buried so scarily deep!

The careful reader may have already noticed that the sort t@ype is assigned to the template parameter a. In other words, the above implementation of arrayref_reverse cannot handle a case where the values stored in a given array are of some linear type. The reason for choosing the sort t@ype is that both arrayref_get_at and arrayref_set_at can only be applied to an array containing values of a nonlinear type. In the following implementation, the template parameter is given the sort vt@ype so that an array containing linear values, that is, values of some linear type can be handled:

fun{a:vt@ype} arrayref_reverse{n:nat} ( A: arrayref (a, n), n: size_t (n) ) : void = let // fun loop {i: nat | i <= n} .<n-i>. ( A: arrayref (a, n), n: size_t n, i: size_t i ) : void = let val n2 = half (n) in if i < n2 then let val () = arrayref_interchange (A, i, pred(n)-i) in loop (A, n, succ(i)) end else () // end of [if] end // end of [loop] // in loop (A, n, i2sz(0)) end // end of [arrayref_reverse]

The interface for the function template arrayref_interchange is given below:

fun{a:vt@ype} arrayref_interchange{n:int} (A: arrayref (a, n), i: sizeLt n, j: sizeLt n):<!ref> void // end of [arrayref_interchange]

There are various functions available for traversing an array from left to right or from right to left. Also, the following two functions can be conveniently called to traverse an array from left to right:

// fun{a:t0p} arrayref_head{n:pos} (A: arrayref (a, n)): (a) // A[0] fun{a:t0p} arrayref_tail{n:pos} (A: arrayref (a, n)): arrayref (a, n-1) // overload .head with arrayref_head overload .tail with arrayref_tail //

fun{a,b:t@ype} arrayref_foldleft{n:int} ( f: (a, b) -> a, x: a, A: arrayref (b, n), n: size_t(n) ) : a = ( if n > 0 then arrayref_foldleft<a,b> (f, f (x, A.head()), A.tail(), pred(n)) else x // end of [if] ) (* end of [arrayref_foldleft] *)

Please find on-line the entirety of the code used in this chapter.

I use the name *array-with-size* to refer to a persistent
array with attached size information. Given a viewtype VT, the type for an
array-with-size that contains N values of viewtype VT is
arrszref(VT, N). Essentially, such a value is a boxed pair of
two components of types arrayref(VT, N) and
size_t(N). The interfaces for various functions on persistent
arrays-with-size can be found in
prelude/SATS/arrayref.sats.

For creating an array-with-size, the following functions arrszref_make_arrpsz and arrszref_make_arrayref can be called:

fun{} arrszref_make_arrpsz {a:vt0p}{n:int} (arrpsz (INV(a), n)): arrszref(a) fun{} arrszref_make_arrayref {a:vt0p}{n:int} (arrayref (a, n), size_t(n)): arrszref(a) // end of [arrszref_make_arrayref]

For reading from and writing to an array-with-size, the function templates arrszref_get_at and arrszref_set_at can be used, respectively, which are assigned the following interfaces:

fun{a:t@ype} arrszref_get_at (A: arrszref (a), i: size_t): (a) fun{a:t@ype} arrszref_set_at (A: arrszref (a), i: size_t, x: a): void

As a simple example, the following code implements a function that reverses the content of the array inside a given array-with-size:

fun{a:t@ype} arrszref_reverse ( A: arrszref (a) ) : void = let // val n = A.size() val n2 = half (n) // fun loop (i: size_t): void = let in if i < n2 then let val tmp = A[i] val ni = pred(n)-i in A[i] := A[ni]; A[ni] := tmp; loop (succ(i)) end else () // end of [if] end // end of [loop] // in loop (i2sz(0)) end // end of [arrszref_reverse]

Arrays-with-size can be a good choice over arrays in a prototype implementation as it is often more demanding to program with arrays. Also, for programmers who are yet to become familiar with dependent types, it is definitely easier to work with arrays-with-size than arrays. When programming in ATS, I often start out with arrays-with-size and then replace them with arrays when I can see clear benefits from doing so.

Please find on-line the entirety of the code used in this chapter.

A persistent matrix of dimension m by n is just a persistent array of size m*n. Like in C, the representation of a matrix in ATS is row-major. In other words, element (i, j) in a matrix of dimension m by n is element i*n+j in the underlying array that represents the matrix.

Given a viewtype VT and two integers M and N, the type
matrixref(VT, M, N) is for persistent matrices of dimension M
by N that contain elements of the viewtype VT. There is no dimension
information attached to matrixref-values explicitly. The interfaces for various
functions on persistent matrices can be found in the SATS file
prelude/SATS/matrixref.sats, which is automatically loaded by
**atsopt**.

The following function is commonly used to create a matrixref-value:

fun{a:t0p} matrixref_make_elt{m,n:int} (m: size_t m, n: size_t n, x0: a):<!wrt> matrixref (a, m, n) // end of [matrixref_make_elt]

Also, the following cast function can be called to turn an array into a matrix:

castfn arrayref2matrixref {a:vt0p}{m,n:nat} (A: arrayref (a, m*n)):<> matrixref (a, m, n) // end of [arrayref2matrixref]

For accessing and updating the content of a matrix-cell, the following two functions matrixref_get_at and matrixref_set_at can be called:

// fun{a:t0p} matrixref_get_at {m,n:int} ( A: matrixref (a, m, n), i: sizeLt(m), n: size_t(n), j: sizeLt(n) ) :<!ref> (a) // end of [matrixref_get_at] // fun{a:t0p} matrixref_set_at {m,n:int} ( A: matrixref (INV(a), m, n), i: sizeLt (m), n: size_t n, j: sizeLt (n), x: a ) :<!refwrt> void // end of [matrixref_set_at] //

In the following presentation, I give an implementation of a function that turns a given square matrix into its transpose:

// extern fun{a:t0p} matrixref_transpose {n:nat} ( M: matrixref (a, n, n), n: size_t (n) ) : void // end of [matrixref_transpose] // implement{a} matrixref_transpose {n} (M, n) = let // macdef mget (i, j) = matrixref_get_at (M, ,(i), n, ,(j)) macdef mset (i, j, x) = matrixref_set_at (M, ,(i), n, ,(j), ,(x)) // fun loop {i,j:nat | i < j; j <= n } .<n-i,n-j>. ( i: size_t (i), j: size_t (j) ) : void = if j < n then let val x = mget(i, j) val () = mset(i, j, mget(j, i)) val () = mset(j, i, x) in loop (i, j+1) end else let val i1 = succ (i) in if i1 < n then loop (i1, succ(i1)) else () end // end of [if] // in if n > 0 then loop (i2sz(0), i2sz(1)) else () end // end of [matrixref_transpose]

Please find on-line the entirety of the code used in this chapter.

I use the name *matrix-with-size* to refer to a persistent
matrix with attached dimension information (that is, number of rows and
number of columns). Given a viewtype VT, the type for a matrix-with-size
that contains M rows and N columns of elements of viewtype VT is
mtrxszref(VT, M, N). Essentially, such a value is a boxed
record of three components of types arrayref(VT, N),
size_t(M) and size_t(N). The interfaces for various
functions on persistent matrices-with-size can be found in
prelude/SATS/matrixref.sats.

The following function is commonly used to create a matrix-with-size:

fun{a:t0p} mtrxszref_make_elt (m: size_t, n: size_t, x0: a): mtrxref (a) // end of [mtrxszref_make_elt]

For accessing and updating the content of a matrix-cell, the following two functions mtrxszref_get_at and mtrxszref_set_at can be called:

fun{a:t0p} mtrxszref_get_at (M: mtrxszref(a), i: size_t, j: size_t): (a) fun{a:t0p} mtrxszref_set_at (M: mtrxszref(a), i: size_t, j: size_t, x: a): void

As a simple example, the following code implements a function that transpose the content of the matrix inside a given matrix-with-size:

// extern fun{a:t0p} mtrxszref_transpose (M: mtrxszref (a)): void // implement{a} mtrxszref_transpose (M) = let // val n = M.nrow() // val ((*void*)) = assertloc (M.nrow() = M.ncol()) // fun loop ( i: size_t, j: size_t ) : void = if j < n then let val x = M[i,j] val () = M[i,j] := M[j,i] val () = M[j,i] := x in loop (i, succ(j)) end else let val i1 = succ (i) in if i1 < n then loop (i1, succ(i1)) else () end // end of [if] // in if n > 0 then loop (i2sz(0), i2sz(1)) else () end // end of [mtrxszref_transpose]

Like arrays-with-size, matrices-with-size are easier to program with than dependently typed matrices. However, the latter can not only lead to more effective error detection at compile-time but also more efficent code execution at run-time. For someone programming in ATS, it is quite reasonable to start out with matrices-with-size and then replace them with matrices when there are clear benefits from doing so.

Please find on-line the entirety of the code used in this chapter.

Hashtables are commonly used to implement finite maps. In ATSLIB/libats, there are hashtable implementations based on linear chaining and linear probing. There is also support for linear hashtables as well as persistent hashtables. The linear ones can be safely freed by the programmer, and the persistent ones (which are directly based on linear ones) can only be safely reclaimed through garbage collection (GC). In this chapter, I show how persistent hashtables can be created and operated on.

Suppose that a map is needed for mapping keys of type key_t to items of type itm_t. The following code essentially sets up an interface for creating and operating on such a map based on a hashtable implementation in ATSLIB/libats:

local typedef key = key_t and itm = itm_t in (* in-of-local *) #include "libats/ML/HATS/myhashtblref.hats" end // end of [local]

Assume that key_t is string and itm_t is int. The following line of code creates a hashtable with its initial capacity set to be 1000:

Note that the capacity in this case is the size of the array associated with the created hashtable. The underlying hashtable implementation is based on linear chaining, and this hashtable can store up to 5000 (5*1000) items without need for resizing. When resizing is indeed needed, it is done automatically. The following few lines insert some key/item pairs into mymap:// val-~None_vt() = mymap.insert("a", 0) val-~Some_vt(0) = mymap.insert("a", 1) // val-~None_vt() = mymap.insert("b", 1) val-~Some_vt(1) = mymap.insert("b", 2) // val-~None_vt() = mymap.insert("c", 2) val-~Some_vt(2) = mymap.insert("c", 3) //

// val () = mymap.insert_any("a", 0) val () = mymap.insert_any("b", 1) val () = mymap.insert_any("c", 2) val kxs = mymap.listize1((*void*)) val ((*void*)) = fprintln! (stdout_ref, "kxs = ", kxs) val kxs = mymap.takeout_all((*void*)) val ((*void*)) = fprintln! (stdout_ref, "kxs = ", kxs) // val () = assertloc (mymap.size() = 0) //

// extern fun myhashtbl_foreach_cloref ( tbl: myhashtbl , fwork: (key, &(itm) >> _) -<cloref1> void ) : void // end-of-function //

// val () = myhashtbl_foreach_cloref ( mymap , lam (k, x) => fprintln! (stdout_ref, "k=", k, " and ", "x=", x) ) (* myhashtbl_foreach_cloref *) //

Please find the entirety of the code used in this chapter on-line. Also, there is a hashtable-based implementation of symbol table available on-line.

Please see this article for a detailed explanation on tail-recursion and the support in ATS for turning tail-recursive calls into local jumps.

A higher-order function is one that takes another function as its argument. Let us use BT to range over base types such as int, bool, char, double and string. A simple type T is formed according to the following inductive definition:

BT is a simple type.

(T

_{1}, ..., T_{n}) -> T_{0}is a simple type if T_{0}, T_{1}, ... T_{n}are simple types.

Let *order* be a function from simple types to natural numbers
defined as follows:

*order*(BT) = 0*order*((T_{1}, ..., T_{n}) -> T_{0}) =*max*(*order*(T_{0}), 1 +*order*(T_{1}), ..., 1 +*order*(T_{n}))

Given a function f of some simple type T, let us say that f is a
*n*th-order function if *order*(T) =
*n*. For instance, a function of the type (int, int) -> int
is 1st-order, and a function of the type int -> (int -> int) is also
1st-order, and a function of the type ((int -> int), int) -> int is
2nd-order. In practice, most functions are 1st-order and most higher-order
functions are 2nd-order.

As an example, let us implement as follows a 2nd-order function find_root that takes as its only argument a function f from integers to integers and searches for a root of f by enumeration:

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

As another example, let us implement as follows the famous Newton-Raphson's method for finding roots of functions on reals:

typedef fdouble = double -<cloref1> double // macdef epsilon = 1E-6 (* precision *) // // [f1] is the derivative of [f] // fun newton_raphson ( f: fdouble, f1: fdouble, x0: double ) : double = let fun loop ( f: fdouble, f1: fdouble, x0: double ) : double = let val y0 = f x0 in if abs (y0 / x0) < epsilon then x0 else let val y1 = f1 x0 in loop (f, f1, x0 - y0 / y1) end // end of [if] end // end of [loop] in loop (f, f1, x0) end // end of [newton_raphson]

// square root function fn sqrt (c: double): double = newton_raphson (lam x => x * x - c, lam x => 2.0 * x, 1.0) // cubic root function fn cbrt (c: double): double = newton_raphson (lam x => x * x * x - c, lam x => 3.0 * x * x, 1.0)

Higher-order functions can be of great use in supporting a form of code sharing that is both common and flexible. As function arguments are often represented as heap-allocated closures that can only be reclaimed through garbage collection (GC), higher-order functions are used infrequently, if at all, in a setting where GC is not present. In ATS, linear closures, which can be freed explictly in a safe manner, are available to support higher-order functions in the absence of GC, making it possible to employ higher-order functions extensively in systems programming (where GC is unavailable or simply disallowed). The details on linear closures are to be given elsewhere.

Please find on-line the entirety of the code used in this chapter.

While the core of ATS is based on call-by-value evaluation, there is also direct support in ATS for lazy (that is, call-by-need) evaluation.

There is a special language construct $delay for delaying or suspending the evaluation of an expression (by forming a thunk), and there is also a special function lazy_force for resuming a suspended evaluation (represented by a thunk). The abstract type constructor lazy of the sort (t@ype) => type forms a (boxed) type when applied to a type. Given an expression exp of type T, the value $delay(exp) of the type lazy(T) represents the suspended evaluation of exp. Given a value V of the type lazy(T) for some type T, calling lazy_force on V resumes the suspended evaluation represented by V. If the call returns, then the returned value is of type T. The interface for the function template lazy_force is given as follows:

where the symbol !laz indicates a form of effect associated with lazy-evaluation. Note that the special prefix operator ! in ATS is overloaded with lazy_force.In prelude/SATS/stream.sats, the following types stream_con and stream are declared mutually recursively for representing lazy streams:

datatype stream_con (a:t@ype+) = | stream_nil of ((*void*)) | stream_cons of (a, stream(a)) where stream (a:t@ype) = lazy (stream_con(a))

The following code gives a standard implementation of the sieve of Eratosthenes:

// fun from (n: int): stream (int) = $delay (stream_cons (n, from (n+1))) // fun sieve ( ns: stream(int) ) :<!laz> stream(int) = $delay let // // [val-] means no warning message from the compiler // val-stream_cons(n, ns) = !ns in stream_cons (n, sieve (stream_filter_cloref<int> (ns, lam x => x mod n > 0))) end // end of [$delay let] // end of [sieve] // val thePrimes = sieve(from(2)) //

The function template stream_filter_cloref is of the following interface:

fun{a:t@ype} stream_filter_cloref (xs: stream(a), pred: a -<cloref> bool):<!laz> stream(a) // end of [stream_filter_cloref]

Let us see another example of lazy evaluation. The follow code demonstrates an interesting approach to computing the Fibonacci numbers:

// val _0_ = $UNSAFE.cast{int64}(0) val _1_ = $UNSAFE.cast{int64}(1) // val // the following values are defined mutually recursively rec theFibs_0 : stream(int64) = $delay (stream_cons(_0_, theFibs_1)) // fib0, fib1, ... and theFibs_1 : stream(int64) = $delay (stream_cons(_1_, theFibs_2)) // fib1, fib2, ... and theFibs_2 : stream(int64) = // fib2, fib3, fib4, ... ( stream_map2_fun<int64,int64><int64> (theFibs_0, theFibs_1, lam (x, y) => x + y) ) (* end of [val/and/and] *) //

fun{ a1,a2:t0p}{b:t0p } stream_map2_cloref ( xs1: stream (a1), xs2: stream (a2), f: (a1, a2) -<fun> b ) :<!laz> stream (b) // end of [stream_map2_cloref]

Let us see yet another example of lazy evaluation. A Hamming number is a positive natural number whose prime factors can contain only 2, 3 and 5. The following code shows a straightforward way to generate a stream consisting of all the Hamming numbers:

// val compare_int_int = lam (x1: int, x2: int): int =<fun> compare(x1, x2) // macdef merge2 (xs1, xs2) = stream_mergeq_fun<int> (,(xs1), ,(xs2), compare_int_int) // val rec theHamming : stream(int) = $delay ( stream_cons(1, merge2(merge2(theHamming2, theHamming3), theHamming5)) ) (* end of [theHamming] *) and theHamming2 : stream(int) = stream_map_fun<int><int> (theHamming, lam x => 2 * x) and theHamming3 : stream(int) = stream_map_fun<int><int> (theHamming, lam x => 3 * x) and theHamming5 : stream(int) = stream_map_fun<int><int> (theHamming, lam x => 5 * x) //

fun{a:t0p} stream_mergeq_fun ( xs1: stream (a), xs2: stream (a), (a, a) -<fun> int ) :<!laz> stream (a) // end of [stream_mergeq_fun]

With stream-based lazy evaluation, an illusion of infinite data can be readily created. This illusion is given a simple programming interface plus automatic support for memoization, enabling a programming style that can often be both elegant and intriguing.

In general, it is difficult to estimate the time-complexity and space-complexity of a program based on lazy evaluation. This is regarded as a serious weakness. With linear stream-based lazy evalution, this weakness can essentially be removed.

Please find on-line the entirety of the code used in this chapter.

A linearly typed list in ATS is also referred to as a linear list, which essentially corresponds to a singly-linked list in C. The following linear datatype declaration introduces a linear type list_vt for linear lists:

// datavtype list_vt(a:vt@ype, int) = | list_vt_nil(a, 0) of () | {n:nat} list_vt_cons(a, n+1) of (a, list_vt(a, n)) //

The following function list_vt_length shows a typical way of handling a linear list in a read-only situation:

// fun {a:vt@ype} list_vt_length (xs: !list_vt(a, n)): int(n) = ( case+ xs of | list_vt_nil() => 0 | list_vt_cons(x, xs2) => 1 + list_vt_length<a> (xs2) ) //

The following function list_vt_foreach shows a typical way of modifying elements stored in a linear list:

// fun {a:vt@ype} list_vt_foreach ( xs: !list_vt(a, n) , fwork: (&(a) >> _) -<cloref1> void ) : void = ( case+ xs of | list_vt_nil() => () | @list_vt_cons(x, xs2) => (fwork(x); list_vt_foreach<a> (xs2, fwork); fold@(xs)) ) //

// fun {a:vt@ype} list_vt_append {m,n:nat} ( xs: list_vt(a, m), ys: list_vt(a, n) ) : list_vt(a, m+n) = let // fun loop{m:nat} ( xs: &list_vt(a, m) >> list_vt(a, m+n), ys: list_vt(a, n) ) : void = ( case+ xs of | ~list_vt_nil() => (xs := ys) | @list_vt_cons(x, xs2) => (loop(xs2, ys); fold@(xs)) ) // in case+ xs of | ~list_vt_nil () => ys | @list_vt_cons (x, xs2) => (loop(xs2, ys); fold@(xs); xs) end // end of [list_vt_append] //

The following function list_vt_free frees a given linear list containing non-linear elements:

// fun {a:vt@ype} list_vt_free {n:nat} ( xs: list_vt(a?, n) ) : void = ( case+ xs of | ~list_vt_nil() => () | ~list_vt_cons(x, xs2) => list_vt_free<a> (xs2) ) //

Please find on-line the entirety of the code used in this chapter plus some testing code.

**Table of Contents**- 25. Extvar-Declaration
- 26. Linear Closure-Functions
- 27. Stack-Allocated Closure-Functions
- 28. Automatic Code Generation
- 29. Linear Stream-Based Lazy Evaluation

ATS puts great emphasis on interacting with other programming languages.

Suppose that I have in some C code a (global) integer variable of the name foo and I want to increase in some ATS code the value stored in foo by 1. This can be done as follows:

val x0 = $extval(int, "foo") // get the value of foo val p_foo = $extval(ptr, "&foo") // get the address of foo val () = $UNSAFE.ptr_set<int> (p_foo, x0 + 1) // update foo

As for another example, let us suppose that foo2 is a record variable that contains two integer fields named first and second. Then the following code assigns integers 1 and 2 to these two fields of foo2:

By its very nature, the feature of extvar-declaration is inherently unsafe, and it should only be used with caution.Please find on-line the entirety of the code presented in this chapter.

A closure-function is a boxed record that contains a pointer to an envless function plus bindings that map certain names in the body of the envless function to values. In practice, a function argument of a higher-order function is often a closure-function (instead of an envless function). For instance, the following higher-order function list_map_cloref takes a closure-function as its second argument:

fun{ a:t@ype}{b:t@ype } list_map_cloref{n:int} (xs: list (a, n), f: (a) -<cloref> b): list_vt (b, n)

Closure-functions can be either linear or non-linear, and linear ones can be explicitly freed in a safe manner. The keyword -<cloref> is used to form a type for non-linear closure-functions. As a variant of list_map_cloref, the following higher-order function list_map_cloptr takes a linear closure-function as its second argument:

fun{ a:t@ype}{b:t@ype } list_map_cloptr{n:int} (xs: list (a, n), f: !(a) -<cloptr> b): list_vt (b, n)

A typical example making use of list_map_cloptr is given as follows:

fun foo{n:int} ( x0: int, xs: list (int, n) ) : list_vt (int, n) = res where { // val f = lam (x) =<cloptr> x0 + x val res = list_map_cloptr (xs, f) val () = cloptr_free ($UNSAFE.cast{cloptr(void)}(f)) // } (* end of [foo] *)

There is also some interesting interaction between currying and linear closure-functions. In functional programming, currying means turning a function taking multiple arguments simutaneously into a corresponding one that takes these arguments sequentially. For instance, the function acker2 in the following code is a curried version of the function acker, which implements the famous Ackermann function (that is recursive but not primitive recursive):

fun acker(m:int, n:int): int = ( case+ (m, n) of | (0, _) => n + 1 | (m, 0) => acker (m-1, 1) | (_, _) => acker (m-1, acker (m, n-1)) ) (* end of [acker] *) fun acker2 (m:int) (n:int): int = acker (m, n)

It is also possible to define a curried version of acker as follows:

While the evaluation of acker3(3)(4) yields the same result as acker2(3)(4), the compiler of ATS (ATS/Postiats) inserts code that automatically frees the linear closure-function generated from evaluating acker3(3) after the evaluation of acker3(3)(4) finishes.In ATS1, linear closure-functions play a pivotal role in supporting programming with higher-order functions in the absence of GC. Due to advanced support for templates in ATS2, the role played by linear closure-functions in ATS1 is greatly diminished. However, if closure-functions need to be stored in a data structure but GC is unavailable or undesirable, then using linear closure-functions can lead to a solution that avoids the risk of generatig memory leaks at run-time.

Please find on-line the entirety of the code used in this chapter.

Higher-order functions are a very convenient programming feature for supporting certain forms of code reuse. Often a function passed as an argument to a higher-order function call is a closure-function created on heap at run-time, and it is most likely of no more use after the call. If the closure-function is linear, then it needs to be freed explicitly by the programmer (or a type-error would occur during typechecking). If the closure-function is non-linear, then its memory should be reclaimed through garbage-collection (GC) (or the memory is leaked).

Creating heap-allocated closure-functions implies the need for dynamic memory allocation (DMA). In a restricted environment (e.g., one for embedded programming), DMA may not be (fully) supported. One option for constructing a closure-function in the absence of support for DMA is to store it in the stack-frame of the calling function, and there is special systax in ATS for doing so.

Let us see a concrete example of stack-allocated closure. The following code implements a higher-order function template:

// fun {res:t@ype} ifold{n:nat} ( n: int(n) , fopr: (res, natLt(n)) -<cloref1> res, ini: res ) : res = let // fun loop {i:nat | i <= n} .<n-i>. (i: int(i), res: res): res = if i < n then loop(i+1, fopr(res, i)) else res // in loop(0, ini) end // end of [ifold] //

// typedef res = double // fun dotprod {n:nat} ( n: int(n) , A: arrayref(res, n) , B: arrayref(res, n) ) : res = ( ifold<res>(n, lam(res, i) => res + A[i]*B[i], 0.0) ) //

// fun dotprod {n:nat} ( n: int(n) , A: arrayref(res, n) , B: arrayref(res, n) ) : res = let // var fopr = lam@(res: res, i: natLt(n)): res => res + A[i]*B[i] // in ifold<res>(n, $UNSAFE.cast(addr@fopr), 0.0) end // end of [dotprod] //

In order to remove the (unsafe) cast in the implementation of dotprod, we need to implement a slight variant of ifold as follows:

// fun {res:t@ype} ifold_{n:nat} ( n: int(n) , fopr: &(res, natLt(n)) -<clo1> res, ini: res ) : res = let // fun loop {i:nat | i <= n} .<n-i>. ( i: int(i) , fopr: &(res, natLt(n)) -<clo1> res, res: res ) : res = if i < n then loop(i+1, fopr, fopr(res, i)) else res // end of [if] // in loop(0, fopr, ini) end // end of [ifold_] // (* ****** ****** *) // fun dotprod_ {n:nat} ( n: int(n) , A: arrayref(res, n) , B: arrayref(res, n) ) : res = let // var fopr = lam@(res: res, i: natLt(n)): res => res + A[i]*B[i] // in ifold_<res>(n, fopr, 0.0) end // end of [dotprod_] //

Please find on-line the entirety of the code used in this chapter plus some testing code.

In practice, one often encounters a need to write boilerplate code or code that tends to follow certain clearly recognizable patterns. It is commonly seen that meta-programming (of various forms) is employed to automatically generate such code, thus not only increasing programming productivity but also potentially eliminating bugs that would otherwise be introduced due to manual code construction.

In the following presentation, I am to show that the ATS compiler can be directed to generate the code for certain functions on values of a declared datatype. Following is the datatype used for illustration:

// datatype expr = | Int of int | Var of string | Add of (expr, expr) | Sub of (expr, expr) | Mul of (expr, expr) | Div of (expr, expr) | Ifgtz of (expr, expr, expr) // if expr > 0 then ... else ... | Ifgtez of (expr, expr, expr) // if expr >= 0 then ... else ... //

Given a datatype, its datcon-function is the one that takes a value of the datatype and then returns a string representing the name of the (outmost) constructor in the construction of the value. We can use the following directive to indicate (to the ATS compiler) that the datcon-function for the datatype expr needs to be generated:

By default, the name of the generated function is datcon_expr. If a different name is needed, it can be supplied as the third argument of the #codegen2-directive. For instance, the following directive indicates that the generated function is of the given name my_datcon_expr: Assume that a file of the name(* ****** ****** *) // implement {}(*tmp*) datcon_expr (arg0) = ( case+ arg0 of | Int _ => "Int" | Var _ => "Var" | Add _ => "Add" | Sub _ => "Sub" | Mul _ => "Mul" | Div _ => "Div" | Ifgtz _ => "Ifgtz" | Ifgtez _ => "Ifgtez" ) // (* ****** ****** *)

Please find on-line the entirety of this presented example plus a Makefile (for illustrating the code generation process).

A datcontag-function is very similar to a datcon-function. Given a datatype, its datcontag-function is the one that takes a value of the datatype and then returns the tag (which is a small integer) assigned to the (outmost) constructor in the construction of the value. We can use the following directive to indicate (to the ATS compiler) that the datcontag-function for the datatype expr needs to be generated:

By default, the name of the generated function is datcontag_expr. If a different name is needed, it can be supplied as the third argument of the #codegen2-directive. For instance, the following directive indicates that the generated function is of the given name my_datcontag_expr: The following ATS code is expected to be generated that implements datcontag_expr:(* ****** ****** *) // implement {}(*tmp*) datcontag_expr (arg0) = ( case+ arg0 of | Int _ => 0 | Var _ => 1 | Add _ => 2 | Sub _ => 3 | Mul _ => 4 | Div _ => 5 | Ifgtz _ => 6 | Ifgtez _ => 7 ) // (* ****** ****** *)

Please find on-line the entirety of this presented example plus a Makefile (for illustrating the code generation process).

A fprint-function takes a file-handle (of the type FILEref) and a value and then outputs a text representation of the value to the file-handle. Given a datatype, one is often in need of a function that can output certain kind of text representation for values of this datatype. For instance, such a function can be of great use in debugging.

Let us first declare a function template fprint_expr as follows:

We can then use the directive below to indicate (to the ATS compiler) that the fprint-function for the datatype expr needs to be generated: The third argument of the codegen2-directive can be omitted in this case as it coincides with the default. The generated code that implements fprint_expr is listed as follows:(* ****** ****** *) // extern fun{} fprint_expr$Int: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Var: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Add: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Sub: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Mul: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Div: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez: $d2ctype(fprint_expr<>) // (* ****** ****** *) // implement{} fprint_expr (out, arg0) = ( case+ arg0 of | Int _ => fprint_expr$Int<>(out, arg0) | Var _ => fprint_expr$Var<>(out, arg0) | Add _ => fprint_expr$Add<>(out, arg0) | Sub _ => fprint_expr$Sub<>(out, arg0) | Mul _ => fprint_expr$Mul<>(out, arg0) | Div _ => fprint_expr$Div<>(out, arg0) | Ifgtz _ => fprint_expr$Ifgtz<>(out, arg0) | Ifgtez _ => fprint_expr$Ifgtez<>(out, arg0) ) // (* ****** ****** *) // extern fun{} fprint_expr$sep: (FILEref) -> void implement{} fprint_expr$sep(out) = fprint(out, ",") // extern fun{} fprint_expr$lpar: (FILEref) -> void implement{} fprint_expr$lpar(out) = fprint(out, "(") // extern fun{} fprint_expr$rpar: (FILEref) -> void implement{} fprint_expr$rpar(out) = fprint(out, ")") // extern fun{a:t0p} fprint_expr$carg: (FILEref, INV(a)) -> void implement{a} fprint_expr$carg(out, arg) = fprint_val<a>(out, arg) // (* ****** ****** *) // extern fun{} fprint_expr$Int$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Int$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Int$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Int$arg1: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Int(out, arg0) = { // val () = fprint_expr$Int$con<>(out, arg0) val () = fprint_expr$Int$lpar<>(out, arg0) val () = fprint_expr$Int$arg1<>(out, arg0) val () = fprint_expr$Int$rpar<>(out, arg0) // } implement{} fprint_expr$Int$con(out, _) = fprint(out, "Int") implement{} fprint_expr$Int$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Int$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Int$arg1(out, arg0) = let val-Int(arg1) = arg0 in fprint_expr$carg(out, arg1) end // extern fun{} fprint_expr$Var$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Var$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Var$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Var$arg1: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Var(out, arg0) = { // val () = fprint_expr$Var$con<>(out, arg0) val () = fprint_expr$Var$lpar<>(out, arg0) val () = fprint_expr$Var$arg1<>(out, arg0) val () = fprint_expr$Var$rpar<>(out, arg0) // } implement{} fprint_expr$Var$con(out, _) = fprint(out, "Var") implement{} fprint_expr$Var$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Var$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Var$arg1(out, arg0) = let val-Var(arg1) = arg0 in fprint_expr$carg(out, arg1) end // extern fun{} fprint_expr$Add$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Add$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Add$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Add$sep1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Add$arg1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Add$arg2: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Add(out, arg0) = { // val () = fprint_expr$Add$con<>(out, arg0) val () = fprint_expr$Add$lpar<>(out, arg0) val () = fprint_expr$Add$arg1<>(out, arg0) val () = fprint_expr$Add$sep1<>(out, arg0) val () = fprint_expr$Add$arg2<>(out, arg0) val () = fprint_expr$Add$rpar<>(out, arg0) // } implement{} fprint_expr$Add$con(out, _) = fprint(out, "Add") implement{} fprint_expr$Add$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Add$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Add$sep1(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Add$arg1(out, arg0) = let val-Add(arg1, _) = arg0 in fprint_expr$carg(out, arg1) end implement{} fprint_expr$Add$arg2(out, arg0) = let val-Add(_, arg2) = arg0 in fprint_expr$carg(out, arg2) end // extern fun{} fprint_expr$Sub$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Sub$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Sub$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Sub$sep1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Sub$arg1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Sub$arg2: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Sub(out, arg0) = { // val () = fprint_expr$Sub$con<>(out, arg0) val () = fprint_expr$Sub$lpar<>(out, arg0) val () = fprint_expr$Sub$arg1<>(out, arg0) val () = fprint_expr$Sub$sep1<>(out, arg0) val () = fprint_expr$Sub$arg2<>(out, arg0) val () = fprint_expr$Sub$rpar<>(out, arg0) // } implement{} fprint_expr$Sub$con(out, _) = fprint(out, "Sub") implement{} fprint_expr$Sub$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Sub$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Sub$sep1(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Sub$arg1(out, arg0) = let val-Sub(arg1, _) = arg0 in fprint_expr$carg(out, arg1) end implement{} fprint_expr$Sub$arg2(out, arg0) = let val-Sub(_, arg2) = arg0 in fprint_expr$carg(out, arg2) end // extern fun{} fprint_expr$Mul$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Mul$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Mul$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Mul$sep1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Mul$arg1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Mul$arg2: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Mul(out, arg0) = { // val () = fprint_expr$Mul$con<>(out, arg0) val () = fprint_expr$Mul$lpar<>(out, arg0) val () = fprint_expr$Mul$arg1<>(out, arg0) val () = fprint_expr$Mul$sep1<>(out, arg0) val () = fprint_expr$Mul$arg2<>(out, arg0) val () = fprint_expr$Mul$rpar<>(out, arg0) // } implement{} fprint_expr$Mul$con(out, _) = fprint(out, "Mul") implement{} fprint_expr$Mul$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Mul$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Mul$sep1(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Mul$arg1(out, arg0) = let val-Mul(arg1, _) = arg0 in fprint_expr$carg(out, arg1) end implement{} fprint_expr$Mul$arg2(out, arg0) = let val-Mul(_, arg2) = arg0 in fprint_expr$carg(out, arg2) end // extern fun{} fprint_expr$Div$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Div$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Div$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Div$sep1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Div$arg1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Div$arg2: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Div(out, arg0) = { // val () = fprint_expr$Div$con<>(out, arg0) val () = fprint_expr$Div$lpar<>(out, arg0) val () = fprint_expr$Div$arg1<>(out, arg0) val () = fprint_expr$Div$sep1<>(out, arg0) val () = fprint_expr$Div$arg2<>(out, arg0) val () = fprint_expr$Div$rpar<>(out, arg0) // } implement{} fprint_expr$Div$con(out, _) = fprint(out, "Div") implement{} fprint_expr$Div$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Div$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Div$sep1(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Div$arg1(out, arg0) = let val-Div(arg1, _) = arg0 in fprint_expr$carg(out, arg1) end implement{} fprint_expr$Div$arg2(out, arg0) = let val-Div(_, arg2) = arg0 in fprint_expr$carg(out, arg2) end // extern fun{} fprint_expr$Ifgtz$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz$sep1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz$sep2: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz$arg1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz$arg2: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtz$arg3: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Ifgtz(out, arg0) = { // val () = fprint_expr$Ifgtz$con<>(out, arg0) val () = fprint_expr$Ifgtz$lpar<>(out, arg0) val () = fprint_expr$Ifgtz$arg1<>(out, arg0) val () = fprint_expr$Ifgtz$sep1<>(out, arg0) val () = fprint_expr$Ifgtz$arg2<>(out, arg0) val () = fprint_expr$Ifgtz$sep2<>(out, arg0) val () = fprint_expr$Ifgtz$arg3<>(out, arg0) val () = fprint_expr$Ifgtz$rpar<>(out, arg0) // } implement{} fprint_expr$Ifgtz$con(out, _) = fprint(out, "Ifgtz") implement{} fprint_expr$Ifgtz$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Ifgtz$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Ifgtz$sep1(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Ifgtz$sep2(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Ifgtz$arg1(out, arg0) = let val-Ifgtz(arg1, _, _) = arg0 in fprint_expr$carg(out, arg1) end implement{} fprint_expr$Ifgtz$arg2(out, arg0) = let val-Ifgtz(_, arg2, _) = arg0 in fprint_expr$carg(out, arg2) end implement{} fprint_expr$Ifgtz$arg3(out, arg0) = let val-Ifgtz(_, _, arg3) = arg0 in fprint_expr$carg(out, arg3) end // extern fun{} fprint_expr$Ifgtez$con: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez$lpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez$rpar: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez$sep1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez$sep2: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez$arg1: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez$arg2: $d2ctype(fprint_expr<>) extern fun{} fprint_expr$Ifgtez$arg3: $d2ctype(fprint_expr<>) // implement{} fprint_expr$Ifgtez(out, arg0) = { // val () = fprint_expr$Ifgtez$con<>(out, arg0) val () = fprint_expr$Ifgtez$lpar<>(out, arg0) val () = fprint_expr$Ifgtez$arg1<>(out, arg0) val () = fprint_expr$Ifgtez$sep1<>(out, arg0) val () = fprint_expr$Ifgtez$arg2<>(out, arg0) val () = fprint_expr$Ifgtez$sep2<>(out, arg0) val () = fprint_expr$Ifgtez$arg3<>(out, arg0) val () = fprint_expr$Ifgtez$rpar<>(out, arg0) // } implement{} fprint_expr$Ifgtez$con(out, _) = fprint(out, "Ifgtez") implement{} fprint_expr$Ifgtez$lpar(out, _) = fprint_expr$lpar(out) implement{} fprint_expr$Ifgtez$rpar(out, _) = fprint_expr$rpar(out) implement{} fprint_expr$Ifgtez$sep1(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Ifgtez$sep2(out, _) = fprint_expr$sep<>(out) implement{} fprint_expr$Ifgtez$arg1(out, arg0) = let val-Ifgtez(arg1, _, _) = arg0 in fprint_expr$carg(out, arg1) end implement{} fprint_expr$Ifgtez$arg2(out, arg0) = let val-Ifgtez(_, arg2, _) = arg0 in fprint_expr$carg(out, arg2) end implement{} fprint_expr$Ifgtez$arg3(out, arg0) = let val-Ifgtez(_, _, arg3) = arg0 in fprint_expr$carg(out, arg3) end // (* ****** ****** *)

implement fprint_expr$Add$con<> (_, _) = () implement fprint_expr$Add$sep1<> (out, _) = fprint! (out, "+")

After proper adaptation is done, one can introduce a (non-template) function as follows:

// extern fun my_fprint_expr(FILEref, expr): void implement my_fprint_expr (out, x) = fprint_expr<> (out, x) //

Please find on-line the entirety of this presented example plus a Makefile (for illustrating the code generation process).

In ATS, there is also support for lazy evaluation based on linear streams. As far as I can tell, linear stream-based lazy evaluation is currently a unique language feature of ATS.

In practice, it is most likely that (non-linear) stream-based lazy evaluation requires the support of garbage collection (GC). As the behavior of GC can in general be very difficult to predict, lazy evaluation may not be suitable in a setting where great precision in control is needed. With linear stream-based lazy evaluation, the need for GC to reclaim values representing streams is eliminated as such values can be explicitly freed in a safe manner.

There is a special language construct $ldelay for delaying or suspending the evaluation of an expression (by forming a linear thunk), and there are also a pair of special functions lazy_vt_force and lazy_vt_free for resuming and freeing, respectively, a suspended evaluation (represented by a linear thunk). Unlike delay, $ldelay applies to two expressions to form a linear lazy stream; the first expression is the one whose evaluation is suspended; the second expression is the one whose evaluation results in all the linear values contained in the first expression being freed.

The abstract type constructor lazy_vt of the sort (vt@ype) => vtype forms a (boxed) viewtype when applied to a viewtype. Given two expressions exp1 of some type T and exp2 of the type void, the value $ldelay(exp1, exp2) is of the type lazy_vt(T); calling lazy_vt_force on $ldelay(exp1, exp2) resumes the suspended evaluation of exp1; calling lazy_vt_free on $ldelay(exp1, exp2) initiates the evaluation of exp2 (to free linear values contained in exp1).

The interface for the function template lazy_vt_force is given as follows:

Note that the special prefix operator ! in ATS is overloaded with lazy_vt_force.The interface for the function lazy_vt_free is given as follows:

Note that the special prefix operator ~ in ATS is overloaded with lazy_vt_free.In prelude/SATS/stream_vt.sats, the following viewtypes stream_vt_con and stream_vt are declared mutually recursively for representing linear lazy streams:

datavtype stream_vt_con (a:vt@ype+) = | stream_vt_nil of ((*void*)) | stream_vt_cons of (a, stream_vt(a)) where stream_vt (a:vt@ype) = lazy_vt (stream_vt_con(a))

The following code gives an implementation of the sieve of Eratosthenes in which a linear stream of all the prime numbers is constructed:

// fun from (n: int): stream_vt (int) = $ldelay (stream_vt_cons (n, from (n+1))) // fun sieve ( ns: stream_vt(int) ) : stream_vt(int) = $ldelay ( let // // [val-] means no warning message from the compiler // val ns_con = !ns val-@stream_vt_cons(n, ns1) = ns_con val n = n val ns1_ = ns1 val ((*void*)) = ns1 := sieve (stream_vt_filter_cloptr<int> (ns1_, lam x => x mod n > 0)) prval ((*void*)) = fold@(ns_con) in ns_con end // end of [let] , ~ns // [ns] is freed ) (* end of [$ldelay] *) // end of [sieve] // val thePrimes = sieve(from(2)) //

The function template stream_vt_filter_cloptr is given the following interface:

fun{a:t0p} stream_vt_filter_cloptr (xs: stream_vt (a), pred: (&a) -<cloptr> bool): stream_vt (a) // end of [stream_vt_filter_cloptr]

Please find on-line the entirety of the code used in this chapter. One can readily use a tool like valgrind to verify that the implementation given above leaks no memory.