ATS Trustful Software, Inc.

Copyright © 2010-201? Hongwei Xi

As a programming language, ATS is both syntax-rich and feature-rich. This book introduces the reader to some core features of ATS, including basic functional programming, simple types, (recursively defined) datatypes, polymorphic types, dependent types, linear types, theorem-proving, programming with theorem-proving (PwTP), and template-based programming. Although the reader is not assumed to be familiar with programming in general, the book is likely to be rather dense for someone without considerable programming experience.

To Jinning, Zoe, and Chloe.

**Table of Contents**- Preface
- I. Basic Functional Programming
- 1. Preparation for Starting
- 2. Elements of Programming
- 3. Functions
- Functions as a Simple Form of Abstraction
- Function Arity
- Function Interface
- Evaluation of Function Calls
- Recursive Functions
- Evaluation of Recursive Function Calls
- Example: Coin Changes for Fun
- Tail-Call and Tail-Recursion
- Example: The Eight-Queens Puzzle
- Mutually Recursive Functions
- Mutually Defined Tail-Recursion
- Envless Functions and Closure-Functions
- Higher-Order Functions
- Example: Binary Search for Fun
- Example: A Higher-Order Fun Puzzle
- Currying and Uncurrying

- 4. Datatypes
- 5. Parametric Polymorphism

- II. Support for Practical Programming
- III. Programming with Dependent Types
- IV. Programming with Views and Viewtypes
- V. Programming with Function Templates

ATS is a statically
typed programming language that unifies implementation with formal
specification. Within ATS, there are two sublanguages: one for
specification and the other for implementation, and there is also a
theorem-proving subsystem for verifying whether an implementation indeed
implements according to its specification. If I could associate only one
single word with ATS, I would choose the word
*precision*. Programming in ATS is about being precise
and being able to effectively enforce precision. This point will be
demonstrated concretely and repeatedly in this book.

In order to be precise in building software systems, we need to specify what such a system is expected to accomplish. In the current day and age, software specification, which is used in a rather loose sense here, is often done in forms of varying degrees of formalism, ranging from verbal discussions to pencil/paper drawings to diagrammatic depictions in modeling languages such as UML to text descriptions in formal specification languages such as VDM and Z. Often the main purpose of software specification is to establish some mutual understanding among a team of developers. After the specification for a software system is done, either formally or informally, we need to implement the specification in a programming language. In general, it is exceedingly difficult to be reasonably certain whether an implementation actually meets its specification. Even if the implementation coheres well with its specification initially, it nearly inevitably diverges from the specification as the software system evolves. The dreadful consequences of such a divergence are all too familiar; the specification becomes less and less reliable for understanding the behavior of the software system while the implementation gradually turns into its own specification; for the developers, it becomes increasingly difficult and risky to maintain and extend the software system; for the users, it requires increased amount of time and effort to learn and use the software system.

Largely inspired by Martin-Loef's constructive type theory, which was originally developed for the purpose of establishing a foundation for mathematics, I designed ATS in an attempt to combine specification and implementation into a single programming language. There are a static component (statics) and a dynamic component (dynamics) in ATS. Intuitively, the statics and dynamics are each for handling types and programs, respectively. In particular, specification is done in the statics. Given a specification, how can we then effectively ensure that an implementation of the specification (type) indeed implements according to the specification? We request that the programmer who does the implementation also construct a proof in the theorem-proving subsystem of ATS to demonstrate it. This is a style of program verification that puts the programmer at the center, and thus we refer to it as a programmer-centric approach to program verification.

As a programming language, ATS is both syntax-rich and feature-rich. It can support a variety of programming paradigms, including functional programming, imperative programming, object-oriented programming, concurrent programming, modular programming, etc. However, the core of ATS, which is based on a call-by-value functional language, is surprisingly simple, and this is where the journey of programming in ATS starts. In this book, I will demonstrate primarily through examples how various programming features in ATS can be employed effectively to facilitate the construction of high-quality programs. I will focus on programming practice instead of programming theory. If you are primarily interested in the type-theoretical foundation of ATS, then you have to find it elsewhere.

If you can implement, then you are a good programmer. In order to be a better programmer, you should also be able to explain what you implement. If you can guarantee what is implemented matches what is specified, then you are surely the best programmer. Hopefully, learning ATS will put you on a wonderful exploring journey to become the best programmer. Let that journey start now!

**Table of Contents**- 1. Preparation for Starting
- 2. Elements of Programming
- 3. Functions
- 4. Datatypes
- 5. Parametric Polymorphism

It is likely that you want to write programs in the programming language you are learning. You may also want to try some of the examples included in this book and see what really happens. So I will first show you how to write in ATS a single-file program, that is, a program contained in a single file, and compile it and then execute it.

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

The keyword val initiates a binding between the variable _ (underscore) and the function call print("Hello, world!\n"). However, this binding is never used after it is introduced; its sole purpose is for the call to the print function to get evaluated.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:

which indicates that main0 is a nullary function, that is, a function taking no arguments, and it returns no value (or it returns the void value). The double slash symbol (//) initiates a comment that terminates at the end of the current line.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:

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 you program in this section // (* ****** ****** *) implement main0 () = () // a dummy implementation for [main]

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] ######

The core of ATS is a call-by-value functional programming language. I will
explain the meaning of *call-by-value* in a moment. As
for functional programming, there is really no precise definition. The
most important aspect of functional programming that I want to explore is
the notion of binding, which relates names to expressions.

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.

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:

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:

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:

The error message reported in this case indicates that the name (or dynamic identifier) x in the expression x + 1 is unbound. In particular, the two occurrences of x in the above code are unrelated.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:

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:

where the bindings introduced between the keywords local and in are effective until the keyword end is reached. Note that the bindings introduced between the keywords in and end are themselves toplevel bindings. The difference between let and local should be clear: The former is used to form an expression while the latter is used to introduce a sequence of declarations.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:

We start with the empty environment ENV0; we evaluate 3.14 to itself and 10.0 * 10.0 to 100.0 under the environment ENV0; we then extend ENV0 to ENV1 with two bindings mapping PI to 3.14 and radius2 to 100.0; we then evaluate PI * radius2 under ENV1 to 3.14 * radius2, then to 3.14 * 100.0, and finally to 314.0, which is the value of the let-expression.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.

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.

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:

Note that the constructed tuple can be assigned the tuple type (char, int, double). Another method for selecting components in a given tuple is based on pattern matching, which is employed in the following example: Note that (x, y, z) is a pattern that can match any tuples of exact 3 components. I will say more about pattern matching elsewhere.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:

Note that a space is needed between '( and 'A' for otherwise the current parser (for ATS/Postiats) would be confused.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.

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:

where x and y are the names of the two fields in a record value of this type. We also refer to a field in a record as a component. The special symbol @{ indicates that the formed type is for flat/native/unboxed records. A value of the type point2D is constructed as follows and given the name theOrigin: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:

Alternatively, we can use pattern matching for doing component extraction as is done in the next line of code: In this case, the names theOrigin_x and theOrigin_y are bound to the components in theOrgin that are named x and y, respectively. If we only need to extract out a selected few of components (instead of all the available ones), we can make use of the following kind of patterns: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.

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

where if, then and else are keywords in ATS. In a conditional expression, the expression following if is the test and the expressions following then and else are referred to as the then-branch and the else-branch (of the conditional expression), respectively.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:

which is equivalent to the following conditional expression: Note that () stands for the void value (of the type void). If a type can be assigned to a conditional expression in the truncated form, then the type must be void.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:

Evaluating this sequence expression prints out (onto the console) the 5-letter string "Hello". Instead of parentheses, we can also use the keywords begin and end to form a sequence expression: If we like, we may also add a semicolon immediately after the last expression in a sequence as long as the last expression is of the type void. For instance, the above example can also be written as follows: I also want to point out the following style of sequencing: which is quite common in functional programming.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 play a foundational role in programming. While it may be theoretically possible to program without functions (but with loops), such a programming style is of little practical value. ATS does provide some language constructs for implementing for-loops and while-loops directly. I, however, strongly recommend that the programmer implement loops as recursive functions or more precisely, as tail-recursive functions. This is a programming style that matches well with more advanced programming features in ATS, which will be presented in this book later.

The code employed for illustration in this chapter plus some additional code for testing is available on-line.

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:

Now suppose that we have found a more efficient way to do squaring. In order to take full advantage of it, we need to modify each occurrence of squaring in the current program accordingly. This style of programming is clearly not modular, and it is of little chance to scale. To address this problem, we can implement a function as follows to compute the square of a given floating point number: The keyword fn initiates the definition of a non-recursive function, and the name following it is for the function to be defined. In the above example, the function square takes one argument of the name x, which is assumed to have the type double, and returns a value of the type double. The expression on the right-hand side (RHS) of the symbol = is the body of the function, which is x * x in this case. If we have a more efficient way to do squaring, we can just re-implement the body of the function square accordingly to take advantage of it, and there is no other changes needed (assuming that squaring is solely done by calling square).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:

where the RHS of the symbol = is a lambda-expression representing an anonymous function that takes one argument of the type double and returns a value of the type double, and the expression following the symbol => is the body of the function. If we wish, we can change the name of the function argument as follows: This is called alpha-renaming (of function arguments), and the new lambda-expression is said to be alpha-equivalent to the original one.
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_{1} and exp_{2} can be assigned
the types T1 and T2, then the function application
exp(exp_{1}, exp_{2}), 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:

Note that the subtraction and multiplication functions are of the type (double, double) -> double and square is of the type (double) -> double. It is thus a simple routine to verify that the body of area_of_ring can be assigned the type double.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:

We can define a unary function sqrsum2 as follows:// 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.

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:

where arg1 and arg2 may be replaced with any other legal identifiers for function arguments. For functions of more or fewer arguments, interfaces can be written in a similar fashion. For instance, we have the following interfaces for various functions on integers: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

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:

We first evaluate the argument of the call to ~1.0 under ENV0; we then extend ENV0 to ENV1 with a binding between x and ~1.0 and start to evaluate the body of abs under ENV1; we evaluate the test x >= 0 to ~1.0 >= 0 and then to false, which indicates that we take the else-branch ~x to continue; we evaluate ~x to ~(~1.0) and then to 1.0; so the evaluation of the function call abs(0.0 - 1.0) returns 1.0.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:

To find out the sum of all the integers ranging from 1 to n, we call sum1 (n). The reduction strategy for sum1 (n) is straightforward: If n is greater than 1, then we can readily find the value of sum1 (n) by solving a simpler problem, that is, finding the value of sum1 (n-1).We can also solve the problem by implementing the following recursive function sum2 that sums up all the integers in a given range:

This time, we call sum2 (1, n) in order to find out the sum of all the integers ranging from 1 to n. The reduction strategy for sum2 (m, n) is also straightforward: If m is less than n, then we can readily find the value of sum2 (m, n) by solving a simpler problem, that is, finding the value of sum2 (m+1, n). The reason for sum2 (m+1, n) being simpler than sum2 (m, n) is that m+1 is closer to n than m is.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:

It should be noted that the division involved in the expression (m+n)/2 is integer division for which rounding is done by truncation.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:

Suppose that we are to evaluate fib(2) under some environment ENV0. Given that 2 is already a value, we extend ENV0 to ENV1 with a binding between n and 2 and start to evaluate the body of fib under ENV1; clearly, this evaluation leads to the evaluation of fib(n-1) + fib(n-2); it is easy to see that evaluating fib(n-1) and fib(n-2) under ENV1 leads to 1 and 0, respectively, and the evaluation of fib(n-1) + fib(n-2) eventually returns 1 (as the result of 1+0); thus the evaluation of fib(2) under ENV0 yields the integer value 1.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).

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

_{1}, x) + cc(S, x-c), where S_{1}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.

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:

where the outer recursive call is a self tail-call while the inner one is not.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.

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:

After this declaration, each occurrence of the name N is to be replaced with 8. For representing board configurations, we define a type int8 as follows: A value of the type int8 is a tuple of 8 integers where the first integer states the column position of the queen piece on the first row (row 0), and the second integer states the column position of the queen piece on the second row (row 1), and so on.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.

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)

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.

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.

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 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.

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.

Let us first introduce a type definition as follows:

Given a type T, I(T) is for a closure-function that maps a given input value of type T to an output value of the same type T. Given a function f of type I(T), we can compose f with itself to form another function, which just applies f twice to a given argument. The following function template twice does precisely the described function composition: Let us now take a look at some interesting code involving twice that is also likely to be puzzling:// 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, 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.

The feature of datatypes in ATS in largely taken from ML.

A datatype is like a tagged union type. For each datatype, there are some constructors associated with it, and these constructors are needed for constructing values of the datatype. As an example, the following syntax declares a datatype named intopt:

There are two constructors associated with intopt: intopt_none, which is nullary, and intopt_some, which is unary. For instance, intopt_none() and intopt_some(1) are two values of the type intopt. In order for accessing components in such values, a mechanism often referred to as pattern-matching is provided in ATS. I will demonstrate through examples that datatypes plus pattern matching can offer not only great convenience in programming but also clarity in code.The code employed for illustration in this chapter plus some additional code for testing is available on-line.

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 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.

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.

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]

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:

When applied to a character and a value of the type charlst, the constructor charlst_cons forms a value of the type charlst. As an example, the following value represents a character list consisting of 'a', 'b' and 'c': We can define a function charlst_length as follows to compute the length of a given character list: Note that this implementation is recursive but not tail-recursive. By relying on the commutativity and associativity of integer addition, we can give the following implementation of charlst_length that is tail-recursive: Note that the naming convention I follow closely in this book (and elsewhere) mandates that only a tail-recursive function be given a name indicative of its being a loop. A non-tail-recursive function is not called a loop because it cannot be translated directly to a loop in an imperative programming language like C.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.

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:

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.

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]

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.

Code sharing is of paramount importance in programming. In a typed
programming language, we often encounter a situation where the same
functionality is needed for values of different types. For instance, we may
need to compute the length of a list while the elements in the list can be
characters, integers, strings, etc. Evidently, we want to avoid
implementing a list-length function for each element type as it would
probably be the worst form of code duplication. We want to implement one
single function that can be applied to any list to compute the length of
the list. This list-length function parameterizes over the element type of
a given list, and it behaves uniformly regardless what the element type is.
This is a form of code sharing that is often referred to as
*parametric polymorphism*, which should be distinguished from
other forms of polymorphism such as inheritance polymorphism in
object-oriented programming.

The code employed for illustration in this chapter plus some additional code for testing is available on-line.

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:

where the template parameters are given sequentially (instead of simultaneously). The following code shows how swap2 can be instantiated to form instances: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.

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:

The type variables a and b are often referred as static arguments while xy is a dynamic argument. For example, the following code makes use of the polymorphic function swap_boxed: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:

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:

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.

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

More precisely, list0 is a type constructor. Given a type T, we can form a type list0(T) for lists consisting of elements of the type T. For instance, list0(char) is for character lists, list0(int) for integer lists, list0(list0(int)) for lists whose elements are themselves integer lists, etc. To a great extent, the need for function templates or polymorphic functions largely stems from the availability of polymorphic datatypes. As an example, a function template list0_length is implemented as follows for computing the length of any given list: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:

A typical use of option0 is to perform some kind of error-handling. Suppose that we are to implement a function doing integer division and we want to make sure that the function returns even if it is called in a case where the divisor equals 0. This can be done as follows: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]

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.

Given two lists xs and ys of the type list0(T) for some type T, list0_append(xs, ys) returns a list that is the concatenation of xs and ys:

Clearly, this implementation of list0_append is not tail-recursive.Given two lists xs and ys of the type list0(T) for some type T, list0_reverse_append(xs, ys) returns a list that is the concatenation of the reverse of xs and ys:

Clearly, this implementation of list0_reverse_append is tail-recursive.Given a list xs of the type list0(T1) for some type T1 and a closure function f0 of the type T1 -<cloref1> T2 for some type T2, list0_map(xs, f0) returns a list ys of the type list0(T2):

The length of ys equals that of xs and each element y in ys equals f0(x), where x is the corresponding element in xs. Clearly, this implementation of list0_map is not tail-recursive.Given xs, ini and f0, list0_foldleft(ini, xs, f0) computes the value of the expression f0(... f0(f0(ini, xs[0]), xs[1]) ..., xs[n-1]), where n is the length of xs and xs[i] refers to element i in xs for each i < n. The following implementation of list0_foldleft is tail-recursive:

Given xs, res and f0, list0_foldright(xs, res, f0) computes the value of the expression f0(xs[0], f0(xs[1], f0(... f0(xs[n-1], res) ...))), where n is the length of xs and xs[i] refers to element i in xs for each i < n. The following implementation of list0_foldright is not tail-recursive:

Given two lists xs and ys of the types list0(T1) and list0(T2) for some types T1 and T2, respectively, list0_zip(xs, ys) returns a list zs of the type list0(@(T1, T2)):

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]

Given two lists xs and ys of the types list0(T1) and list0(T2) for some types T1 and T2, respectively, and a closure function f of the type (T1, T2) -<cloref1> T3 for some type T3, list0_zipwith(xs, ys, f0) returns a list zs of the type list0(T3):

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] *)

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

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.

**Table of Contents**- 6. Effectful Programming Features
- 7. Modularity
- 8. Interaction with C

Effectful programming features are those that can generate effects at run-time. But what is really an effect? The answer to this question is rather complex as it depends on the model of evaluation. I will gradually introduce various kinds of effects in this book. In sequential programming, that is, constructing programs to be evaluated sequentially (in contrast to concurrently), an expression is effectless if there exists a value such that the expression and the value cannot be distinguished as far as evaluation is concerned. For instance, the expression 1+2 is effectless as it cannot be distinguished from the value 3. An effectless expression is also said to be pure. On the other hand, an effectful expression is one that can be distinguished from any given values. For instance, the expression print("Hello") is effectful as its evaluation results in an observable behavior that distinguishes the expression from any values. In this case, print("Hello") is said to certain I/O effect. If the evaluation of an expression never terminates, then the expression is also effectul. For instance, let us define a function loop as follows:

Then the expression loop() can be distinguished from any values in the following context: If the hole [] in the context is replaced with loop(), then the evaluation of the resulting expression continues forever. If the hole [] is replaced with any value, then the evaluation leads to the string "Terminated" being printed out. The expression loop is said to contain non-termination effect.I will cover programming features related to exceptional control-flow, persistent memory storage and simple I/O in this chapter, which are all of common use in practical programming.

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:

The constructor FatalError0 is nullary while the constructor FatalError1 is unary. Exception values, that is, values of the type exn can be formed by applying exception constructors to proper arguments. For instance, FatalError0() and FatalError1("division-by-zero") are two exception values (or simply exceptions). In the following program, a function for integer division is implemented: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.

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.

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.

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.

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]

I myself think that the above counter implementation is of rather a poor style. It is also possible to protect the integrity of a state by simply making it abstract. I will present elsewhere another counter implementation based on a linear abstract type (that is, abstract viewtype in ATS), where counters can be created and then safely freed.

I mentioned earlier that a reference is just an array of size 1. I would now like to state that an array of size n is just n references allocated consecutively. These references can also be called cells, and they are numbered from 0 until n-1, inclusive.

Given an array of size n, an integer is a valid index for this array if it is a natural number strictly less than n. Otherwise, the integer is out of the bounds of the array. For an array named A, the expression A[i] means to fetch the content of the cell in A that is numbered i if i is a valid index for A. The expression A[i] can also be used as a left value. For instance, the assignment (A[i] := exp) means to evaluate exp to a value and then store the value into the cell in A that is numbered i if i is a valid index.

What happens if the index i in A[i] is invalid, that is, it is out of the bounds of the array A? In this case, A[i] is referred to as out-of-bounds array subscription and evaluating A[i] leads to a raised exception where the exception is ArraySubscriptExn(). One simple and reliable way to tell whether an integer is a valid index for a given array is to compare it with the size of the array at run-time. Given a type T, the type arrszref(T) is for an array paired with its size in which elements of the type T are stored. I will loosely refer to values of the type arrszref(T) as arrays from now on. In case there is a clear need to avoid potential confusion, I may also refer to them as array0-values.

Various functions and function templates on array0-values are declared in
the file arrayref.sats,
which is automatically loaded by **atsopt**. For instance,
three function templates and one polymorphic function on arrays are
depicted by the following interfaces:

// fun{a:t@ype} // template arrszref_make_elt (asz: size_t, x: a): arrszref a // array creation // // polymorphic fun: // fun arrszref_get_size {a:t@ype}(A: arrszref a): size_t // size of an array // fun{a:t@ype} // template arrszref_get_elt_at(A: arrszref a, i: size_t): a // A[i] // fun{a:t@ype} // template arrszref_set_elt_at(A: arrszref a, i: size_t, x: a): void // A[i] := x //

Like in C, there are many types of integer values in ATS. The type size_t is essentially for unsigned long integers. The functions for converting between the type int and the type size_t are g0int2uint_int_size and g0uint2int_size_int. Given a type T and two values asz and init of the types size_t and T, respectively, arrszref_make_elt<T> (asz, init) returns an array of the type arrszref(T) such that the size of the array is asz and each cell in the array is initialized with the value init. Given an array A of the type arrszref(T) for some T, arrszref_get_size(A) returns the size of A, which is of the type size_t. For convenience, arrszref_get_size(A) can be written as A.size(). As for array access and update, the functions arrszref_get_elt_at and arrszref_set_elt_at can be called. For convenience, the bracket notation can be used to call these functions.

In the following program, the function template insertion_sort implements the standard insertion sort on arrays:

fun{ a:t@ype } insertion_sort ( A: arrszref(a) , cmp: (a, a) -> int ) : void = loop(1) where { fun ins ( x: a, i: int ) :<cloref1> void = if i >= 0 then ( if cmp(x, A[i]) < 0 then (A[i+1] := A[i]; ins(x, i-1)) else (A[i+1] := x) // end of [if] ) else A[0] := x // end of [if] // end of [ins] val asz = g0uint2int_size_int(A.size()) // end of [val] fun loop(i: int):<cloref1> void = if i < asz then (ins(A[i], i-1); loop(i+1)) else () // end of [loop] } (* end of [insertion_sort] *)

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

Given a natural number n, we want to print out all the permutations consisting of integers ranging from 1 to n, inclusive. In addition, we want to print them out according to the lexicographic ordering on integer sequences. For instance, we want the following output to be generated when n is 3:

Let us first define a function as follows for printing out an array of integers:

fun print_intarray (A: arrszref(int)): void = loop(0, ", ") where { // val asz = g0uint2int_size_int(A.size()) // // The integers are to be separated by the string [sep] // fun loop (i: int, sep: string): void = if i < asz then (if i > 0 then print sep; print A[i]; loop(i+1, sep)) // end of [if] } (* end of [print_intarray] *)

We next implement two functions lrotate and rrotate for rearranging the elements in a given integer array:

fun lrotate ( A: arrszref int, i: int, j: int ) : void = let fun lshift ( A: arrszref int, i: int, j: int ) : void = if i < j then (A[i] := A[i+1]; lshift(A, i+1, j)) // end of [if] in if i < j then let val tmp = A[i] in lshift(A, i, j); A[j] := tmp end // end of [if] end // end of [lrotate] fun rrotate ( A: arrszref int, i: int, j: int ) : void = let fun rshift ( A: arrszref int, i: int, j: int ) : void = if i < j then (A[j] := A[j-1]; rshift(A, i, j-1)) // end of [if] in if i < j then let val tmp = A[j] in rshift(A, i, j); A[i] := tmp end // end of [if] end // end of [rrotate]

Given a natural number n, the following defined function permute prints out all the permutations consisting of integers ranging from 1 to n, inclusive while arranging the output according to the lexicographic ordering on integer sequences.

fun permute ( n: int ) : void = aux(1) where { // #define i2sz g0int2uint_int_size // // Creating array A of size n // val A = arrszref_make_elt<int>(i2sz(n), 0) // // Initializing A // with integers from 1 to n, inclusive // val () = init(0) where { fun init(i: int): void = if i < n then (A[i] := i+1; init(i+1)) // end of [if] } // end of [where] // end of [val] // fun aux (i: int): void = ( if i <= n then aux2(i, i) else ( print_intarray(A); print_newline() ) (* end of [else] *) ) (* end of [aux] *) // and aux2 (i: int, j: int): void = ( if j <= n then let val () = ( rrotate(A, i-1, j-1); aux(i+1); lrotate(A, i-1, j-1) ) // end of [val] in aux2 (i, j + 1) end // end of [if] ) (* end of [aux2] *) // } (* end of [permute] *)

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

A matrix in ATS is just a two-dimensional array but it is represented by a one-dimensional array and the representation is of the row-major style (in contrast to the column-major style). Given a type T, the type mtrxszref(T) is for a matrix combined with its number of rows and number of columns such that each element stored in the matrix is of the type T. I will loosely refer to values of the type mtrxszref(T) as matrices from now on. If there is a clear need to avoid potential confusion, I may also refer to them as matrix0-values.

Given a matrix M of dimension m by n, the expression M[i,j] means to fetch the content of the cell in M that is indexed by (i, j), where i and j are natural numbers strictly less than m and n, respectively. The expression M[i,j] can also be used as a left value. For instance, the assignment (M[i,j] := exp) means to evaluate exp to a value and then store the value into the cell in M that is indexed by (i, j).

Various functions and function templates on matrix0-values are declared in
the file matrixref.sats,
which is automatically loaded by **atsopt**. For instance,
three function templates and two polymorphic functions on matrices are
depicted by the following interfaces:

// fun{a:t@ype} mtrxszref_make_elt // template (row: size_t, col: size_t, x: a): mtrxszref (a) // fun mtrxszref_get_nrow{a:t@ype}(M: mtrxszref a): size_t // polyfun fun mtrxszref_get_ncol{a:t@ype}(M: mtrxszref a): size_t // polyfun // fun{a:t@ype} mtrxszref_get_elt_at // template (M: mtrxszref a, i: size_t, j: size_t): a // M[i,j] fun{a:t@ype} mtrxszref_set_elt_at // template (M: mtrxszref a, i: size_t, j: size_t, x: a): void // M[i,j] := x //

Given a type T and three values nrow, ncol and init of the types size_t, size_t and T, respectively, mtrxszref_make_elt<T> (row, col, init) returns a matrix of the type mtrxszref(T) such that the dimension of the matrix is nrow by ncol and each cell in the matrix is initialized with the value init. Given a matrix M of the type mtrxszref(T) for some T, mtrxszref_get_nrow(M) and mtrxszref_get_ncol(M) return the number of rows and the number of columns of M, respectively, which are both of the type size_t. For convenience, mtrxszref_get_nrow(M) and mtrxszref_get_ncol(M) can also be written as M.nrow and M.ncol, respectively. As for matrix access and update, the function templates mtrxszref_get_elt_at and mtrxszref_set_elt_at can be called, respectively. For convenience, bracket notation can used for these functions.

Let us now take a look at an example. The following defined function mtrxszref_transpose turns a given matrix into its transpose:

fun{a:t@ype} mtrxszref_transpose (M: mtrxszref a): void = let // val nrow = mtrxszref_get_nrow(M) // fnx loop1 (i: size_t): void = if i < nrow then loop2(i, 0) else () // and loop2 (i: size_t, j: size_t): void = if j < i then let val tmp = M[i,j] in M[i,j] := M[j,i]; M[j,i] := tmp; loop2(i, j+1) end else loop1(i+1) // end of [if] // in loop1 (0) end // end of [mtrxszref_transpose]

I present as follows a Monte Carlo approach to estimating the constant Pi, the ratio of the circumference of a circle over its diameter.

Assume that we have a square of the dimension N by N, where N is a relatively large natural number (e.g., 1000), and a disk of radius 1 that is contained in the square. Let N2 stand for N*N, that is, the square of N. If we randomly choose a point inside the square, then the probability for the point to hit the disk is Pi/N2.

The experiment we use to estimate the constant Pi can be described as follows. Given a natural number K, let us randomly choose K points inside the square in K rounds. In each round, we choose exactly one point. If the point chosen in round k hits on the disk centered at a previously chosen point, then we record one hit. Clearly, the expected number of hits recorded in round k is (k-1)*Pi/N2 as k-1 points have already being chosen in the previous rounds. Therefore, in K rounds, the expected total number of hits is (K*(K-1)/2)*Pi/N2. If K is fixed to be N2, then the expected total number of hits is (N2-1)*Pi/2. It can be proven that the total number of hits divided by N2 converges to Pi/2 (with probability 1) as N approaches infinity.

If we implement the above experiment directly based on the given description, the time-complexity of the implementation is evidently proportional to N2*N2 as the time spent in round k is proportional to k, where k ranges from 1 to N2. An implementation as such is simply impractical for handling N around the order 1000 (and thus N2 around the order of 1,000,000). To address the issue, we can impose a grid on the square, dividing it into N2 unit squares (of the dimension 1 by 1). We then associate with each unit square a list of chosen points that are inside it. In each round, we first choose a point randomly inside the original square; we next locate the unit square that contains this point; we then only search the lists associated with the unit square or any of its neighbors to count the number of hits generated by the point chosen in this round as this point cannot hit any disks centered at points that are not on these lists. As each unit square can have at most 8 neighbors and the average length of the list associated with each square is less than 1 during the experiment, the time spent during each round is O(1), that is, bounded by a constant. Hence, the time taken by the entire experiment is O(N2).

An implementation that precisely matches the above description plus some testing code is available on-line.

Handling I/O in ATS properly requires the availability of both dependent types and linear types, which I will cover elsewhere. In this section, I only present a means for allowing the programmer to access certain very basic I/O functionalities.

A file handle essentially associates a stream (of bytes) with a file identifier (represented as an integer). In ATS, the type for file handles is FILEref. There are three standard file handles, which are listed as follows:

stdin_ref: standard input

stdout_ref: standard output

stderr_ref: standard error output

Various functions on file handles are declared in the file
filebas.sats, which is
automatically loaded by **atsopt**. For instance, the
functions for opening and closing file handles have the following
interfaces:

fun fileref_open_exn ( path: string, fm: file_mode ) : FILEref // endfun fun fileref_close(fil: FILEref): void

The type file_mode is for values representing file modes, which are listed as follows:

file_mode_r: opening a file for reading and positioning the associated stream at the beginning of the file.

file_mode_rr: opening a file for both reading and and writing and positioning the associated stream at the beginning of the file.

file_mode_w: truncating a given file to zero length or creating a new one for writing and positioning the associated stream at the beginning of the file.

file_mode_ww: truncating a given file to zero length or creating a new one for both reading and writing and positioning the associated stream at the beginning of the file.

file_mode_a: opening a file for writing and positioning the associated stream at the end of the file.

file_mode_aa: opening a file for both reading and writing and positioning the associated stream at the beginning of the file for reading and at the end for writing.

As an example, the following short program opens a file handle, outputs the string "Hello, world!" plus a newline into the stream associated with the file handle and then closes the file handle:

implement main0 () = { // val out = fileref_open_exn("hello.txt", file_mode_w) val () = fprint_string(out, "Hello, world!\n") val () = fileref_close(out) // } (* end of [main0] *)

Another common I/O function is given the following interface:

The function fileref_get_line_string reads a line from the stream associated with a given file handle, and it returns a value of the type Strptr1. For the moment, I will simply say that such a value is just like a string except that it needs to be freed explicitly. As an example, the following short program echos onto the standard output each line read from the standard input:implement main0 ( // argumentless ) = loop() where { // fun loop(): void = let val isnot = fileref_isnot_eof(stdin_ref) // end of [val] in // if isnot then let val line = fileref_get_line_string(stdin_ref) val ((*void*)) = fprintln!(stdout_ref, line) val ((*void*)) = strptr_free(line) in loop((*void*)) end else ((*loop exits as the end-of-file is reached*)) // end (* end of [loop] *) // } (* end of [main0] *)

Generally speaking, modularity in programming means to organize programs in a modular fashion so that they each can be constructed in a relatively isolated manner and then be combined to function coherently. I will introduce in this section some features in ATS that are largely designed to facilitate program organization.

The interface for a function or value specifies a type that any implementation of the function or value should possess. For instance, the following code defines a function fact for computing the factorial of a given integer:

It is also possible to first declare an interface for fact as follows: where extern is a keyword in ATS that initiates the declaration of an interface. Alternative ways to declare an interface for fact are given as follows: If fact is declared to be a function, then it is required to be applied when occurring in code. If it is declared to be a value, there is no such a restriction.A function interface can be considered as a form of specification. For instance, the above interface for fact specifies that fact is a function that takes one argument required to be an integer and returns a value guaranteed to be an integer. What is so special about this form of specification is that it is formally enforced in ATS through typechecking: Any well-typed implementation of fact in ATS must possess the interface declared for it. Of course, this interface for fact is not a precise specification as there are (infinitely) many functions that can be given the same interface. This kind of imprecision can, however, be reduced or even eliminated, sometimes. After dependent types are introduced, I will present an interface for fact such that any implementation of the interface is guaranteed to implement precisely the factorial function as is defined by the following two equations:

fact(0) = 1

fact(n) = n * fact (n-1) for each natural number n > 0

An implementation for fact as the following one can be given at any point where the declared interface for fact is accessible:

The keyword implement is for initiating an implementation of a function or value whose interface is already declared. It is fairly common to see the following style of coding, usually, by a beginning ATS programmer: While this implementation can pass typechecking, it is nonetheless of a poor style: The types provided by the programmer for the argument and the result of fact are redundant as they can be automatically synthesized by the typechecker.As an example of an interface for a value, fact10 is declared as follows to be a value of the type int:

The following implementation for fact10 can be given at any point where the declared interface for fact10 is accessible:As another example, the following code declares an interface for a polymorphic function named swap_boxed:

Note that both type variables a and b are boxed. An implementation for swap_boxed is given as follows: The syntax {a,b} is for passing static arguments a and b to swap_boxed simultaneously. As neither a nor b is actually used in the body of swap_boxed, it is allowed to drop {a,b} in this case.As yet another example, the following code declares an interface for a function template named swap_tmplt:

Note that both type variables a and b are of the sort t@ype, indicating that they can be of any size. An implementation for swap_tmplt is given as follows:It is a standard practice for a programmer to first design interfaces for the functions to be supported in a package before actually implementing any of these functions. When such interfaces are available, application programs can be constructed to test whether the interface design makes sense or is convenient for practical use. Please remember that a superb implementation of a poor design cannot make the design any better. Therefore, testing a design before actually implementing it is often of vital importance. This is especially true if the involved design is complex.

The first letters in the ATS filename extensions *sats* and
*dats* refer to the words *static* and
*dynamic*, respectively. For instance, `foo.sats` is
a name for a static file while `bar.dats` is for a dynamic
one. A static file is often referred to as a SATS-file, and it usually
contains interface declarations for functions and values, datatype
declarations, type definitions, etc. The primary purpose of a SATS-file is
for allowing its content to be shared among various other ATS files, either
static or dynamic.

Let us now go through a simple example to see a typical use of static
files. Suppose that we want to implement the Ackermann's function, which is
famous for being recursive but not primitive recursive. In a static file
named `acker.sats` (or any other legal filename), we can declare
the following function interface:

staload "acker.sats" implement acker (m, n) = if m > 0 then if n > 0 then acker (m-1, acker (m, n-1)) else acker (m-1, 1) else n+1 // end of [acker]

It is also possible to give the following implementation for the declared function acker:

staload ACKER = "acker.sats" implement $ACKER.acker (m, n) = acker (m, n) where { fun acker (m: int, n:int): int = if m > 0 then if n > 0 then acker (m-1, acker (m, n-1)) else acker (m-1, 1) else n+1 } // end of [$ACKER.acker]

In another file named `test_acker.dats`, let us
write the following code:

// #include "share/atspre_staload.hats" // staload "acker.sats" dynload "acker.dats" implement main0 () = () where { // // acker (3, 3) should return 61 // val () = assertloc (acker (3, 3) = 61) } // end of [main0]

The simplest way to compile the two files `acker.dats` and
`test_acker.dats` is to issue the following command-line:

If we want to, we can also merge `acker.sats` and
`acker.dats` into a single filename of the following content:

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

Interfaces for function templates are mostly similar to those for functions. For example, the following syntax declares an interface in a dynamic file for a function template of the name list0_fold_left:

where t0p is a shorthand for t@ype.If the same interface is declared in a static file, the keyword extern should be dropped. Implementing an interface for a function template is also mostly similar to implementing one for a function. The above interface for list0_fold_left is given an implementation in the following code:

implement{a}{b} list0_fold_left (xs, f, init) = let // fun loop ( xs: list0 b, res: a ) : a = ( case+ xs of | list0_nil () => res | list0_cons (x, xs) => loop (xs, f (res, x)) ) (* end of [loop] *) // in loop (xs, init) end // end of [list0_fold_left]

extern fun {a,b:t0p}{c:t0p} app2 (f: (a, b) -<cloref1> c, x: a, y: b): c implement{a,b}{c} app2 (f, x, y) = f (x, y)

The style of template implementation presented in this section is referred to as generic template implementation. I will later present a different style of template implementation, which is often referred to as specific template implementation.

Implementing an interface for a function template specifically means to give an implementation for a fixed instance of the template. For instance, the following interface is for a function template of the name eq_elt_elt:

There is no meaningful generic implementation for eq_elt_elt as equality test for values of a type T depends on T. Two specific template implementations are given as follows for the instances eq_elt_elt<int> and eq_elt_elt<double>:implement eq_elt_elt<int> (x, y) = g0int_eq (x, y) implement eq_elt_elt<double> (x, y) = g0float_eq (x, y)

Let us now see a typical use of specific template implementation. The following defined function template listeq implements an equality function on lists:

fun{ a:t0p } listeq ( xs: list0 a , ys: list0 a ) : bool = ( case+ (xs, ys) of | (list0_cons (x, xs), list0_cons (y, ys)) => if eq_elt_elt<a> (x, y) then listeq (xs, ys) else false | (list0_nil (), list0_nil ()) => true | (_, _) => false ) (* end of [listeq] *)

As a comparison, the following defined function template listeqf also implements equality test on two given lists:

fun{ a:t0p } listeqf ( xs: list0 a , ys: list0 a , eq: (a, a) -> bool ) : bool = ( case+ (xs, ys) of | (list0_cons (x, xs), list0_cons (y, ys)) => if eq (x, y) then listeqf (xs, ys, eq) else false | (list0_nil (), list0_nil ()) => true | (_, _) => false ) (* end of [listeqf] *)

Please find the code presented in this section plus some additional testing code available on-line.

The name *abstract type* refers to a type such
that values of the type are represented in a way that is completely hidden
from users of the type. This form of information-hiding attempts to ensure
that changes to the implementation of an abstract type cannot introduce
type-errors into well-typed code that makes use of the abstract type. In
ATS as well as in many other programming languages, abstract types play a
pivotal role in support of modular programming. I will present as follows a
concrete example to illustrate a typical use of abstract types in
practice.

Suppose that we are to implement a package to provide various funtionalities on finite sets of integers. We first declare an abstract type intset as follows for values representing finite sets of integers:

The keyword abstype indicates that the declared abstract type intset is boxed, that is, the size of intset is the same as that of a pointer. There is a related keyword abst@ype for introducing unboxed abstract types, which will be explained elsewhere. We next present an interface for each function or value that we want to implement in the package:// empty set val intset_empty : intset // singleton set of [x] fun intset_make_sing (x: int): intset // turning a list into a set fun intset_make_list (xs: list0 int): intset // turning a set into a list fun intset_listize (xs: intset): list0 (int) // membership test fun intset_ismem (xs: intset, x: int): bool // computing the size of [xs] fun intset_size (xs: intset): size_t // adding [x] into [xs] fun intset_add (xs: intset, x: int): intset // deleting [x] from [xs] fun intset_del (xs: intset, x: int): intset // union of [xs1] and [xs2] fun intset_union (xs1: intset, xs2: intset): intset // intersection of [xs1] and [xs2] fun intset_inter (xs1: intset, xs2: intset): intset // difference between [xs1] and [xs2] fun intset_differ (xs1: intset, xs2: intset): intset

Usually, a realistic implementation for finite sets is based on some kind
of balanced trees (e.g., AVL trees, red-black trees). For the purpose of
illustration, I hereby give an implementation in which finite sets of
integers are represented as ordered lists of integers. This implementation
is contained in a file named `intset.dats`, which is available
on-line. In order to
construct values of an abstract type, we need to concretize it temporarily
by using the following form of declaration:

implement intset_union (xs1, xs2) = ( case+ (xs1, xs2) of | (list0_cons (x1, xs11), list0_cons (x2, xs21)) => let val sgn = compare (x1, x2) in case+ 0 of | _ when sgn < 0 => list0_cons{int}(x1, intset_union (xs11, xs2)) | _ when sgn > 0 => list0_cons{int}(x2, intset_union (xs1, xs21)) | _ (* sgn = 0 *) => list0_cons{int}(x1, intset_union (xs11, xs21)) // end of [case] end // end of [(cons, cons)] | (list0_nil (), _) => xs2 | (_, list0_nil ()) => xs1 ) (* end of [intset_union] *)

Let us represent a rational number as a pair of integers. If we declare a boxed abstract type rat for values representing rational numbers, then each value of the type rat is stored in heap-allocated memory, which can only be reclaimed through garbage collection (GC). Instead, we follow an alternative approach by declaring rat as an unboxed abstract type. Therefore, a declaration like the following one is expected:

The problem with this declaration is that it is too abstract. As there is not information given about the size of the type rat, the ATS compiler does not even know how much memory is needed for storing a value of the type rat. However, the programmer should not assume that such a form of declaration is useless. There are realistic circumstances where a declaration of this form can be of great importance, and this is a topic I will cover elsewhere. For now, let us declare an unboxed abstract type as follows: This declaration simply informs the ATS compiler that the representation for values of the type rat is the same as the one for values of the type (int, int). However, this information is not made available to the typechecker of ATS. In particular, if a value of the type rat is treated as a pair of integers in a program, then a type-error will surely occur.The following code is contained in a file named
`ratmod.sats`, which is available
on-line.

exception Denominator exception DivisionByZero fun rat_make_int_int (p: int, q: int): rat fun ratneg: (rat) -> rat // negation fun ratadd: (rat, rat) -> rat // addition fun ratsub: (rat, rat) -> rat // subtraction fun ratmul: (rat, rat) -> rat // multiplication fun ratdiv: (rat, rat) -> rat // division

implement rat_make_int_int (p, q) = let fun make ( p: int, q: int ) : rat = let val r = gcd (p, q) in (p / r, q / r) end // end of [make] // val () = if q = 0 then $raise Denominator // in if q > 0 then make (p, q) else make (~p, ~q) end // end of [rat_make_int_int]

implement ratneg (x) = (~x.0, x.1) implement ratadd (x, y) = rat_make_int_int (x.0 * y.1 + x.1 * y.0, x.1 * y.1) // end of [ratadd] implement ratsub (x, y) = rat_make_int_int (x.0 * y.1 - x.1 * y.0, x.1 * y.1) // end of [ratsub] implement ratmul (x, y) = rat_make_int_int (x.0 * y.0, x.1 * y.1) implement ratdiv (x, y) = ( if y.0 > 0 then rat_make_int_int (x.0 * y.1, x.1 * y.0) else $raise DivisionByZero() // end of [if] ) (* end of [ratdiv] *)

The previous package for rational numbers contains a serious limitation: The type for the integers employed in the representation of rational numbers is fixed to be int. If we ever want to represent rational numbers based on integers of a different type (for instance, lint for long integers or llint for long long integers), then we need to implement another package for rationals based on such integers. It is clearly advantageous to avoid this style of programming as it involves code duplication to a great extent.

The approach I employ in this section to implement a package for rational numbers that can address the aforementioned limitation follows the idea of functors in the programming language Standard ML (SML). Let us first introduce a type definition as follows:

typedef intmod (a:t@ype) = '{ ofint= int -> a , fprint= (FILEref, a) -> void , neg= (a) -> a // negation , add= (a, a) -> a // addition , sub= (a, a) -> a // subtraction , mul= (a, a) -> a // multiplication , div= (a, a) -> a // division , mod= (a, a) -> a // modulo operation , cmp= (a, a) -> int // comparison } // end of [intmod]

abst@ype rat(a:t@ype) = (a, a) typedef ratmod (a:t@ype) = '{ make= (a, a) -<cloref1> rat a , fprint= (FILEref, rat a) -<cloref1> void , numer= rat a -> a // numerator , denom= rat a -> a // denominator , neg= (rat a) -<cloref1> rat a // negation , add= (rat a, rat a) -<cloref1> rat a // addition , sub= (rat a, rat a) -<cloref1> rat a // subtraction , mul= (rat a, rat a) -<cloref1> rat a // multiplication , div= (rat a, rat a) -<cloref1> rat a // division , cmp= (rat a, rat a) -<cloref1> int // comparison } // end of [ratmod]

staload M = "libc/SATS/math.sats" val ratmod_int = let // val intmod_int = '{ ofint= lam (i) => i , fprint= lam (out, x) => $extfcall (void, "fprintf", out, "%i", x) , neg= lam (x) => ~x , add= lam (x, y) => x + y , sub= lam (x, y) => x - y , mul= lam (x, y) => x * y , div= lam (x, y) => x / y , mod= lam (x, y) => op mod (x, y) , cmp= lam (x, y) => compare (x, y) } : intmod (int) // end of [val] // in ratmod_make_intmod<int> (intmod_int) end // end of [val] val ratmod_dbl = let // val intmod_dbl = '{ ofint= lam (i) => g0i2f(i) , fprint= lam (out, x) => $extfcall (void, "fprintf", out, "%0.f", x) , neg= lam (x) => ~x , add= lam (x, y) => x + y , sub= lam (x, y) => x - y , mul= lam (x, y) => x * y , div= lam (x, y) => $M.trunc (x / y) // truncation , mod= lam (x, y) => $M.fmod (x, y) , cmp= lam (x, y) => compare (x, y) } : intmod (double) // end of [val] // in ratmod_make_intmod<double> (intmod_dbl) end // end of [ratmod_dbl]

ATS and C share precisely the same native/flat/unboxed data representation. As a consequence, there is no need for wrapping/unwrapping or boxing/unboxing when calling from C a function implemented in ATS or vice versa, and there is also no run-time overhead for doing so. To a large extent, ATS can be considered a front-end to C that is equipped with a highly expressive type system (for specifying program invariants) and a highly adaptable template system (for facilitating code reuse). In particular, ATS can often be effectively employed to turn a large task into subtasks of coherent interfaces, which can be implemented in ATS, C or some other langauges and then assembled together to form a solution to the orginal task.

As can be expected, C code that appears directly in ATS does not go through the kind of rigorous typechecking like ATS code should. So it is recommended that the programmer be extra cautious when making direct use of C code inside ATS code. In practice, my own experience clearly indicates that the portion of C code inside my ATS code is highly likely to be the culprit for most of encountered bugs.

A function declared in ATS can be given a global name of C-style so as to allow the function to appear in both ATS code and C code. In particular, the function can be implemented in ATS and called in C or vice versa.

In the following code, we see that two functions are declared:

The first function fact does not have a global name while the second function fact2 is assigned a global name fact2_in_c. The symbol ext# indicates that fact2_in_c is treated as a global function in C and its prototype needs to be declared (via the extern keyword) before it can be called. If ext# is written in place of ext#fact2_in_c in the above declaration, then the global name for the function fact2 in ATS is assumed to be same as the name of the function in ATS. In other words, writing ext# in the above declaration is equivalent to writing ext#fact2.Let us assume that fact can be implemented as follows:

When compiling this implementation, the ATS compiler needs to form function names in the generated C code to refer to fact and fact2. For the former, the function name in the C code is determined by a set of rules (which take into account the issue of namespace). For the latter, the function name is simply chosen to be the assigned global name fact2_in_c. As is suggested by the name of fact2_in_c, this function can be directly implemented in C as follows: It is also allowed to implement fact2 in ATS directly as is shown below: This implementation of fact2 can be called in C through the name fact2_in_c.If both fact2 and fact2_in_c are implemented (the former in ATS and the latter in C), then a link-time error is to be issued to indicate that fact2_in_c is implemented repeatedly.

One can also declare fact2 as follows:

The symbol mac# indicates that fact2_in_c is treated like a macro in C. In particular, fact2_in_c can be called without its prototype being declared first. As a matter of fact, it may not even have a prototype. This style of declaration naturally expects fact2_in_c to be implemented in C directly.It is also allowed to use sta# in place of mac#:

If declared in this style, which only occurs rarely in practice, then fact2_in_c is treated like a static function in C.For the sake of completeness, I mention as follows another way of declaring a static function:

This style of declaration is automatically translated into the following one: where the use of sta# means that the name referring to fact2 in C is simply fact2.External types and values can be readily formed in ATS to refer to types and values declared in C.

Suppose that there is a type in C of the name some_type_in_c, then this type can be referred to in ATS as $extype"some_type_in_c". For instance, type definitions are introduced in the following code for some external types in C:

typedef Cint = $extype"int" typedef Clint = $extype"long int" typedef Cllint = $extype"long long int" typedef Cint2 = $extype"struct{ int x; int y; }"

Just like including assembly code inside C code, it is straightforward to include C code inside ATS code. For instance, the example appearing at the beginning of this chapter can be written as follows in a single file:

// extern fun fact (n: int): int extern fun fact2 (n: int, res: int): int = "ext#fact2_in_c" // implement fact (n) = fact2 (n, 1) // %{ int fact2_in_c (int n, int res) { while (n > 0) { res *= n ; n -= 1 ; } ; return res ; } %} //

It is also allowed to put C code between the symbols
%{# and %}. Suppose that there is a file of the
name `foo.sats` that contains C code included in this manner.
If `foo.sats` is staloaded in another file of the name
`foo.dats`, then the lines between %{# and
%} in `foo.sats` are pasted into the C code
generated from compiling `foo.dats`.

It is straightforward to make calls to external functions in ATS. For instance, the following code demonstrates a typical way to do so:

local extern fun __fprintf : (FILEref, string(*fmt*), int, int) -> int = "mac#fprintf" in (* in of [local] *) // val N = 12 val _ = __fprintf (stdout_ref, "fact(%i) = %i\n", N, fact(N)) // end // end of [local]

There is also built-in support for calling external functions in ATS directly. For instance, the following code does essentially the same as the code presented above:

When $extfcall is employed to make an external function call, its first argument is the return type of the call, and its second argument is the name of the called function (represented as a string), and its rest of arguments are the arguments of the called function.ATS is probably not a programming language easy for one to write code in. While ATS provides many features to support safe (low-level) programming, it may take a long time and some great efforts for a programmer to learn and then master these features before he or she can make effective use of them. In this section, I would like to present some ATS code written in C-style that makes typical use of certain unsafe programming features in ATS. This is a programming style that should be familiar to any programmer who can write C code competently.

There are always occasions where one may find it sensible to program in unsafe C-style. Sometimes, one just wants to get a running implementation and then relies on testing to detect and fix bugs. Sometimes, one simply does not know enough of ATS needed to implement a function in a safe programming manner. This list of occasions can be readily extended as one wishes. I myself do unsafe C-style programming in ATS frequently, and I see it as a necessary skill for anyone who not just only wants to be able to write code in ATS but also wants to do it highly productively. Let us now see a concrete example of unsafe C-style programming in ATS.

Suppose that we want to implement a function for comparing two given strings according to the standard lexicographic ordering. Let us name the function strcmp and give it the following interface:

Given two strings str1 and str2, strcmp(str1, str2) is expected to return 1, -1, and 0 if str1 is greater than, less than, and equal to str2, respectively. An implementation of strcmp is given as follows:staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) implement strcmp (str1, str2) = let // fun loop ( p1: ptr, p2: ptr ) : int = let // val c1 = $UN.ptr0_get<uchar>(p1) val c2 = $UN.ptr0_get<uchar>(p2) // in case+ 0 of | _ when c1 > c2 => 1 | _ when c1 < c2 => ~1 | _ (* c1 = c2 *) => ( if $UN.cast{int}(c1) = 0 then 0 else loop (ptr0_succ<uchar>(p1), ptr0_succ<uchar>(p2)) // end of [if] ) end (* end of [loop] *) // in loop (string2ptr(str1), string2ptr(str2)) end (* end of [strcmp] *)

Please find the entire code for this example on-line.

For a function like strcmp, one can readily implement it in C directly. For instance, an implementation of strcmp in C, which is essentially a translation of the above implementation of strcmp in ATS, is given as follows:

int strcmp (char *p1, char *p2) { int res ; unsigned char c1, c2; while (1) { c1 = *p1; c2 = *p2; if (c1 > c2) { res = 1; break; } ; if (c1 < c2) { res = -1; break; } ; if ((int)c1==0) { res = 0 ; break ; } else { p1++; p2++; } ; } return res ; }

Suppose we want a function for copying into a given array the elements stored in a list. Let us name the function array_copy_from_list and give it the following interface:

Given a type T, array0(T) is for an array0-value containing a pointer p and a size n such that p points to a C-style array storing n elements of the type T.For the moment, let us require that the size of the array A equals the length of the list xs when array_copy_from_list(A, xs) is called. Following is an implementation of array_copy_from_list in ATS that makes use of an unsafe function (ptr0_set) declared in unsafe.sats:

staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) implement {a}(*tmp*) array_copy_from_list (A, xs) = let // fun loop ( p: ptr, xs: list0(a) ) : void = ( case+ xs of | list0_nil() => () | list0_cons(x, xs) => let val () = $UN.ptr0_set<a>(p, x) in loop (ptr0_succ<a>(p), xs) end // end of [list0_cons] ) (* end of [loop] *) // in loop (array0_get_ref(A), xs) end // end of [array_copy_from_list]

Please find the entire code for this example on-line.

There is also support in ATS for exporting types to make them available for use in C directly. In the following example, a typedef of the name int_and_string is expected to be declared in the generated C code for values that are assigned the type (int, string) in ATS:

Essentially, int_and_string is defined in C as follows:Sometimes, we want to construct in C values of a datatype declared in ATS. For instance, let us try to construct a value of the form cons2(i, d) in C for an integer i and a double d, where cons2 is a data constructor associated with the following declared datatype abc:

Whenever a data constructor is declared, a corresponding (linear) type constructor is created whose name equals the concatenation of the name of the data constructor and the string "_pstruct". So in the case of the above declared datatype abc, the type constructors cons1_pstruct and cons2_pstruct are created, and these type constructors can be used to form types for boxed values constructed with the data constructors cons1 and cons2.In the following declaration, the type cons2_pstruct(int, double) in ATS is exported to C under the name cons2_node:

Implicitly, a typedef in C of the name cons2_node_ is also introduced for the unboxed portion of a value constructed with the data constructor cons2. Essentially, we have the following generated code in C:typedef struct { int contag ; // constructor tag int atslab__0; double atslab__1; } cons2_node_ ; typedef cons2_node_ *cons2_node ;

cons2_node cons2_make ( int i, double d ) { cons2_node p ; p = ATS_MALLOC(sizeof(cons2_node_)) ; p->contag = 1 ; p->atslab__0 = i ; p->atslab__1 = d ; return p ; } /* end of [cons2_make] */

By assigning an interface to cons2_make in ATS, we can readily check whether cons2_make behaves as expected:

In general, it is essential for a pragrammer to acquire a solid understanding of low-level data representation of a programming language in order to use that language in low-level systems programming. The low-level data representation of ATS can be readily explained in terms of types in C, making it straightforward, when needed, to construct and manipulate ATS-values in C directly.

In embedded programming, static memory allocation is often preferred due to dynamic memory allocation being less predictable. I present as follows an example in which a list is constructed with statically allocated memory. This example also strongly attests to ATS and C being intimately related.

In order to statically allocate memory for list-nodes, we need to first form a type for list-nodes so that we can inform the C compiler how much memory is needed for each list-node. In the following code, the type list_node in ATS is for boxed list-nodes, and this type is exported to C under the same name:

// vtypedef list_node = list_cons_pstruct(int,ptr) // [list_node] for boxed nodes // extern vtypedef "list_node" = list_node // exporting [list_node] to C //

The following code statically allocates an array of list-nodes and then initialize these nodes, turning the array into a list:

local #define N 10 (* ** static allocation *) var nodes = @[list_node_][N]() fun loop ( p: ptr, i: int ) : void = let in // if i < N then let val res = $UN.castvwtp0{list_node}(p) val+list_cons (x, xs) = res val ( ) = x := i*i val p = ptr_succ<list_node_> (p) val i = i + 1 val () = ( if i < N then xs := p else xs := the_null_ptr ) : void // end of [val] val _(*ptr*) = $UN.castvwtp0{ptr}((view@x, view@xs | res)) in loop (p, i) end else ((*void*)) // end of [if] // end // end of [loop] in (* in of [local] *) val () = loop (addr@nodes, 0) val xs_static = $UN.castvwtp0{list(int,N)}((view@nodes|addr@nodes)) val () = println! ("xs_static = ", xs_static) // 0, 1, 4, 9, 16, ... end // end of [local]

Please find the entire code for this example on-line.

**Table of Contents**- 9. Introduction to Dependent Types
- 10. Datatype Refinement
- 11. Theorem-Proving in ATS/LF
- 12. Programming with Theorem-Proving

The types we have encountered so far in this book are often not adequately precise in capturing programming invariants. For instance, if we assign the type int to both of integers 0 and 1, then we simply cannot distinguish 0 from 1 at the level of types. This means that 0 and 1 are interchangeable as far as typechecking is concerned. In other words, we cannot expect a program error to be caught during typechecking if the error is caused by 0 being mistyped as 1. This form of imprecision in types can become a crippling limitation if we ever want to build a type-based specification language that is reasonably expressive for practical use.

Please find on-line the code employed for illustration in this chapter plus some additional code for testing.

The primary purpose of introducing dependent types into the type system of ATS is to greatly enhance the expressiveness of types so that they can be employed to capture program invariants with much greater precision. Generally speaking, dependent types are types dependent on values of expressions. For instance, bool is a type constructor in ATS that forms a type bool(b) when applied to a given boolean value b. As this type can only be assigned to a boolean expression of the value b, it is often referred to as a singleton type, that is, a type for exactly one value. Clearly, the meaning of bool(b) depends on the boolean value b. Similarly, int is a type constructor in ATS that forms a type int(i) when applied to a given integer i. This type is also a singleton type as it can only be assigned to an integer expression of the value i. Please note that both bool and int are overloaded as they also refer to (non-dependent) types. I will gradually introduce many other examples of dependent types. In particular, I will present a flexible means for the programmer to declare dependent datatypes.

The statics of ATS is a simply-typed language, and the types in this
language are called *sorts* so as to avoid some
potential confusion (with the types for dynamic terms). The following four
listed sorts are commonly used:

*bool*: for static terms of boolean values*int*: for static terms of integer values*type*: for static terms representing boxed types (for dynamic terms)*t@ype*: for static terms representing unboxed types (for dynamic terms)

~ (negation):

*(int) -> int*+ (addition):

*(int, int) -> int*- (subtraction):

*(int, int) -> int** (multiplication):

*(int, int) -> int*/ (division):

*(int, int) -> int*> (greater-than):

*(int, int) -> bool*>= (greater-than-or-equal-to):

*(int, int) -> bool*< (less-than):

*(int, int) -> bool*<= (less-than-or-equal-to):

*(int, int) -> bool*== (equal-to):

*(int, int) -> bool*!= (not-equal-to):

*(int, int) -> bool*<> (not-equal-to):

*(int, int) -> bool*~ (boolean negation):

*(bool) -> bool*|| (disjunction):

*(bool, bool) -> bool*&& (conjunction) :

*(bool, bool) -> bool*

sortdef nat = {a: int | a >= 0} // for natural numbers sortdef pos = {a: int | a >= 1} // for positive numbers sortdef neg = {a: int | a <= ~1} // for negative numbers sortdef nat1 = {a: nat | a < 1} // for 0 sortdef nat2 = {a: nat | a < 2} // for 0, 1 sortdef nat3 = {a: nat | a < 3} // for 0, 1, 2 sortdef nat4 = {a: nat | a < 4} // for 0, 1, 2, 3

sortdef nat2 = {a: int | 0 <= a; a < 2} // for 0, 1 sortdef nat3 = {a: int | 0 <= a; a < 3} // for 0, 1, 2 sortdef sgn = { i:int | ~1 <= i; i <= 1 } // for ~1, 0, 1

sortdef nat2 = {a: int | a == 0 || a == 1} // for 0, 1 sortdef nat3 = {a: int | 0 <= a && a <= 2} // for 0, 1, 2

In order to unleash the expressiveness of dependent types, we need to employ both universal and existential quantification over static variables. For instance, the type Int in ATS is defined as follows:

where the syntax [a:int] means existential quantification over a static variable a of the sortAt this point, types have already become much more expressive. For instance, we could only assign the type (int) -> int to a function that maps integers to natural numbers (e.g., the function that computes the absolute value of a given integer), but we can now do better by assigning it the type (Int) -> Nat, which is clearly more precise. In order to relate at the level of types the return value of a function to its arguments, we need universal quantification. For instance, the following universally quantified type is for a function that returns the successor of its integer argument:

where the syntax {i:int} means universal quantification over a static variable i of the sort int and the scope of this quantification is the function type following it. One may think that this function type is also a singleton type as the only function of this type is the successor function on integers. Actually, there are infinitely may partial functions that can be given this type as well. For the successor function on natural numbers, we can use the following type: where the syntax {i:int | i >= 0} means universal quantification over a static variable i of the sortfun g1int_neg {i:int} (int i): int (~i) // negation fun g1int_add {i,j:int} (int i, int j): int (i+j) // addition fun g1int_sub {i,j:int} (int i, int j): int (i-j) // subtraction fun g1int_mul {i,j:int} (int i, int j): int (i*j) // multiplication fun g1int_div {i,j:int} (int i, int j): int (i/j) // division fun g1int_lt {i,j:int} (int i, int j): bool (i < j) // less-than fun g1int_lte {i,j:int} (int i, int j): bool (i <= j) // less-than-or-equal-to fun g1int_gt {i,j:int} (int i, int j): bool (i > j) // greater-than fun g1int_gte {i,j:int} (int i, int j): bool (i >= j) // greater-than-or-equal-to fun g1int_eq {i,j:int} (int i, int j): bool (i == j) // equal-to fun g1int_neq {i,j:int} (int i, int j): bool (i != j) // not-equal-to

It is now a proper moment for me to raise an interesting question: What does a dependently typed interface for the factorial function look like? After seeing the above examples, it is only natural for one to expect something along the following line of thought:

whereTypechecking in ATS involves generating and solving constraints. As an example, the code below implements the well-known factorial function:

fun fact{n:nat} ( x: int(n) ) : [r:nat] int r = if x > 0 then x * fact (x-1) else 1 // end of [fact]

For each natural number n, n > 0 implies n - 1 >= 0

For each natural number n and each natural number r

_{1}, n > 0 implies n * r_{1}>= 0For each natural number n, 1 >= 0 holds.

By default, the constraint-solver implemented for ATS/Postiats makes use of the standard arithmetic of infinite precision. For the sake of efficiency, one may also choose to use machine-level arithmetic for solving integer constraints. Due to potential arithmetic overflow, results returned by the constraint-solver that uses machine-level arithmetic can be incorrect (but I have so far not knowingly encountered such a situation in practice).

A string in ATS is represented in the same manner as in C: It is a sequence
of adjacently stored non-null characters followed by the null character,
and its length is the number of non-null characters in the sequence.
Conventionally, such strings are often referred to as C-style strings,
which are notoriously difficult to be processed safely (as is clearly
indicated by so many bugs and breaches due to misusing such strings). As a
matter of fact, ATS is the first practical programming language that I know
can fully support safe processing of C-style strings. In ATS,
string is a type constructor of the sort *(int) ->
type*.
Given a static integer n, string(n) is the type for strings of
length n. Note that string also refers to a non-dependent type
for strings of unspecified length, which is basically equivalent to the
type String defined as follows:

// fun string_is_atend {n:int}{i:nat | i <= n} (str: string (n), i: size_t (i)): bool (i==n) // end of [string_is_atend] // fun string_isnot_atend {n:int}{i:nat | i <= n} (str: string (n), i: size_t (i)): bool (i < n) // end of [string_isnot_atend] //

fun string_length {n:nat} ( str: string (n) ) : size_t (n) = let fun loop {i:nat | i <= n} .<n-i>. (str: string n, i: size_t i): size_t (n) = if string_isnot_atend (str, i) then loop (str, succ(i)) else i // end of [loop] in loop (str, i2sz(0)) end // end of [string_length]

The following two functions are for accessing and updating characters stored in strings:

// typedef charNZ = [c:int | c != 0] char(c) // fun string_get_at {n:int}{i:nat | i < n}(str: string n, i: size_t i): charNZ overload [] with string_get_at // fun string_set_char_at {n:int}{i:nat | i < n}(str: string n, i: size_t i, c: charNZ): void overload [] with string_set_char_at //

// typedef sizeLt (n:int) = [i:nat | i < n] size_t (i) // fun string_find{n:nat} ( str: string n, c0: char ) : Option (sizeLt n) = let typedef res = sizeLt (n) fun loop{i:nat | i <= n} ( str: string n, c0: char, i: size_t i ) : Option (res) = let val isnot = string_isnot_atend (str, i) in if isnot then if (c0 = str[i]) then Some{res}(i) else loop (str, c0, succ(i)) else None () // end of [if] end (* end of [loop] *) in loop (str, c0, i2sz(0)) end // end of [string_find] //

There is some inherent inefficiency in the implementation of string_find: A given position i is first checked to see if it is strictly less than the length of the string str by calling string_isnot_atend, and, if it is, the character stored at the position in the string is fetched by calling string_get_at. These two function calls are merged into one in the following implementation:

// // This implementation does the same as [string_find] // but should be more efficient. // fun string_find2{n:nat} ( str: string n, c0: char ) : Option (sizeLt n) = let // fun loop{i:nat | i <= n} ( str: string n , c0: char, i: size_t i ) : Option (sizeLt n) = let typedef res = sizeLt (n) val c = string_test_at (str, i) in if c != '\000' then ( if (c0 = c) then Some{res}(i) else loop(str, c0, succ(i)) // end of [if] ) else None((*void*)) // end of [if] end // end of [loop] // in loop (str, c0, i2sz(0)) end // end of [string_find2]

fun string_test_at {n:int}{i:nat | i <= n} ( str: string (n), i: size_t (i) ) : [c:char | (c != NUL && i < n) || (c == NUL && i >= n)] char(c) // end of [string_test_at]

Handling strings safely and efficiently is a complicated matter in programming language design, and a great deal of information about a programming language can often be revealed by simply studying its treatment of strings. In ATS, properly processing C-style strings also makes essential use of linear types, which I will cover in another part of this book.

Given a type T of the sort *t@ype* and a static integer I (i.e.,
a static term of the sort *int*), arrayref(T, I) is
a boxed type for arrays of size I in which each stored element is of the
type T. Note that such arrays have no size information attached to them.
The following interface is for a function template
array_make_elt that can be called to create an array (with no
size information attached to it):

// fun{a:t@ype} arrayref_get_at {n:int}{i:nat | i < n} (A: arrayref (a, n), i: size_t i): (a) overload [] with arrayref_get_at // fun{a:t@ype} arrayref_set_at {n:int}{i:nat | i < n} (A: arrayref (a, n), i: size_t i, x: a): void overload [] with arrayref_set_at //

As a convincing example of practical programming with dependent types, the following code implements the standard binary search algorithm on an ordered array:

fun{ a:t@ype } bsearch_arr{n:nat} ( A: arrayref (a, n), n: int n, x0: a, cmp: (a, a) -> int ) : int = let // fun loop {i,j:int | 0 <= i; i <= j+1; j+1 <= n} ( A: arrayref (a, n), l: int i, u: int j ) :<cloref1> int = ( if l <= u then let val m = l + half (u - l) val x = A[m] val sgn = cmp (x0, x) in if sgn >= 0 then loop (A, m+1, u) else loop (A, l, m-1) end else u // end of [if] ) (* end of [loop] *) // in loop (A, 0, n-1) end // end of [bsearch_arr]

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

There is a mechanism in ATS that allows the programmer to supply termination metrics for checking whether recursively defined functions are terminating. It will soon become clear that this mechanism of termination-checking plays a fundamental role in the design of ATS/LF, a theorem-proving subsystem of ATS, where proofs are constructed as total functional programs.

A termination metric is just a tuple of natural numbers and the standard lexicographic ordering on natural numbers is used to order such tuples. In the following example, a singleton metric n is supplied to verify that the recursive function fact is terminating, where n is the value of the integer argument of fact:

Note that the metric attached to the recursive call fact(x-1) is n-1, which is strictly less than the initial metric n. Essentially, termination-checking in ATS verifies that the metric attached to each recursive call in the body of a function is strictly less that the initial metric attached to the function.A more difficult and also more interesting example is given as follows, where the MacCarthy's 91-function is implemented:

fun f91 {i:int} .<max(101-i,0)>. (x: int i) : [j:int | (i < 101 && j==91) || (i >= 101 && j==i-10)] int (j) = if x >= 101 then x-10 else f91 (f91 (x+11)) // end of [f91]

As another example, the following code implements the Ackermann's function, which is well-known for being recursive but not primitive recursive:

fun acker {m,n:nat} .<m,n>. (x: int m, y: int n): Nat = if x > 0 then if y > 0 then acker (x-1, acker (x, y-1)) else acker (x-1, 1) else y + 1 // end of [acker]

Termination-checking for mutually recursive functions is similar. In the following example, isevn and isodd are defined mutually recursively:

The metrics supplied for verifying the termination of isevn and isodd are 2*n and 2*n+1, respectively, where n is the value of the integer argument of isevn and also the value of the integer argument of isodd. Clearly, if the metrics (n, 0) and (n, 1) are supplied for isevn and isodd, respectively, the termination of these two functions can also be verified. Note that it is required that the metrics for mutually recursively defined functions be tuples of the same length.Given an integer x >= 0, the integer square root of x is the greatest integer i satisfying i * i <= x. An implementation of the integer square root function is given as follows based on the method of binary search:

fun isqrt ( x: int ) : int = let // fun search ( x: int, l: int, r: int ) : int = let val diff = r - l in case+ 0 of | _ when diff > 0 => let val m = l + (diff / 2) in // x < m * m can overflow easily if x / m < m then search (x, l, m) else search (x, m, r) // end of [if] end // end of [if] | _ (* diff <= 0 *) => l (* the result is found *) end // end of [search] // in search (x, 0, x) end // end of [isqrt]

l * l <= x and x <= r * r must hold when search(x, l, r) is called.

Assume l * l <= x < r * r for some integers x, l, r. If a recursive call search(x, l1, r1) for some integers l1 and r1 is encountered in the body of search(x, l, r), then r1-l1 < r-l must hold. This invariant implies that search is terminating.

fun isqrt {x:nat} ( x: int x ) : int = let // fun search {x,l,r:nat | l < r} .<r-l>. ( x: int x, l: int l, r: int r ) : int = let val diff = r - l in case+ 0 of | _ when diff > 1 => let val m = l + half(diff) in if x / m < m then search (x, l, m) else search (x, m, r) // end of [if] end // end of [if] | _ (* diff <= 1 *) => l (* the result is found *) end // end of [search] // in if x > 0 then search (x, 0, x) else 0 end // end of [isqrt]

By being precise and being able to enforce precision effectively, the programmer will surely notice that his or her need for run-time debugging is diminishing rapidly.

The datatype mechanism in ATS is adopted from ML directly, and it is really a signatory feature in functional programming. However, the datatypes we have seen so far are not very precise when employed to classify values. For instance, given a type T, the type list0(T) is for values representing both empty and non-empty lists consisting of elements of the type T. Therefore, empty and non-empty lists cannot be distinguished at the level of types. This limitation severely diminishes the effectiveness of datatypes of ML-style in capturing program invariants. In ATS, datatypes of ML-style can be refined into dependent datatypes of DML-style, where DML refers to the programming language Dependent ML, the immediate precursor of ATS. With such refinement, datatypes can classify values with greatly enhanced precision.

The syntax for declaring dependent datatypes is mostly similar to the syntax for declaring non-dependent datatypes: For instance, the dependent datatype list in ATS is declared as follows:

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

There two data (or value) constructors list_nil and list_cons associated with list, which are declared to be of the following types:

Given a type T and a static integer I, the type list(T, I) is for values representing lists of length I in which each element is of the type T. Hence, the types of list_nil and list_cons mean that list_nil forms a list of length 0 and list_cons forms a list of length n+1 if applied to an element and a list of length n. Note that it is also possible to declare list as follows in a more concise style:datatype list (a:t@ype+, int) = | list_nil(a, 0) of () // [of ()] is optional | {n:nat} list_cons(a, n+1) of (a, list(a, n))

As an example of programming with dependent datatypes, the following code implements a function template for computing the length of a given list:

fun{ a:t@ype } list_length {n:nat} .<n>. // .<n>. is a termination metric (xs: list (a, n)): int (n) = case+ xs of | list_nil((*void*)) => 0 | list_cons(_(*x*), xs1) => 1 + list_length<a>(xs1) // end of [list_length]

Given that the two clauses typecheck properly, the case-expression containing them can be assigned the type int(n). Therefore, the definition of list_length typechecks.

As the recursive call in the body of the above defined function list_length is not a tail-call, the function may not be able to handle a long list (e.g., one that contains 1 million elements). The following code gives another implementation for computing the length of a given list:

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

This time, list_length is based on a tail-recursive function loop and thus can handle lists of any length in constant stack space. Note that the type assigned to loop indicates that loop takes a list of length i and an integer of value j for some natural numbers i and j and returns an integer of value i+j. Also, loop is verified to be terminating.

There is also a dependent datatype option in ATS for forming optional values:

As an example, the following function template list_last tries to find the last element in a given list:

fun{ a:t@ype } list_last {n:nat} .<>. ( xs: list (a, n) ) : option (a, n > 0) = let // fun loop {n:pos} .<n>. ( xs: list (a, n) ) : a = let val+ list_cons (_, xs1) = xs in case+ xs1 of | list_cons _ => loop (xs1) | list_nil () => let val+ list_cons (x, _) = xs in x end // end of [list_nil] end // end of [loop] // in case+ xs of | list_cons _ => Some (loop (xs)) | list_nil () => None () end // end of [list_last]

The inner function loop is evidently tail-recursive and it is verified to be terminating.

After a programmer becomes familar with list and option, there is little incentive for him or her to use list0 and option0 anymore. Internally, values of list and list0 have exactly the same representation and there are cast functions of zero run-time cost in ATS for translating between values of list and list0. The same applies to values of option and option0 as well.

I have presented previously implementation of some commonly used function templates on lists formed with the constructors list0_nil and list0_cons. This time, I present as follows implementation of the corresponding function templates on lists formed with the constructors list_nil and list_cons, which make it possible to assign more accurate types to these templates.

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

Given two lists xs and ys of the types list(T, I1) and list(T, I2) for some type T and integers I1 and I2, list_append(xs, ys) returns a list of the type list(T,I1+I2) that is the concatenation of xs and ys:

Clearly, this implementation of list_append is not tail-recursive.Given two lists xs and ys of the type list(T, I1) and list(T, I2) for some type T and integers I1 and I2, list_reverse_append(xs, ys) returns a list of the type list(T, I1+I2) that is the concatenation of the reverse of xs and ys:

Clearly, this implementation of list_reverse_append is tail-recursive.Given a list xs, list_reverse(xs) returns the reverse of xs, which is of the same length as xs:

Given a list xs of the type list(T1, I) for some type T1 and integer I and a closure function f of the type T1 -<cloref1> T2 for some T2, list_map(xs) returns a list ys of the type list(T2, I):

Each element y in ys equals f(x), where x is the corresponding element in xs. Clearly, this implementation of list_map is not tail-recursive.Given two lists xs and ys of the types list(T1, I) and list(T2, I) for some types T1 and T2 and integer I, respectively, list_zip(xs, ys) returns a list zs of the type list((T1,T2), I).

Each element z in zs equals the pair (x, y), where x and y are the corresponding elements in xs and ys, respectively. Clearly, this implementation of list_zip is not tail-recursive.Given two lists xs and ys of the types list(T1, I) and list(T2, I) for some types T1 and T2 and integer I, respectively, and a closure function f of the type (T1, T2) -<cloref1> T3 for some type T3, list_zipwith(xs, ys, f) returns a list zs of the type list(T3, I):

fun{ a,b:t@ype }{c:t@ype } list_zipwith {n:nat} .<n>. ( xs: list (a, n) , ys: list (b, n) , f: (a, b) -<cloref1> c ) : list (c, n) = ( case+ (xs, ys) of | ( list_nil() , list_nil() ) => list_nil((*void*)) | ( list_cons(x, xs) , list_cons(y, ys) ) => list_cons(f(x, y), list_zipwith<a,b><c>(xs, ys, f)) // end of (list_cons, list_cons) ) (* end of [list_zipwith] *)

I have previously presented an implementation of mergesort on lists that are formed with the constructors list0_nil and list0_cons. In this section, I give an implementation of mergesort on lists formed with the constructors list_nil and list_cons. This implementation is based on the same algorithm as the previous one but it assigns a type to the implemented sorting function that guarantees the function to be length-preserving, that is, the function always returns a list of the same length as the list it sorts.

The following defined function merge combines two ordered list (according to a given ordering) into a single ordered list:

// typedef lte (a:t@ype) = (a, a) -> bool // fun{ a:t@ype } merge {m,n:nat} .<m+n>. ( xs0: list (a, m), ys0: list (a, n), lte: lte a ) : list (a, m+n) = case+ xs0 of | list_nil() => ys0 | list_cons(x, xs1) => ( case+ ys0 of | list_nil() => xs0 | list_cons(y, ys1) => if x \lte y then list_cons (x, merge (xs1, ys0, lte)) else list_cons (y, merge (xs0, ys1, lte)) // end of [if] ) // end of [list_cons] // end of [merge] //

The following defined function mergesort mergesorts a list according to a given ordering:

fun{ a:t@ype } mergesort{n:nat} ( xs: list (a, n), lte: lte a ) : list (a, n) = let // fun msort {n:nat} .<n,n>. ( xs: list (a, n), n: int n, lte: lte a ) : list (a, n) = if n >= 2 then split (xs, n, lte, half(n), list_nil) else xs // end of [if] // end of [msort] and split {n:int | n >= 2}{i:nat | i <= n/2} .<n,i>. ( xs: list (a, n-n/2+i) , n: int n, lte: lte a, i: int i, xsf: list (a, n/2-i) ) : list (a, n) = if i > 0 then let val+ list_cons (x, xs) = xs in split (xs, n, lte, i-1, list_cons (x, xsf)) end else let val n2 = half(n) val xsf = list_reverse<a> (xsf) // make sorting stable! val xsf = list_of_list_vt (xsf) // linear list -> nonlinear list val xsf = msort (xsf, n2, lte) and xs = msort (xs, n-n2, lte) in merge (xsf, xs, lte) end // end of [if] // end of [split] // in msort(xs, list_length<a>(xs), lte) end // end of [mergesort]

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

In ATS, pattern matching is performed sequentially at run-time. In other words, a clause is selected only if a given value matches the pattern guard associated with this clause but the value fails to match the pattern associated with any clause ahead of it. Naturally, one may expect that the following implementation of list_zipwith also typechecks:

fun{ a,b:t@ype }{c:t@ype } list_zipwith {n:nat} ( xs: list(a, n) , ys: list(b, n) , f: (a, b) -<cloref1> c ) : list(c, n) = ( // case+ (xs, ys) of | ( list_cons(x, xs) , list_cons(y, ys)) => ( list_cons(f(x, y), list_zipwith<a,b><c>(xs, ys, f)) ) | (_, _) => list_nil((*void*)) // ) (* end of [list_zipwith] *)

(list_cons _, list_nil ())

(list_nil (), list_cons _)

(list_nil (), list_nil ())

One may be wondering why typechecking clauses is not required to be done sequentially by default. The simple reason is that this requirement, if fully enforced, can have a great negative impact on the efficiency of typechecking. Therefore, it is a reasonable design to provide the programmer with an explict means to occasionally make use of the sequentiality assumption needed for typechecking a particular clause.

A red-black tree is defined as a binary tree such that each node in it is
colored red or black and every path from the root to a leaf has the same
number of black nodes while containing no occurrences of two red nodes in a
row. Clearly, the length of a longest path in each red-black tree is
bounded by 2 times the length of a shortest path in it. Therefore,
red-black trees are a family of balanced trees. The number of black nodes
occurring on each path in a red-black tree is often referred to as the
*black height* of the tree.

Formally, a datatype precisely for red-black trees can be declared in ATS as follows:

// #define BLK 0 #define RED 1 sortdef clr = {c:nat | c <= 1} // datatype rbtree (a:t@ype+, int(*clr*), int(*bh*)) = | rbtree_nil (a, BLK, 0) | {c,cl,cr:clr | cl <= 1-c; cr <= 1-c} {bh:nat} rbtree_cons (a, c, bh+1-c) of (int c, rbtree (a, cl, bh), a, rbtree (a, cr, bh)) // end of [rbtree] //

The color of a tree is the color of its root node or is black if the tree is empty. Given a type T, a color C (represented by a integer) and an integer BH, the type rbtree(T, C, BH) is for red-black trees carrying elements of the type T that is of the color C and the black height BH.

When implementing various operations (such as insertion and deletion) on a red-black tree, we often need to first construct intermediate trees that contain color violations caused by a red node being followed by another red node and then employ tree rotations to fix such violations. This need makes the above datatype rbtree too rigid as it cannot be assigned to any intermediate trees containing color violations. To address this issue, we can declare rbtree as follows:

// datatype rbtree ( a:t@ype+ , int // color , int // black height , int // violations ) = // rbtree | rbtree_nil (a, BLK, 0, 0) of () | {c,cl,cr:clr}{bh:nat}{v:int} {c==BLK && v==0 || c == RED && v==cl+cr} rbtree_cons (a, c, bh+1-c, v) of ( int c, rbtree0 (a, cl, bh), a, rbtree0(a, cr, bh) ) (* end of [rbtree_cons] *) // end of [rbtree] // where rbtree0(a:t@ype, c:int, bh:int) = rbtree(a, c, bh, 0) //

We count each occurrence of two red nodes in a row as one color violation. Given a type T, a color C (represented by a integer), an integer BH and an integer V, the type rbtree(T, C, BH, V) is for trees carrying elements of the type T that is of the color C and the black height BH and contains exactly V color violations. Therefore, the type rbtree(T, C, BH, 0) is for valid red-black trees (containing no color violations).

Given a tree containing at most one color violation, an element and another tree containing no violations, the following operation constructs a valid red-black tree:

fn{ a:t@ype } insfix_l // right rotation for fixing left insertion {cl,cr:clr} {bh:nat} {v:nat} ( tl: rbtree (a, cl, bh, v), x0: a, tr: rbtree (a, cr, bh, 0) ) : [c:clr] rbtree0 (a, c, bh+1) = let #define B BLK; #define R RED; #define cons rbtree_cons in case+ (tl, x0, tr) of | (cons (R, cons (R, a, x, b), y, c), z, d) => cons (R, cons (B, a, x, b), y, cons (B, c, z, d)) // shallow rot | (cons (R, a, x, cons (R, b, y, c)), z, d) => cons (R, cons (B, a, x, b), y, cons (B, c, z, d)) // deep rotation | (a, x, b) =>> cons (B, a, x, b) end // end of [insfix_l]

By simply reading the interface of insfix_l, we can see that the two tree arguments are required to be of the same black height bh for some natural number bh and the returned tree is of the black height bh+1.

The following operation insfix_r is just the mirror image of insfix_l:

fn{ a:t@ype } insfix_r // left rotation for fixing right insertion {cl,cr:clr} {bh:nat} {v:nat} ( tl: rbtree (a, cl, bh, 0), x0: a, tr: rbtree (a, cr, bh, v) ) : [c:clr] rbtree0 (a, c, bh+1) = let #define B BLK; #define R RED; #define cons rbtree_cons in case+ (tl, x0, tr) of | (a, x, cons (R, b, y, cons (R, c, z, d))) => cons (R, cons (B, a, x, b), y, cons (B, c, z, d)) // shallow rot | (a, x, cons (R, cons (R, b, y, c), z, d)) => cons (R, cons (B, a, x, b), y, cons (B, c, z, d)) // deep rotation | (a, x, b) =>> cons (B, a, x, b) end // end of [insfix_r]

The preparation for implementing insertion on a red-black tree is all done by now, and we are ready to see an implementation of insertion guaranteeing that the tree obtained from inserting an element into a given red-black tree is always a valid red-black tree itself. This guarantee is precisely captured in the following interface for insertion:

extern fun{ a:t@ype } rbtree_insert {c:clr} {bh:nat} ( t: rbtree0 (a, c, bh), x0: a, cmp: cmp a ) : [bh1:nat] rbtree0 (a, BLK, bh1)

Interestingly, this interface also implies that the tree returned by a call to rbtree_insert is always black. The code presented below gives an implementation of rbtree_insert:

implement{a} rbtree_insert (t, x0, cmp) = let // #define B BLK #define R RED #define nil rbtree_nil #define cons rbtree_cons // fun ins {c:clr}{bh:nat} .<bh,c>. ( t: rbtree0 (a, c, bh), x0: a ) : [ cl:clr;v:nat | v <= c ] rbtree (a, cl, bh, v) = ( case+ t of | nil ((*void*)) => cons{..}{..}{..}{0} (R, nil, x0, nil) | cons (c, tl, x, tr) => let val sgn = compare (x0, x, cmp) in if sgn < 0 then let val [cl,v:int] tl = ins (tl, x0) in if c = B then insfix_l (tl, x, tr) else cons{..}{..}{..}{cl} (R, tl, x, tr) // end of [if] end else if sgn > 0 then let val [cr,v:int] tr = ins (tr, x0) in if c = B then insfix_r (tl, x, tr) else cons{..}{..}{..}{cr} (R, tl, x, tr) // end of [if] end else t // end of [if] end // end of [cons] ) (* end of [ins] *) // val t = ins (t, x0) // in case+ t of cons (R, tl, x, tr) => cons (B, tl, x, tr) | _ =>> t end // end of [rbtree_insert]

Note that the type assigned to the inner function ins is so informative that it literally gives an formal explanation about the way in which insertion works on a red-black tree. Many a programmer implements red-black trees by simply following an algorithm written in some format of pseudo code while having little understanding about the innerworkings of the algorithm. For instance, if the above inner function ins is implemented in C, few programmers are likely to see that the function always maintain the black height of a given red-black tree after insertion but may introduce one color violation if the root of the tree is red. On the other hand, knowing this invariant is essential to gaining a thorough understanding of the insertion algorithm on red-black trees.

The insertion operation implemented above does not insert an element if it is already in the given red-black tree. It may be desirable to require that the operation inform the caller if such a case occurs. For instance, an exception can be raised for this purpose. An alternative is to give rbtree_insert a call-by-reference argument so that a flag can be returned in it to indicate whether the element to be inserted is actually inserted. I will explain elsewhere what call-by-reference is and how it is supported in ATS.

Often deleting an element from a binary search tree is significantly more difficult to implement than inserting one. This is especially so in the case of a red-black tree. I refer the interested reader to the libats library of ATS for some code implementing a deletion operation on red-black trees that can guarantee based on types each tree returned by the operation being a valid red-black tree (containing no color violations).

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

Within the ATS programming language system, there is a component named
ATS/LF for supporting (interactive) therorem-proving. In ATS/LF,
theorem-proving is done by constructing proofs as total functional
programs. It will soon become clear that this style of theorem-proving can
be combined cohesively with functional programming to yield a programming
paradigm that is considered the signature of ATS: *programming
with theorem-proving*. Moreover, ATS/LF can be employed to encode various
deduction systems and their meta-properties.

Please find on-line the code employed for illustration in this chapter plus some additional code for testing.

In the statics of ATS, there is a built-in sort *prop* for
static terms that represent types for proofs. A static term of the sort
*prop* can also be referred to as a type or more accurately, a
prop-type or just a prop. A dataprop can be declared in a manner that is
mostly similar to the declaration of a datatype. For instance, a prop
construct FIB is introduced in the following dataprop declaration:

dataprop FIB(int, int) = | FIB0(0, 0) of () // [of ()] can be dropped | FIB1(1, 1) of () // [of ()] can be dropped | {n:nat}{r0,r1:int} FIB2(n+2, r0+r1) of (FIB(n, r0), FIB(n+1, r1)) // end of [FIB]

FIB0: () -> FIB(0, 0)

FIB1: () -> FIB(1, 1)

FIB2: {n:nat}{r0,r1:int} (FIB(n, r0), FIB(n+1, r1)) -> FIB(n+2, r0+r1)

fib(0) = 0, and

fib(1) = 1, and

fib(n+2) = fib(n) + fib(n+1) for n >= 2.

As another example of dataprop, the following declaration introduces a prop constructor MUL together with three associated proof constructors:

dataprop MUL(int, int, int) = | {n:int} MULbas(0, n, 0) of () | {m:nat}{n:int}{p:int} MULind(m+1, n, p+n) of MUL(m, n, p) | {m:pos}{n:int}{p:int} MULneg(~(m), n, ~(p)) of MUL(m, n, p) // end of [MUL]

0*n = 0 for every integer n, and

(m+1)*n = m*n + n for each pair of integers m and n, and

(~m)*n = ~(m*n) for each pair of integers m and n.

It can be readily noticed that the process of encoding a functional relation (i.e., a relation representing a function) as a dataprop is analogous to implementing a function in a logic programming language such as Prolog.

Theorems are represented as types (or more accurately, props) in ATS/LF. For instance, the following prop states that integer multiplication is commutative:

Constructing a proof for a theorem in ATS/LF means implementing a total value (which is most likely to be a total function) of the type that is the encoding of the theorem in ATS/LF, where being total means being pure and terminating. Please note that this style of theorem-proving may seem rather peculiar to those who have never tried it before.As a simple introductory example, let us first construct a proof function in ATS/LF that is given the following interface:

The keyword prfun indicates that the interface is for a proof function (in contrast to a non-proof function). Note that mul_istot is declared to be of the following type (or more accurately, prop): which essentially states that integer multiplication is a total function: Given any two integers m and n, there exists an integer p such that m, n and p are related according to the structurally inductively defined relation MUL. The following code gives an implementation of mul_istot:primplement mul_istot{m,n}() = let // prfun istot {m:nat;n:int} .<m>. (): [p:int] MUL(m, n, p) = sif m > 0 then MULind(istot{m-1,n}()) else MULbas() // end of [istot] // in sif m >= 0 then istot{m,n}() else MULneg(istot{~m,n}()) end // end of [mul_istot]

As another example of theorem-proving in ATS/LF, a proof function of the name mul_isfun is given as follows:

prfn mul_isfun {m,n:int}{p1,p2:int} ( pf1: MUL(m, n, p1), pf2: MUL(m, n, p2) ) : [p1==p2] void = let prfun isfun {m:nat;n:int}{p1,p2:int} .<m>. ( pf1: MUL(m, n, p1), pf2: MUL(m, n, p2) ) : [p1==p2] void = case+ pf1 of | MULind(pf1prev) => let prval MULind(pf2prev) = pf2 in isfun (pf1prev, pf2prev) end // end of [MULind] | MULbas() => let prval MULbas() = pf2 in () end // end of [MULbas] // end of [isfun] in case+ pf1 of | MULneg(pf1nat) => let prval MULneg(pf2nat) = pf2 in isfun (pf1nat, pf2nat) end // end of [MULneg] | _ (*non-MULneg*) =>> isfun (pf1, pf2) end // end of [mul_isfun]

What mul_isfun proves is that the relation MUL is functional on its first two arguments: If m, n and p1 are related according to MUL and m, n and p2 are also related according to MUL, then p1 and p2 are equal. The statement is first proven by the inner proof function isfun under the assumption that m is a natural number, and then the assumption is dropped. Let us now take a look at the first matching clause in the body of isfun. If the clause is chosen, then pf1 matches the pattern MULind(pf1prev) and thus pf1prev is of the type MUL(m1, n1, q1) for some natural number m1 and integer n1 and integer p1 such that m=m1+1, n=n1, and p1=q1+n1. This means that pf2 must be of the form MULind(pf2prev) for some pf2prev of the type MUL(m2, n2, q2) such that m2+1=m, n2=n and p2=q2+n2. By calling isfun on pf1prev and pf2prev, which amounts to invoking the induction hypothesis on m-1, we establish q1=q2, which implies p1=p2. The second matching clause in the body of isfun can be readily understood, which corresponds to the base case in the inductive proof encoded by isfun.

The distributivity of multiplication over addition means that the following equation holds

for m, n1 and n2 ranging over integers. A direct encoding of the equation is given by the following (proof) function interface:// prfun mul_distribute {m,n1,n2:int}{p1,p2:int} (MUL(m, n1, p1), MUL(m, n2, p2)): MUL(m, n1+n2, p1+p2) //

primplement mul_distribute {m,n1,n2}{p1,p2} (pf1, pf2) = let // prfun auxnat {m:nat}{p1,p2:int} .<m>. ( pf1: MUL(m, n1, p1), pf2: MUL(m, n2, p2) ) : MUL(m, n1+n2, p1+p2) = ( case+ (pf1, pf2) of | (MULbas(), MULbas()) => MULbas() | (MULind pf1, MULind pf2) => MULind(auxnat (pf1, pf2)) ) (* end of [auxnat] *) // in // sif m >= 0 then ( auxnat (pf1, pf2) ) // end of [then] else let prval MULneg(pf1) = pf1 prval MULneg(pf2) = pf2 in MULneg(auxnat (pf1, pf2)) end // end of [else] // end // end of [mul_distribute]

The commutativity of multiplication means that the following equation holds

for m and n ranging over integers. A direct encoding of this equation is given by the following (proof) function interface: An implementation of mul_commute is given as follows:primplmnt mul_commute {m,n}{p}(pf0) = let // prfun auxnat {m:nat} {p:int} .<m>. ( pf: MUL(m, n, p) ) : MUL(n, m, p) = ( case+ pf of | MULbas() => mul_nx0_0{n}() | MULind(pf1) => mul_distribute(auxnat(pf1), mul_nx1_n{n}()) // end of [MULind] ) (* end of [auxnat] *) // in // sif m >= 0 then auxnat(pf0) else let prval MULneg(pf1) = pf0 in mul_neg_2(auxnat(pf1)) end // end of [else] // end // end of [mul_commute]

A datasort is rather similar to a dataype. However, the former is
declared in the statics of ATS while the latter in the dynamics of ATS. To
see a typical need for datasorts, let us try to encode a theorem in ATS
stating that s is strictly less than 2^{h} if s and
h are the size and height, respectively, of a given binary tree. To
represent binary trees in the statics, we first declare a datasort as
follows:

We now declare two dataprops as follows for capturing the notion of size and height of trees:

// dataprop SZ (tree, int) = | SZE (E (), 0) of () | {tl,tr:tree}{sl,sr:nat} SZB (B (tl, tr), 1+sl+sr) of (SZ (tl, sl), SZ (tr, sr)) // end of [SZ] // dataprop HT (tree, int) = | HTE (E (), 0) of () | {tl,tr:tree}{hl,hr:nat} HTB (B (tl, tr), 1+max(hl,hr)) of (HT (tl, hl), HT (tr, hr)) // end of [HT] //

As the power function (of base 2) is not available in the statics of ATS, we declare a dataprop as follows to capture it:

dataprop POW2 (int, int) = | POW2bas (0, 1) | {n:nat}{p:int} POW2ind (n+1, p+p) of POW2 (n, p) // end of [POW2]

It should be clear by now that the following proof function
interface encodes the theorem stating that s is strictly less than
2^{h} if s and h are the size and height of a
given binary tree:

prfun lemma_tree_size_height {t:tree}{s,h:nat}{p:int} ( pf1: SZ (t, s), pf2: HT (t, h), pf3: POW2 (h, p) ) : [s < p] void // end of [prfun]

We first establish some elementary properties on the power function (of base 2):

prfun pow2_istot {h:nat} .<h>. (): [p:int] POW2 (h, p) = sif h==0 then POW2bas () else POW2ind (pow2_istot {h-1} ()) // end of [sif] // end of [pow2_istot] prfun pow2_pos {h:nat}{p:int} .<h>. (pf: POW2 (h, p)): [p > 0] void = case+ pf of | POW2bas () => () | POW2ind (pf1) => pow2_pos (pf1) // end of [pow2_pos] prfun pow2_inc {h1,h2:nat | h1 <= h2}{p1,p2:int} .<h2>. (pf1: POW2 (h1, p1), pf2: POW2 (h2, p2)): [p1 <= p2] void = case+ pf1 of | POW2bas () => pow2_pos (pf2) | POW2ind (pf11) => let prval POW2ind (pf21) = pf2 in pow2_inc (pf11, pf21) end // end of [POW2ind] // end of [pow2_inc]

The function lemma_tree_size_height can be implemented as follows:

primplement lemma_tree_size_height (pf1, pf2, pf3) = let // prfun lemma{t:tree} {s,h:nat}{p:int} .<t>. ( pf1: SZ (t, s) , pf2: HT (t, h) , pf3: POW2 (h, p) ) : [p > s] void = ( scase t of | E () => let prval SZE () = pf1 prval HTE () = pf2 prval POW2bas () = pf3 in // nothing end // end of [E] | B (tl, tr) => let prval SZB (pf1l, pf1r) = pf1 prval HTB {tl,tr}{hl,hr} (pf2l, pf2r) = pf2 prval POW2ind (pf31) = pf3 prval pf3l = pow2_istot {hl} () prval pf3r = pow2_istot {hr} () prval () = lemma (pf1l, pf2l, pf3l) prval () = lemma (pf1r, pf2r, pf3r) prval () = pow2_inc (pf3l, pf31) prval () = pow2_inc (pf3r, pf31) in // nothing end // end of [B] ) (* end of [lemma] *) // in lemma (pf1, pf2, pf3) end // end of [lemma_tree_size_height]

As stated previously in this book, a binary tree is a Braun tree if it is empty or if its left and right subtrees are Braun trees and the size of the left one minus the size of the right one is either 0 or 1. Formally, we can declare the following dataprop isBraun to capture the notion of Braun trees:

dataprop isBraun (tree) = | isBraunE (E) of () | {tl,tr:tree} {sl,sr:nat | sr <= sl; sl <= sr + 1} isBraunB ( B(tl, tr)) of (isBraun tl, isBraun tr, SZ (tl, sl), SZ (tr, sr) ) // end of [isBraunB] // end of [isBraun]

We first prove that there exists a Braun tree of any given size. This property can be encoded as follows in ATS:

Literally, the type assigned to lemma_existence means that there exists a tree t for any given natural number n such that t is a Braun tree and the size of t is n. The following code gives an implementation of lemma_existence:primplement lemma_existence {n}((*void*)) = let // prfun lemma{n:nat} .<n>. ( // argless ) : [t:tree] (isBraun (t), SZ (t, n)) = sif n==0 then (isBraunE (), SZE ()) else let stadef nl = n / 2 stadef nr = n - 1 - nl val (pfl1, pfl2) = lemma{nl}((*void*)) and (pfr1, pfr2) = lemma{nr}((*void*)) in (isBraunB (pfl1, pfr1, pfl2, pfr2), SZB (pfl2, pfr2)) end // end of [else] // end of [sif] // in lemma{n}((*void*)) end // end of [lemma_existence]

Next we show that two Braun trees of the same size are identical. This property can be encoded as follows:

prfun lemma_unicity {n:nat}{t1,t2:tree} ( pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n) ) : EQ (t1, t2) // end of [lemma_unicity]

dataprop EQ (tree, tree) = | EQE (E, E) of () | {t1l,t1r:tree}{t2l,t2r:tree} EQB (B (t1l, t1r), B (t2l, t2r)) of (EQ (t1l, t2l), EQ (t1r, t2r)) // end of [EQ]

primplement lemma_unicity (pf1, pf2, pf3, pf4) = let prfun lemma{n:nat}{t1,t2:tree} .<n>. ( pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n) ) : EQ (t1, t2) = sif n==0 then let prval SZE () = pf3 and SZE () = pf4 prval isBraunE () = pf1 and isBraunE () = pf2 in EQE () end // end of [then] else let prval SZB (pf3l, pf3r) = pf3 prval SZB (pf4l, pf4r) = pf4 prval isBraunB (pf1l, pf1r, pf1lsz, pf1rsz) = pf1 prval isBraunB (pf2l, pf2r, pf2lsz, pf2rsz) = pf2 prval () = SZ_istot (pf1lsz, pf3l) and () = SZ_istot (pf1rsz, pf3r) prval () = SZ_istot (pf2lsz, pf4l) and () = SZ_istot (pf2rsz, pf4r) prval pfeql = lemma (pf1l, pf2l, pf3l, pf4l) prval pfeqr = lemma (pf1r, pf2r, pf3r, pf4r) in EQB (pfeql, pfeqr) end // end of [else] // end of [sif] in lemma (pf1, pf2, pf3, pf4) end // end of [lemma_unicity]

As a comparison, the following code gives another implementation of lemma_unicity that is of a different (and rather unusual) style:

primplement lemma_unicity (pf1, pf2, pf3, pf4) = let // prfun lemma{n:nat}{t1,t2:tree} .<t1>. ( pf1: isBraun t1, pf2: isBraun t2, pf3: SZ (t1, n), pf4: SZ (t2, n) ) : EQ (t1, t2) = case+ (pf1, pf2) of // | (isBraunE (), isBraunE ()) => EQE () // | (isBraunB (pf11, pf12, pf13, pf14), isBraunB (pf21, pf22, pf23, pf24)) => let // prval SZB (pf31, pf32) = pf3 prval SZB (pf41, pf42) = pf4 // prval () = SZ_istot (pf13, pf31) prval () = SZ_istot (pf23, pf41) // prval () = SZ_istot (pf14, pf32) prval () = SZ_istot (pf24, pf42) // prval pfeq1 = lemma (pf11, pf21, pf31, pf41) prval pfeq2 = lemma (pf12, pf22, pf32, pf42) in EQB (pfeq1, pfeq2) end // | (isBraunE _, isBraunB _) =/=> let prval SZE _ = pf3 and SZB _ = pf4 in (*none*) end | (isBraunB _, isBraunE _) =/=> let prval SZB _ = pf3 and SZE _ = pf4 in (*none*) end // in lemma (pf1, pf2, pf3, pf4) end // end of [lemma_unicity]

I have so far presented several formal proofs in ATS. However, constructing such formal proofs is at most a secondary issue in ATS. If I compare ATS with theorem-proving systems such as Isabelle and Coq, I would like to state emphatically that the design for theorem-proving in ATS takes a fundamentally different view of theorem-proving. In particular, theorem-proving in ATS does not take a foundational approach that establishes the validity of a theorem by reducing it to the validity of a minimal set of axioms and rules. Instead, theorem-proving in ATS is mostly done in a semi-formal manner and its primary purpose is to greatly diminish the chance of a programmer making use of incorrect assumptions or claims. In this regard, theorem-proving in ATS is rather similar to contructing informal paper-and-pencil proofs (in mathematics and elsewhere). I refer to this style of theorem-proving in ATS as being programmer-centric. In order to allow the reader to obtain a more concrete feel as to what this style of theorem-proving is like, I present in the rest of this section a simple but telling example of programmer-centric theorem-proving.

Suppose we are to prove that the square of any rational number cannot equal 2. Note that this statement is a bit weaker than the one stating that the square root of 2 is irrational as the latter assumes the very existence of the square root of 2. Let us first sketch an informal proof as follows.

Suppose (m/n)^{2}=2 for some positive numbers m and n. Clearly,
this means (m)^{2}=2(n)^{2}, implying m being an even number.
Let m=2m_{2}. We have (2m_{2})^{2}=2(n)^{2}, implying
(n/m_{2})^{2}=2. Clearly, m > n > m_{2} holds. If we
assume that m is the least positive number satisfying (m/n)^{2}=2 for
some n, then a contradiction is reached as n satisfies the same property.
Therefore, there is no rational number whose square equals 2. Clearly,
this proof still holds if the number 2 is replaced with another prime number.

The primary argument in the above informal proof can be encoded in ATS as follows:

// extern prfun mylemma_main {m,n,p:int | m*m==p*n*n}(PRIME(p)): [m2:nat | n*n==p*m2*m2] void // primplmnt mylemma_main {m,n,p}(pfprm) = let prval pfeq_mm_pnn = eqint_make{m*m,p*n*n}() prval () = square_is_nat{m}() prval () = square_is_nat{n}() prval () = lemma_PRIME_param(pfprm) prval pfmod1 = lemma_MOD0_intr{m*m,p,n*n}() prval pfmod2 = mylemma1{m,p}(pfmod1, pfprm) prval [m2:int] EQINT() = lemma_MOD0_elim(pfmod2) prval EQINT() = pfeq_mm_pnn prval () = __assert{p}{p*m2*m2,n*n}() where { extern prfun __assert{p:pos}{x,y:int | p*x==p*y}(): [x==y] void } (* end of [where] *) // end of [prval] in #[m2 | ()] end // end of [mylemma_main] //

Given two integers m and p, MOD0(m,p) means that m equals the product of p and q for some natural number q. This meaning is encoded into the following two proof functions:

// prfun lemma_MOD0_intr{m,p,q:nat | m==p*q}(): MOD0(m, p) // prfun lemma_MOD0_elim{m,p:int}(MOD0(m, p)): [q:nat] EQINT(m, p*q) //

// prfun lemma_PRIME_param{p:int}(PRIME(p)): [p >= 2] void // prfun mylemma1{n,p:int}(MOD0(n*n, p), PRIME(p)): MOD0(n, p) //

One may find that the following declaration in the implementation of mylemma_main looks mysterious:

Note that pfeq_mm_pnn is of the prop EQINT(m*m, p*(n*n)). Also, m equaling p*mPlease find on-line the entirety of an encoded proof showing that there exists no rational number whose square equals 2.

*Programming with Theorem-Proving* (PwTP) is a rich and broad
programming paradigm that allows cohesive construction of programs and
proofs in a syntactically intwined manner. The support for PwTP in ATS is a
signatory feature of ATS, and the novelty of ATS largely stems from it. For
people who are familiar with the so-called Curry-Howard isomorphism, I
emphasize that PwTP as is supported in ATS makes little, if any, essential
use of this isomorphism (between proofs and programs): The dynamics of ATS
in which programs are written is certainly not pure and the proofs encoded
in ATS/LF are not required to be constructive, either. However, that proof
construction in ATS can be done in a style of (functional) programming is
fundamentally important in terms of syntax design for ATS, for the need to
combine programs with proofs would otherwise be greatly more challenging.

In this chapter, I will present some simple but convincing examples to illustrate the power and flexibility of PwTP as is supported in ATS. However, the real showcase for PwTP will not arrive until after the introduction of linear types in ATS, when linear proofs can be combined with programs to track and safely manipulate resources such as memory and objects (e.g, file handles). In particular, PwTP is to form the cornersone of the support for imperative programming in ATS.

Please find on-line the code employed for illustration in this chapter plus some additional code for testing.

The constraint-solver of ATS is of rather diminished power. In particular, constraints containing nonlinear integer terms (e.g., those involving the use of multiplication (of variables)) are immediately rejected. This weakness must be properly addressed for otherwise it would become a crippling limitation on practicality of the type system of ATS. I now use a simple example to demonstrate how theorem-proving can be employed to circumvent the need for handling nonlinear constraints directly.

A function template list_concat is implemented as follows:

// // [list_concat] does typecheck in ATS2 // [list_concat] does not typecheck in ATS1 // fun{ a:t@ype } list_concat{m,n:nat} ( xss: list (list (a, n), m) ) : list (a, m * n) = case+ xss of | list_nil () => list_nil () | list_cons (xs, xss) => list_append<a> (xs, list_concat xss) // end of [list_concat]

fun{ a:t@ype } list_concat{m,n:nat} ( xss: list(list(a, n), m) ) : [p:nat] (MUL(m, n, p) | list(a, p)) = ( // case+ xss of | list_nil () => (MULbas() | list_nil()) | list_cons (xs, xss) => let val (pf | res) = list_concat (xss) in (MULind pf | list_append<a> (xs, res)) end // end of [list_cons] // ) (* end of [list_concat] *)

Internally, a matrix of the dimension m by n is represented as an array of the size m*n. For matrix subscripting, we need to implement a function template of the following interface:

fun{ a:t@ype } matrix_get {m,n:int}{i,j:nat | i < m; j < n} (A: arrayref (a, m*n), col: int n, i: int i, j: int j): (a) // end of [matrix_get]

implement {a}(*tmp*) matrix_get {m,n}{i,j} (A, n, i, j) = let // val (pf | _in_) = imul2 (i, n) // prval ((*void*)) = mul_elim(pf) prval ((*void*)) = mul_nat_nat_nat(pf) prval ((*void*)) = mul_gte_gte_gte{m-1-i,n}() // in A[_in_+j] end // end of [matrix_get]

// fun imul2{i,j:int} (int i, int j):<> [ij:int] (MUL(i, j, ij) | int ij) // prfun mul_elim {i,j:int}{ij:int} (pf: MUL(i, j, ij)): [i*j==ij] void // prfun mul_nat_nat_nat {i,j:nat}{ij:int} (pf: MUL(i, j, ij)): [ij >= 0] void // prfun mul_gte_gte_gte {m,n:int | m >= 0; n >= 0} ((*void*)): [m*n >= 0] void //

Note that there are a variety of proof functions declared in arith_prf.sats for helping prove theorems involving arithmetic operations. For examples of proof construction in ATS, please find the implementation of some of these proof functions in arith_prf.dats.

The entirety of the above presented code is available on-line.

The integer addition function can be assigned the following (dependent) type in ATS to indicate that it returns the sum of its two integer arguments:

This type gives a full specification of integer addition as the only (terminating) function that can be given the type is the integer addition function. However, the factorial function, which yields the product of the first n positive integers when applied to a natural number n, cannot be given the following type: as fact, which refers to the factorial function, does not exist in the statics of ATS. Evidently, a highly interesting and relevant question is whether a type can be formed in ATS that fully captures the functional relation specified by fact? The answer is affirmative. We can not only construct such a type but also assign it to a (terminating) function implemented in ATS.Let us recall that the factorial function can be defined by the following two equations:

Naturally, these equations can be encoded by the constructors associated with the dataprop FACT declared as follows:dataprop FACT(int, int) = | FACTbas(0, 1) | {n:nat}{r1,r:int} FACTind(n, r) of (FACT(n-1, r1), MUL(n, r1, r)) // end of [FACT]

// fun ifact {n:nat} .<n>. ( n: int(n) ) :<> [r:int] (FACT(n, r) | int r) = ( // if n = 0 then (FACTbas() | 1) else let val (pf1 | r1) = ifact (n-1) // pf1: FACT(n-1, r1) val (pfmul | r) = imul2 (n, r1) // pfmul: FACT(n, r1, r) in (FACTind(pf1, pfmul) | r) end // end of [else] // ) (* end of [ifact] *) //

Please find the entirety of the above presented code plus some testing code on-line.

The function ifact presented in the section on specifying with enhanced precision is a verified implementation of the factorial function as its type guarantees that ifact implements the specification of factorial encoded by the dataprop FACT. Clearly, the implementation of ifact closely follows the declaration of FACT. If we think of the latter as a logic program, then the former is essentially a functional version extracted from the logic program. However, the implementation of a specification in practice can often digress far from the specification algorithmically. For instance, we may want to have a verified implementation of factorial that is also tail-recursive. This can be done as follows:

fun ifact2 {n:nat} .<>. ( n: int (n) ) :<> [r:int] (FACT(n, r) | int r) = let fun loop {i:nat|i <= n}{r:int} .<n-i>. ( pf: FACT(i, r) | n: int n, i: int i, r: int r ) :<> [r:int] (FACT(n, r) | int r) = if n - i > 0 then let val (pfmul | r1) = imul2 (i+1, r) in loop (FACTind(pf, pfmul) | n, i+1, r1) end else (pf | r) // end of [if] // end of [loop] in loop (FACTbas() | n, 0, 1) end // end of [ifact2]

fun ifact2 (n) = let fun loop (n, i, r) = if n - i > 0 then let val r1 = (i+1) * r in loop (n, i+1, r1) end else r // end of [if] // end of [loop] in loop (n, 0, 1) end // end of [ifact2]

Please find on-line the entirety of the above presented code plus some testing code.

Given an integer x, pow(x, n), the nth power of x, can be defined inductively as follows:

A direct implementation of this definition is given as follows:fun ipow {n:nat} .<n>. (x: int, n: int n): int = if n > 0 then x * ipow (x, n-1) else 1 // end of [ipow]

fun ifastpow {n:nat} .<n>. ( x: int, n: int n ) : int = if n > 0 then let val n2 = half(n) val i2 = n-(2*n2) in if i2 > 0 then ifastpow (x*x, n2) else x * ifastpow (x*x, n2) end else 1 // end of [if] // end of [ifastpow]

Clearly, what is done above is not restricted to exponentiation on integers. As long as the underlying multiplication is associative, fast exponentiation can be employed to compute powers of any given element. In particular, powers of square matrices can be computed in this way. I now present as follows a verified generic implementation of fast exponentiation.

Handling generic data properly in a verified implementation often requires some finesse with the type system of ATS. Let us first introduce an abstract type constructor ELT as follows:

sortdef elt = int // [elt] is just an alias for [int] abst@ype ELT(a:t@ype, x:elt) = a // [x] is an imaginary stamp

// absprop MUL(elt, elt, elt) // abstract mul relation // fun {a:t@ype} mul_elt_elt{x,y:elt} (x: ELT(a, x), y: ELT(a, y)): [xy:elt] (MUL(x, y, xy) | ELT(a, xy)) // end of [mul_elt_elt] //

praxi mul_assoc {x,y,z:elt}{xy,yz:elt}{xy_z,x_yz:elt} ( MUL(x, y, xy), MUL(xy, z, xy_z), MUL(y, z, yz), MUL(x, yz, x_yz) ) : [xy_z==x_yz] void // end of [mul_assoc]

The abstract power function can be readily specified in terms of the abstract prop-type MUL:

dataprop POW ( elt(*base*), int(*exp*), elt(*res*) ) = // res = base^exp | {x:elt} POWbas(x, 0, 1(*unit*)) | {x:elt}{n:nat}{p,p1:elt} POWind(x, n+1, p1) of (POW(x, n, p), MUL(x, p, p1)) // end of [POW]

fun{a:t@ype} fastpow_elt_int{x:elt}{n:nat} (x: ELT(a, x), n: int n): [p:elt] (POW(x, n, p) | ELT(a, p)) // end of [fastpow_elt_int]

With the preparation done above, a straightforward implementation of fastpow_elt_int can now be presented as follows:

implement {a}(*tmp*) fastpow_elt_int (x, n) = let // (* lemma: (x*x)^n = x^(2n) *) extern prfun lemma {x:elt}{xx:elt}{n:nat}{y:elt} (pfxx: MUL(x, x, xx), pfpow: POW(xx, n, y)): POW(x, 2*n, y) // overload * with mul_elt_elt // [*] loaded with mul_elt_elt // in // if n = 0 then let val res = mulunit<a> () in (POWbas () | res) // res = 1 end // end of [then] else let val n2 = half n val (pfxx | xx) = x * x val (pfpow2 | res) = fastpow_elt_int<a> (xx, n2) // xx^n2 = res prval pfpow = lemma (pfxx, pfpow2) // pfpow: x^(2*n2) = res in if n=2*n2 then (pfpow | res) else let val (pfmul | xres) = x * res in (POWind(pfpow, pfmul) | xres) end // end of [else] end // end of [else] // end // end of [fastpow_elt_int]

// praxi mul_istot // MUL is total {x,y:elt} ((*void*)): [xy:elt] MUL(x, y, xy) // praxi mul_isfun // MUL is functional {x,y:elt}{z1,z2:elt}(MUL(x, y, z1), MUL(x, y, z2)): [z1==z2] void //

Please find on-line the two files fastexp.sats and fastexp.dats that contain the entirety of the above presented code.

Now we have implemented fastpow_elt_int. How can it be used? Please find on-line an example in which fastpow_elt_int is called to implement fast exponentiation on a 2-by-2 matrix so that the Fibonacci numbers can be computed in a highly efficient manner.

**Table of Contents**- 13. Introduction to Views and Viewtypes
- 14. Dataviews as Linear Dataprops
- 15. Dataviewtypes as Linear Datatypes
- 16. Abstract Views and Viewtypes

Probably the single greatest motivation behind the development of ATS is the desire to make ATS a programming language that can be employed effectively to construct safe and reliable programs running in the kernels of operating systems. Instead of following seemingly natural approaches that often focus on carving out a "safe" subset of C and/or put wrappers around "unsafe" programming features in C, ATS relies on the paradigm of programming with theorem-proving to prevent resources such as memory from being misused or mismanaged, advocating an approach to safety that is both general and flexible. For example, a well-typed program constructed in ATS cannot cause buffer overrun at run-time even though pointer arithmetic is fully supported in ATS. More specifically, if a pointer is to be dereferenced, ATS requires that a proof be given attesting to the safety of the dereferencing operation. Proofs of this kind are constructed to demonstrate the validity of linear propositions, which are referred to as views in ATS, for classifying resources as well as capabilities.

Please find on-line the code presented for illustration in this chapter.

A view is a linear version of prop, where the word *linear*
comes from linear logic, a resource-aware logic invented by Jean-Yves
Girard. There is a built-in sort view for static terms
representing views. Given a type T and a memory location L, a view of the
form T@L can be formed to indicate a value of the type T being stored in
the memory at the location L, where @ is a special infix
operator. Views of this form are extremely common in practice, and they
are often referred to as at-views. As an example, the following function
templates ptr_get0 and ptr_set0, which reads and
writes through a given pointer, are assigned types containing at-views:

// fun{a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): (a @ l | a) // fun{a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): (a @ l | void) //

Note that ptr is a type constructor that forms a type ptr(L) when applied to a static term L of the sort addr, and the only value of the type ptr(L) is the pointer that points to the location denoted by L.

Given a type T, the function ptr_get0<T> is assigned the following type:

which indicates that the function ptr_get0<T> returns a proof of the view T@L and a value of the type T when applied to a proof of the view T@L and a pointer of the type ptr(L) for some L. Intuitively speaking, a proof of the view T@L, which is a form of resource as T@L is linear, isSimilarly, the function ptr_set0<T> is assigned the following type:

Note that T? is a type for values of size sizeof(T) that are assumed to be uninitialized. The function ptr_set0<T> returns a proof of the view T@L when applied to a proof of the view T?@L, a pointer of the type ptr(L) and a value of the type T. The use of the view T?@L indicates that the memory location at L is assumed to be uninitialized when ptr_set0<T> is called.

As an example, a function template swap0 is implemented as follows for swapping memory contents at two given locations:

fn{a:t@ype} swap0{l1,l2:addr} ( pf1: a @ l1, pf2: a @ l2 | p1: ptr (l1), p2: ptr (l2) ) : (a @ l1, a @ l2 | void) = let val (pf1 | x1) = ptr_get0<a> (pf1 | p1) val (pf2 | x2) = ptr_get0<a> (pf2 | p2) val (pf1 | ()) = ptr_set0<a> (pf1 | p1, x2) val (pf2 | ()) = ptr_set0<a> (pf2 | p2, x1) in (pf1, pf2 | ()) end // end of [swap0]

Compared to a corresponding implementation in C, the verbosity of this one
in ATS is evident. In particular, the need for *threading*
linear proofs through calls to functions that make use of resources can
often result in a lot of *administrative* code to be written. I
now present some special syntax to significantly alleviate the need for
such administrative code.

The function templates ptr_get1 and ptr_set1 are given the following interfaces:

// fun{a:t@ype} ptr_get1 {l:addr} (pf: !a @ l >> a @ l | p: ptr l): a // fun{a:t@ype} ptr_set1 {l:addr} (pf: !a? @ l >> a @ l | p: ptr l, x: a): void //

fn{a:t@ype} swap1{l1,l2:addr} ( pf1: !a@l1, pf2: !a@l2 | p1: ptr l1, p2: ptr l2 ) : void = let val x = ptr_get1<a> (pf1 | p1) val () = ptr_set1<a> (pf1 | p1, ptr_get1<a> (pf2 | p2)) val () = ptr_set1<a> (pf2 | p2, x) in // nothing end // end of [swap1]

A further simplied implementation of swap1 is given as follows:

Given a pointer p of the type ptr(L) for some L, !p yields the value stored at the memory location L. The typechecker first searches for a proof of the view T@L for some T among all the currently available proofs when typechecking !p; if such a proof pf is found, then !p is essentially elaborated into ptr_get1(pf | p) and then typechecked. As !p is a left-value (which is to be explained later in detail), it can also be used to form an assignment like !p := v for some value v. The typechecker elaborates !p := v into ptr_set1(pf | p, v) for the sake of typechecking if a proof of the at-view T@L can be found for some type T among all the currently available proofs. Note that this implementation of swap1 makes no use of administrative code for handling linear proofs explicitly.
A linear type in ATS is given the name *viewtype*, which is
chosen to indicate that a linear type consists of two parts: one part for
views and the other for types. For instance, given a view V and a type T,
then the tuple (V | T) is a viewtype, where the bar symbol (|) is a
separator (just like a comma) to separate views from types. What seems a
bit surprising is the opposite: For each viewtype VT, we may assume the
existence of a view V and a type T such that VT is equivalent to (V |
T). Formally, this T can be referred as VT?! in ATS. This somewhat
unexpected interpretation of linear types is a striking novelty of ATS,
which stresses that the linearity of a viewtype comes *entirely*
from the view part residing within it.

The built-in sorts viewtype and viewt@ype are for static terms representing viewtypes whose type parts are of the sorts type and t@ype, respectively. In other words, the former is assigned to viewtypes for linear values of the size equal to that of a pointer and the latter to viewtypes for linear values of unspecified size. For example, tptr is defined as follows that takes a type and an address to form a viewtype (of the sort viewtype):

Given a type T and an address L, the viewtype tptr(T, L) is for a pointer to L paired with a linear proof stating that a value of the type T is stored at L. If we think of a counter as a pointer paired with a proof stating that the pointer points to an integer (representing the count), then the following defined function getinc returns the current count of a given counter after increasing it by 1:fn getinc {l:addr}{n:nat} ( cnt: !tptr (int(n), l) >> tptr (int(n+1), l) ) : int(n) = n where { val n = ptr_get1<int(n)> (cnt.0 | cnt.1) val () = ptr_set1<int(n+1)> (cnt.0 | cnt.1, n+1) } (* end of [getinc] *)

A particularly interesting example of a viewtype is the following one:

vtypedef cloptr (a:t@ype, b:t@ype, l:addr) = [env:t@ype] (((&env, a) -> b, env) @ l | ptr l) // end of [cloptr_app]

fun{ a:t@ype}{b:t@ype } cloptr_app {l:addr} ( pclo: !cloptr (a, b, l), x: a ) : b = let val p = pclo.1 (* // // taking out pf: ((&env, a) -> b, env) @ l // prval pf = pclo.0 // *) val res = !p.0 (!p.1, x) (* prval () = pclo.0 := pf // putting the proof pf back *) in res end // end of [cloptr]

The very ability to explain within ATS programming features such as closure function is a convincing indication of the expressiveness of the type system of ATS.

In its simplest form, a left-value is just a pointer paired with a linear
proof attesting to a value (of some type) being stored at the location to
which the pointer points. The name *left-value* stems from such a
value being allowed to appear on the left-hand side of an assignment
statement (in languages like C). Often, a left-value is intuitively
explained as a value with an address attached to it. Note that whatever
representation chosen for a left-value must make it possible to identify
both the pointer and the linear proof (of some at-view) that are associated
with the left-value.

In ATS, the simplest expression representing a left-value is !p, where ! is a special symbol and p a value of the type ptr(L) for some address L. When this expression is typechecked, a proof of T@L for some type T is required to be found among the currently available proofs. I will introduce additional forms of left values gradually.

The default strategy for passing a function argument in ATS is call-by-value. However, it is also allowed in ATS to specify that call-by-reference is chosen for passing a particular function argument. By call-by-reference, it is meant that the argument to be passed must be a left-value and what is actually passed is the address of the left-value (instead of the value stored at the address). For example, the following defined function swap2 makes essential use of call-by-reference:

fn{ a:t@ype } swap2 ( x1: &a, x2: &a ) : void = let val tmp = x1 in x1 := x2; x2 := tmp end // end of [swap2]

fn{ a:t@ype } swap1{l1,l2:addr} ( pf1: !a @ l1, pf2: !a @ l2 | p1: ptr l1, p2: ptr l2 ) : void = swap2 (!p1, !p2)

Given a type T and an integer N, the syntax @[T][N] stands for a flat array consisting N elements of the type T. Please note that a value of the type @[T][N] is of the size N*sizeof(T). If a function has a parameter representing an array, then this parameter is most liklely call-by-reference. For instance, the following code implements a function that takes two arrays of doubles to compute their dot product (also knowns as inner product):

Note that both array arguments of dotprod are call-by-reference.Given a type T and an address L, how can a proof of the view T@L be obtained in the first place? There are actually a variety of methods for obtaining such proofs in practice, and I present one as follows that is based on stack-allocation of local variables.

In the body of the following function foo, some stack-allocated local variables are declared:

fn foo (): void = let var x0: int // view@(x0): int? @ x0 val () = x0 := 0 // view@(x0): int(0) @ x0 var x1: int = 1 // view@(x1): int(1) @ x1 // // [with] is a keyword in ATS // var y: int with pfy // pfy is an alias of view@(y): int? @ y val () = y := 2 // pfy = view@(y): int(2) @ y var z: int with pfz = 3 // pfz is an alias of view@(z): int(3) @ z in // nothing end // end of [foo]

The keyword var is for declaring a local variable. When a variable is declared, either its type or its initial value needs to be given. If a variable is declared without a type, then the type of its initial value is assumed to be its type. Assume that a variable x is declared of type T. Then the pointer to the location of the variable is denoted by addr@(x), where addr@ is a keyword, and its associated linear proof (of some at-view) can be referred to as view@(x), where view@ is a keyword. A variable is another form of left-value in ATS. In the body of foo, x0 is declared to be a variable of the type int and then it is initialized with the integer 0; x1 is declared to be a variable of the type int that is given the initial value 1; y is declared to be a variable of the type int while pfy is introduced as an alias for view@(y), and then y is initialized with the integer 2; z is declared to be a variable of the type int that is given the initial value 3 while pfz is introduced as an alias for view@(z).

The following code gives an implementation of the factorial function:

fn fact{n:nat} (n: int (n)): int = let fun loop{n:nat}{l:addr} .<n>. (pf: !int @ l | n: int n, res: ptr l): void = if n > 0 then let val () = !res := n * !res in loop (pf | n-1, res) end // end of [if] // end of [loop] var res: int with pf = 1 val () = loop (pf | n, addr@res) // addr@res: the pointer to res in res end // end of [fact]

Note that the variable res holds the intermediate result during the execution of the loop. As res is stack-allocated, there is no garbage generated after a call to fact is evaluated. When this style of programming is done in C, there is often a concern about the pointer to res being derefenced after a call to fact returns, which is commonly referred to as derefencing a dangling pointer. This concern is completely eliminated in ATS as it is required by the type system of ATS that a linear proof of the at-view associated with the variable res be present at the end of legal scope for res. More specifically, if x is a declared variable of the type T, then a linear proof of the view T?@L, where L is the address of x, must be available when typechecking reaches the end of the scope for x. This requirement ensures that a variable can no longer be accessed after the portion of the stack in which it is allocated is reclaimed as no linear proof of the at-view associated with the variable is ever available from that point on.

Arrays in ATS can also be stack-allocated. For instance, the following code allocates two arrays of doubles in the frame of the function main0 and then passes them to dotprod to compute their dot product:

implement main0 () = { // var A = @[double][3](1.0) // initialized with 1.0, 1.0, 1.0 var B = @[double](1.0, 2.0, 3.0) // initialized with 1.0, 2.0, 3.0 // val () = println! ("A * B = ", dotprod (A, B)) // A * B = 6.0 // } (* end of [main0] *)

Note that allocating large arrays in the call frame of a function may not be a good practice as doing so can greatly increase the likelihood of stack-overflow at run-time.

It is also allowed in ATS to allocate a closure in the call frame of a function. For instance, the following code implements a function named foo that stores a flat closure-function in a stack-allocated variable named bar:

fun foo ( x: int, y: int ) : int = let // var bar = lam@ (): int => x * y // in bar () end // end of [foo]

fun foo2 ( x: int, y: int ) : int = let // var bar2 = fix@ f (x: int): int => if x > 0 then y + f(x-1) else 0 // in bar2 (x) end // end of [foo]

In a setting where dynamic memory allocation is not allowed, stack-allocated closures can play a pivotal role in supporting programming with higher-order functions.

In ATS, a closure-function can be assiged a linear type, allowing it to be properly tracked within the type system and also explicitly freed by the programmer.

The following code implements a higher-order function list_map_cloptr which takes a linear closure-function as its second argument:

fun{ a:t@ype}{b:vt@ype } list_map_cloptr{n:int} ( xs: list (a, n), f: !(a) -<cloptr1> b ) : list_vt (b, n) = ( case+ xs of | list_nil () => list_vt_nil () | list_cons (x, xs) => list_vt_cons (f (x), list_map_cloptr<a><b> (xs, f)) )

Let us now see some concrete code in which a linear closure-function is created, called, and finally freed:

implement main0 () = { // val xs = $list_vt{int}(0, 1, 2, 3, 4) // val len = list_vt_length (xs) // val f = lam (x: int): int =<cloptr1> x * len // val ys = list_map_cloptr<int><int> ($UNSAFE.list_vt2t(xs), f) // val () = cloptr_free($UNSAFE.castvwtp0{cloptr(void)}(f)) // val () = println! ("xs = ", xs) // xs = 0, 1, 2, 3, 4 val () = println! ("ys = ", ys) // ys = 0, 5, 10, 15, 20 // val ((*freed*)) = list_vt_free (xs) val ((*freed*)) = list_vt_free (ys) // } (* end of [main0] *)

The support for linear closure-functions in ATS1 is crucial in a setting where higher-order functions are needed but run-time garbage collection (GC) is not allowed or supported. In ATS2, linear closure-functions become much less important as programming with higher-order functions in a setting without GC can be more conveniently achieved through the use of templates. However, if one wants to store closure-functions in a data structure without causing memory leaks, it is necessary to use linear closure-functions unless GC can be relied upon to reclaim memory.

The at-views of the form T@L for types T and addresses L are building blocks for constructing other forms of views. One mechanism for putting together such building blocks is by declaring dataviews, which is mostly identical to declaring dataprops. I now present in this chapter some commonly encountered dataviews and their uses.

Please find on-line the code presented for illustration in this chapter.

The dataview option_v is declared as follows:

This declaration indicates that the dataview option_v is covariant in its first argument and there are two proof constructors associated with it: Some_v and None_v. Given a view V, option_v(V, b) is often called an optional view, where b is a boolean. Clearly, a proof of the view option_v(V, true) contains a proof of the view V while a proof the view option_v(V, false) contains nothing.As an example, the following function interface involves a typical use of optional view:

Given a type T, the function ptr_alloc_opt<T> returns a pointer paired with a proof of an optional view; if the returned pointer is not null, then the proof can be turned into a proof of the view T?@L, where L is the location to which the pointer points; otherwise, there is no at-view associated with the returned pointer.The dataview VOR is declared as follows:

dataview VOR (v0:view+, v1:view+, int) = | VORleft (v0, v1, 0) of (v0) | VORright (v0, v1, 1) of (v1)

Let T be some type. The following function interface states that getopt takes an unintialized pointer and returns an integers indicating whether the pointer is initialized:

The following code shows a typical use of getopt:fun foo (): void = let var x: T? val (pfor | i) = getopt (view@(x) | addr@(x)) in // if i = 0 then let prval VORleft (pf0) = pfor in view@(x) := pf0 // uninitialized end // end of [then] else let prval VORright (pf1) = pfor in view@(x) := pf1 // initialized end // end of [else] // end of [if] // end // end of [foo]

In ATS, there is a type constructor opt that takes a type T and a boolean B to form an opt-type opt(T, B) such that opt(T, B) equals T if B is true and it equals T? if B is false. The function getopt can be given the following interface that makes use of an opt-type:

The code that calls getopt can now be implemented as follows: where the proof functions opt_unsome and opt_unnone are assgined the following types: Compared to the version that uses VOR, this version based on opt-type is considerably less verbose.
Unlike in most programming languages, arrays are not a primitive data
structure in ATS. More specifically, persistent arrays can be implemented
based on linear arrays, which allow for being freed safely by the
programmer, and linear arrays can be implemented based on
at-views. Intuitively, the view for an array storing N elements of type
T consists of N at-views: T@L_{0}, T@L_{1}, ..., and
T@L_{N-1}, where L_{0} is the starting address of the array and
each subsequent L equals the previous one plus the size of T, that is, the
number of bytes needed to store a value of the type T. The following
declared dataview array_v precisely captures this intuituion:

dataview array_v ( a:t@ype+ // covariant argument , addr(*beg*) , int(*size*) ) = // array_v | {l:addr} array_v_nil (a, l, 0) | {l:addr}{n:nat} array_v_cons (a, l, n+1) of (a @ l, array_v (a, l+sizeof(a), n)) // end of [array_v]

Given a type T, an address L and an integer N, array_v(T, L, N) is a view for the array starting at L that stores N elements of the type T. As can be readily expected, the function templates for array-accessing and array-updating are given the following interfaces:

// fun{ a:t@ype } arrget{l:addr}{n,i:nat | i < n} (pf: !array_v (a, l, n) | p: ptr l, i: int i): a // end of [arrget] // end of [fun] // fun{ a:t@ype } arrset{l:addr}{n,i:nat | i < n} (pf: !array_v (a, l, n) | p: ptr l, i: int i, x: a): void // end of [arrset] // end of [fun] //

Before implementing arrget and arrset, I present as follows some code that implements a function template to access the first element of a nonempty array:

fun{ a:t@ype } arrgetfst{l:addr}{n:pos} ( pf: !array_v (a, l, n) | p: ptr l ) : a = x where { prval array_v_cons (pf1, pf2) = pf // pf1: a @ l; pf2: array_v (a, l+sizeof(a), n-1) val x = !p prval () = pf := array_v_cons (pf1, pf2) } // end of [arrgetfst]

Obviously, the function template arrget can be implemented based on arrgetfst:

implement {a}(*tmp*) arrget (pf | p, i) = if i > 0 then let prval array_v_cons (pf1, pf2) = pf val x = arrget (pf2 | ptr_succ<a> (p), i-1) prval () = pf := array_v_cons (pf1, pf2) in x end else arrgetfst (pf | p) // end of [if]

This is a tail-recursive implementation of time-complexity O(n). However, the very point of having arrays is to support O(1)-time accessing and updating operations. My initial effort spent on implementing such operations immediately dawned on me the need to construct proof functions for supporting view-changes (of no run-time cost).

Clearly, an array starting at L that stores N elements of type T can also be thought of as two arrays: one starting at L that stores I elements while the other starting at L+I*sizeof(T) that stores N-I elements, where I is an natural number less that or equal to N. Formally, this statement can be encoded in the type of the proof function array_v_split:

prfun array_v_split {a:t@ype} {l:addr}{n,i:nat | i <= n} ( pfarr: array_v (a, l, n) ) : (array_v (a, l, i), array_v (a, l+i*sizeof(a), n-i))

The other direction of the above statement can be encoded in the type of the proof function array_v_unsplit:

prfun array_v_unsplit {a:t@ype} {l:addr}{n1,n2:nat} ( pf1arr: array_v (a, l, n1), pf2arr: array_v (a, l+n1*sizeof(a), n2) ) : array_v (a, l, n1+n2)

With array_v_split and array_v_unsplit, we can readily give implementations of arrget and arrset that are O(1)-time:

implement {a}(*tmp*) arrget{l}{n,i} (pf | p, i) = x where { prval (pf1, pf2) = array_v_split{a}{l}{n,i}(pf) prval array_v_cons (pf21, pf22) = pf2 val x = ptr_get1<a> (pf21 | ptr_add<a> (p, i)) prval pf2 = array_v_cons (pf21, pf22) prval () = pf := array_v_unsplit{a}{l}{i,n-i}(pf1, pf2) } (* end of [arrget] *) implement {a}(*tmp*) arrset{l}{n,i} (pf | p, i, x) = () where { prval (pf1, pf2) = array_v_split{a}{l}{n,i}(pf) prval array_v_cons (pf21, pf22) = pf2 val () = ptr_set1<a> (pf21 | ptr_add<a> (p, i), x) prval pf2 = array_v_cons (pf21, pf22) prval () = pf := array_v_unsplit{a}{l}{i,n-i}(pf1, pf2) } (* end of [arrset] *)

Of course, the proof functions array_v_split and array_v_split are still to be implemented, which I will do when covering the topic of view-change.

Given a type T, an address L and a natural number N, a proof of the view array_v(T?, L, N) can be obtained and released by calling the functions malloc and free, respectively, which are to be explained in details elsewhere. I now give as follows an implemention of a function template for array intialization:

typedef natLt (n:int) = [i:nat | i < n] int (i) fun{a:t@ype} array_ptr_tabulate {l:addr}{n:nat} ( pf: !array_v (a?,l,n) >> array_v (a,l,n) | p: ptr (l), n: int (n), f: natLt(n) -<cloref1> a ) : void = let fun loop{l:addr} {i:nat | i <= n} .<n-i>. ( pf: !array_v (a?,l,n-i) >> array_v (a,l,n-i) | p: ptr l, n: int n, f: natLt(n) -<cloref1> a, i: int i ) : void = if i < n then let prval array_v_cons (pf1, pf2) = pf val () = !p := f (i) val () = loop (pf2 | ptr_succ<a> (p), n, f, i+1) in pf := array_v_cons (pf1, pf2) end else let prval array_v_nil () = pf in pf := array_v_nil {a} () end // end of [if] // end of [loop] in loop (pf | p, n, f, 0) end // end of [array_ptr_tabulate]

Given a natural number n, the type natLt(n) is for all natural numbers less than n. Given a type T, the function array_ptr_tabulate<T> takes a pointer to an uninitialized array, the size of the array and a function f that maps each natural number less than n to a value of the type T, and it initializes the array with the sequence of values of f(0), f(1), ..., and f(n-1). In other words, the array stores a tabulation of the given function f after the initialization is over.

Given a type T and an integer N, @[T][N] is a built-in type in ATS for N consecutive values of the type T. Therefore, the at-view @[T][N]@L for any given address L is equivalent to the array-view array_v(T, L, N). By making use of the feature of call-by-reference, we can also assign the following interfaces to the previously presented functions arrget and arrset:

// fun{ a:t@ype } arrget {n,i:nat | i < n} (A: &(@[a][n]), i: int i): (a) // fun{ a:t@ype } arrset {n,i:nat | i < n} (A: &(@[a][n]), i: int i, x: a): void //

Please find the entirety of the above presented code on-line.

The following dataview strbuf_v captures the notion of a string in C, which consisits a sequence of non-null characters followed by the null character:

dataview strbuf_v(addr, int) = | {l:addr} strbuf_v_nil(l, 0) of (char(0) @ l) | {l:addr}{n:nat} strbuf_v_cons(l, n+1) of (charNZ @ l, strbuf_v(l+sizeof(char), n))

Given a C-string, one can always access its first character; if the character is null, then the C-string is empty; if it is not, then the C-string is non-empty. The following implementation of strptr_is_nil precisely follows this simple way of testing whether a C-string is empty or not:

// fun strptr_is_nil {l:addr}{n:int} ( str: !strptr(l, n) ) : bool(n==0) = let // prval (pf_at, fpf) = strbuf_v_getfst(str.0) // prval val c0 = !(str.1) prval () = str.0 := fpf(pf_at) in iseqz(c0) // testing whether [c0] is null end // end of [strptr_is_nil] //

extern prfun strbuf_v_getfst {l:addr}{n:int} ( pf: strbuf_v(l, n) ) : [ c:int | (c==0 && n==0) || (c != 0 && n > 0) ] (char(c) @ l, char(c) @ l -<lin,prf> strbuf_v(l, n)) (* ****** ****** *) primplmnt strbuf_v_getfst (pf) = ( case+ pf of | strbuf_v_nil(pf_at) => #[.. | (pf_at, llam(pf_at) => strbuf_v_nil(pf_at))] | strbuf_v_cons(pf_at, pf2) => #[.. | (pf_at, llam(pf_at) => strbuf_v_cons(pf_at, pf2))] )

The following implementation gives another example of handling the dataview strbuf_v:

fun strptr_length {l:addr}{n:int} ( str: !strptr(l, n) ) : size_t(n) = let // fun loop {l:addr} {i,j:int} ( pf: !strbuf_v(l, i) | p0: ptr(l), j: size_t(j) ) : size_t(i+j) = let // prval [c:int] (pf_at, fpf) = strbuf_v_getfst(pf) // val c0 = !p0 // prval ((*return*)) = pf := fpf(pf_at) // in // if iseqz(c0) then j else res where { prval strbuf_v_cons(pf_at, pf2) = pf val res = loop(pf2 | ptr_succ<char>(p0), succ(j)) prval ((*folded*)) = pf := strbuf_v_cons(pf_at, pf2) } (* end of [else] *) // end // end of [loop] // in loop(str.0 | str.1, i2sz(0)) end // end of [strptr_length]

Please find the entirety of the above presented code on-line.

The following dataview slseg_v captures the notion of a singly-linked list segment:

dataview slseg_v ( a:t@ype+ // covariant argument , addr(*beg*) , addr(*end*) , int(*length*) ) = // slseg_v | {l:addr} slseg_v_nil (a, l, l, 0) of () | {l_fst:agz}{l_nxt,l_end:addr}{n:nat} slseg_v_cons (a, l_fst, l_end, n+1) of ((a, ptr l_nxt) @ l_fst, slseg_v (a, l_nxt, l_end, n)) // end of [slseg]_v

// slseg_v_nil : {a:t@ype}{l:addr} () -> slseg_v (a, l, l, 0) // slseg_v_cons : {a:t@ype}{l_fst:agz}{l_nxt,l_end:addr}{n:nat} ((a, ptr l_nxt) @ l_fst, slseg_v (a, l_nxt, l_end, n)) -> slseg_v (a, l_fst, l_end, n+1) //

Note that agz is a subset sort for addresses that are not null. Given a type T, two addresses L1 and L2, and a natural number N, the view slseg_v(T, L1, L2, N) is for a singly-linked list segment containing N elements of the type T that starts at L1 and finishes at L2. In the case where L2 is the null pointer, then the list segment is considered a list as is formally defined below:

Given a type T, a pointer pointing to L plus a proof of the view slist_v(T, L, N) for some natural number N is essentially the same as a pointer to a struct of the following declared type slist_struct in C:

typedef struct slist { T data ; /* [T] matches the corresponding type in ATS */ struct slist *next ; /* pointing to the tail of the list */ } slist_struct ;

Let us now see a simple example involving singly-linked lists:

fn{a:t@ype} slist_ptr_length {l:addr}{n:nat} ( pflst: !slist_v (a, l, n) | p: ptr l ) : int (n) = let fun loop {l:addr}{i,j:nat} .<i>. ( pflst: !slist_v (a, l, i) | p: ptr l, j: int (j) ) : int (i+j) = if p > 0 then let prval slseg_v_cons (pfat, pf1lst) = pflst val res = loop (pf1lst | !p.1, j+1) // !p.1 points to the tail prval () = pflst := slseg_v_cons (pfat, pf1lst) in res end else let // the length of a null list is 0 prval slseg_v_nil () = pflst in pflst := slseg_v_nil (); j end (* end of [if] *) // end of [loop] in loop (pflst | p, 0) end // end of [slist_ptr_length]

int slist_ptr_length ( slist_struct *p ) { int res = 0 ; while (p != NULL) { res = res + 1 ; p = p->next ; } return res ; } // end of [slist_ptr_length]

As another example, the following function template slist_ptr_reverse turns a given linked list into its reverse:

fn{a:t@ype} slist_ptr_reverse {l:addr}{n:nat} ( pflst: slist_v (a, l, n) | p: ptr l ) : [l:addr] (slist_v (a, l, n) | ptr l) = let fun loop {n1,n2:nat} {l1,l2:addr} .<n1>. ( pf1lst: slist_v (a, l1, n1) , pf2lst: slist_v (a, l2, n2) | p1: ptr l1, p2: ptr l2 ) : [l:addr] (slist_v (a, l, n1+n2) | ptr l) = if p1 > 0 then let prval slseg_v_cons (pf1at, pf1lst) = pf1lst val p1_nxt = !p1.1 val () = !p1.1 := p2 in loop (pf1lst, slseg_v_cons (pf1at, pf2lst) | p1_nxt, p1) end else let prval slseg_v_nil () = pf1lst in (pf2lst | p2) end // end of [if] in loop (pflst, slseg_v_nil | p, the_null_ptr) end // end of [slist_ptr_reverse]

slist_struct* slist_ptr_reverse ( slist_struct *p ) { slist_struct *tmp, *res = NULL ; while (p != NULL) { tmp = p->next ; p->next = res ; res = p ; p = tmp ; } return res ; } // end of [slist_ptr_reverse]

Let us see yet another example. List concatenation is a common operation on lists. This time, we first give an implementation of list concatenation in C:

slist_struct* slist_ptr_append (slist_struct *p, slist_struct *q) { slist_struct *p1 = p ; if (p1 == NULL) return q ; while (p1->next != NULL) p1 = p1->next ; p1->next = q ; return p ; } // end of [slist_ptr_append]

fn{a:t@ype} slist_ptr_append {l1,l2:addr}{n1,n2:nat} ( pf1lst: slist_v (a, l1, n1) , pf2lst: slist_v (a, l2, n2) | p1: ptr l1, p2: ptr l2 ) : [l:addr] (slist_v (a, l, n1+n2) | ptr l) = let fun loop {n1,n2:nat} {l1,l2:addr | l1 > null} .<n1>. ( pf1lst: slist_v (a, l1, n1) , pf2lst: slist_v (a, l2, n2) | p1: ptr l1, p2: ptr l2 ) : (slist_v (a, l1, n1+n2) | void) = let prval slseg_v_cons (pf1at, pf1lst) = pf1lst val p1_nxt = !p1.1 in if p1_nxt > 0 then let val (pflst | ()) = loop (pf1lst, pf2lst | p1_nxt, p2) in (slseg_v_cons (pf1at, pflst) | ()) end else let val () = !p1.1 := p2 prval slseg_v_nil () = pf1lst in (slseg_v_cons (pf1at, pf2lst) | ()) end (* end of [if] *) end // end of [loop] in if p1 > 0 then let val (pflst | ()) = loop (pf1lst, pf2lst | p1, p2) in (pflst | p1) end else let prval slseg_v_nil () = pf1lst in (pf2lst | p2) end (* end of [if] *) end // end of [slist_ptr_append]

In the above examples, it is evident that the code in ATS is a lot more verbose than its counterpart in C. However, the former is also a lot more robust than the latter in the following sense: If a minor change is made to the code in ATS (e.g., renaming identifiers, reordering function arguments), it is most likely that a type-error is to be reported when the changed code is typechecked. On the other hand, the same thing cannot be said about the code written in C. For instance, the following erroneous implementation of slist_ptr_reverse in C is certainly type-correct:

/* ** This implementation is *incorrect* but type-correct: */ slist_struct* slist_ptr_reverse (slist_struct *p) { slist_struct *tmp, *res = NULL ; while (p != NULL) { tmp = p->next ; res = p ; p->next = res ; p = tmp ; } return res ; } // end of [slist_ptr_reverse]

I now point out that the dataview slseg_v is declared here in a manner that does not address the issue of allocating and freeing list nodes, and it is done so for the sake of a less involved presentation. A dataview for singly-linked lists that does handle allocation and deallocation of list nodes can also be declared in ATS, but there is really little need for it as we can declare a dataviewtype for such lists that is far more convenient to use. However, dataviews are fundamentally more general and flexible than dataviewtypes, and there are many common data structures (e.g. doubly-linked lists) that can only be properly handled with dataviews in ATS.

By the phrase *view-change*, I mean applying a function to
proofs of a set of views to turn them into proofs of another set of views.
As this function itself is a proof function, there is no run-time cost
associated with each view-change. For instance, a proof of the at-view
int32@L for any address L can be turned into a proof of a tuple of 4
at-views: int8@L, int8@L+1, int8@L+2 and int8@L+3, where int32 and int8 are
types for 32-bit and 8-bit integers, respectively. Often more interesting
view-changes involve recursively defined proof functions, and I present
several of such cases in the rest of this section.

When implementing an array subscripting operation of O(1)-time, we need a proof function to change the view of one array into the views of two adjacently located arrays and another proof function to do precisely the opposite. Formally speaking, we need to construct the following two proof functions array_v_split and array_v_unsplit:

// prfun array_v_split {a:t@ype} {l:addr}{n,i:nat | i <= n} ( pfarr: array_v (a, l, n) ) : (array_v (a, i, l), array_v (a, n-i, l+i*sizeof(a))) // prfun array_v_unsplit {a:t@ype} {l:addr}{n1,n2:nat} ( pf1arr: array_v (a, l, n1), pf2arr: array_v (a, l+n1*sizeof(a), n2) ) : array_v (a, l, n1+n2) //

An implementation of array_v_split is given as follows:

primplmnt array_v_split {a}{l}{n,i}(pfarr) = let prfun split {l:addr}{n,i:nat | i <= n} .<i>. ( pfarr: array_v (a, l, n) ) : ( array_v (a, l, i) , array_v (a, l+i*sizeof(a), n-i) ) = sif i > 0 then let prval array_v_cons (pf1, pf2arr) = pfarr prval (pf1res1, pf1res2) = split{..}{n-1,i-1} (pf2arr) in (array_v_cons (pf1, pf1res1), pf1res2) end else let prval EQINT () = eqint_make{i,0}((*void*)) in (array_v_nil (), pfarr) end // end of [sif] in split (pfarr) end // end of [array_v_split]

Note that the keyword primplmnt (instead of implement) should be used for implementing proof functions. One can also choose to use the keyword primplement in place of primplmnt. Clearly, the proof function split directly encodes a proof based on mathematical induction. Following is an implementation of array_v_unsplit: