ATS: Programming with TheoremProving/Language Basics
Contents
Primitive Types[edit]
Primitive types in ATS are basically a representation of primitive C types. Every type in ATS can be mapped to a type in C. The mapping is as follows:
ATS type  C type 

void 
void

bool 
int

char 
char

schar 
signed char

uchar 
unsigned char

int 
int

uint 
unsigned int

lint 
long int

ulint 
unsigned long int

llint 
long long int

ullint 
unsigned long long int

float 
float

double 
double

size_t 
size_t

string 
string

The mapping of these types can be found in the file ats_types.h
.
Note that type literals work in the same way as C, so 3.14
is a double, whereas 3.14
is a float.
Functions[edit]
Functions are declared by the keyword fn
. The generic format of a function is:
fn functionName( param_1: type_1, param_2: type_2,..., param_n: type_n ): return_type = function_body
A function doesn't have a return statement, but rather the function body is an expression that evaluates to the return value. So for example, a function to add two values would be something like:
fn add( operand1: int, operand2: int ) = int1 + int2
Recursive Functions[edit]
A functions that calls itself is a recursive functions. Recursive functions have the same structure as generic functions, with the only difference that the keyword fun
replaces the keyword fn
. An example of recursive function is a function to compute the Fibonacci value:
fun fibonacci( n: int ): int =
if ( n > 2 ) then fibonacci( n  1 ) + fibonacci( n  2 ) else n
Tail Recursion[edit]
A special case of recursion is tail recursion. This happens when the return value of the recursive call is used as return value of the calling function. For example:
fun even( n: int ): bool =
if ( n == 0 ) then true
else if ( n == 1 ) then false
else even( n  2 )
The function even
tells if a number is even. The return value of even
can be true
, false
, or the value returned by the call to even( n  2 )
. Because the return value of the call is returned without further processing, the recursive call to even( n  2 )
is a tail recursive call.
Tail recursion is particularly important, because it allows, thanks to an approach known as tail call optimization, to be converted to loops. This means that there is no performance loss due to function calls, and tail recursion can be as fast as a for or while loop.
Improving Tail Recursive Functions with Accumulators[edit]
Recursive functions offer an elegant programming style, but they have a problem: for every call some data is put into the stack. This means that potentially, when the recursive function calls itself a lot of times, a stack overflow exception occurs. Tail recursion has theoretically the same problem, however, because of tail call optimization, the problem doesn't occur in practice; tail recursive functions are stack overflow free.
Considering the privileged status of tail recursion, an obvious question is whether it is possible to always use recursive functions instead of nonrecursive ones. It turns out that any algorithm is implementable with tail recursion by adding extra parameters, called accumulators, to the recursive function. The purpose of these parameters is to accumulate information from the previous calls (hence the name), and carry it across different recursive calls.
For example, considering the code to implement the factorial:
fun factorial( n: int ): int =
if ( n == 1 ) then 1
else n * factorial( n  1 )
This is an obvious implementation of the factorial, and it's recursive, but not tail recursive. To create a tail recursive version we add an accumulator to our function; this accumulator will contain the value of the factorial calculated so far:
fun factorial2( n: int, accumulator: int ): int =
if ( n == 1 ) then 1
else factorial( n  1, accumulator * n )
Now, because we need our factorial function to have only one parameter, we add an extra function, which will be our factorial function, to initialize the accumulator and start the recursion:
fn factorial( n: int ): int =
factorial2( n  1, accumulator * n )
With the help of accumulators any nontail recursive function can be converted to tail recursive.
Simple Control Flow: if  then  else
[edit]
Control Flow in ATS, like in other functional programming languages, is mostly implemented in a different way from languages that follow structured programming. But there is a classic construct that has exactly the same structure in ATS as in imperative languages: if  then  else
. The general structure is:
if boolean_expression then
 expression1
else
 expression2
fn factorial( n: int ): int =
factorial2( n  1, accumulator * n )
Bindings[edit]
A binding is a constant value that is defined using the result of an expression. It can be compared to const
in C/C++ or final
in Java. A binding in ATS is declared using the keyword val
. Example of bindings could be val foo = 1
or val bar = 2 * 2
. The name binding comes from the fact that we bind the names foo
and bar
to the expressions 1
and 2 * 2
. A binding can also be defined using other bindings:
val x = 10
val square = x * x
In this case x
will obviously be initialized before square
.
Note that the bindings declared don't have a type. In fact, a binding declared with val
will take its type from the expression it is bound to. It is possible to be more strict, and explicitly set a type for a binding. For example, the binding val pi = 3.14
defines a double, as the expression 3.14
is by default a double. If we write val pi = 3.14f
then pi
will be a float. It is possible to say that pi
must be a float in any case, by saying val pi: float = 3.14
. If you assign an incompatible type, for example, in val pi: char = 3.14
, a compilation error will occur.
A similar, but slightly different, situation, is the assignment of a type not to a binding but to an expression. This can be achieved by writing something like val pi = 3.14: float
. In this case the float type is given to the expression. So, while at the end our binding will always be a float, the process is slightly different.
Binding Scopes[edit]
Bindings are visible within some specific boundaries. These boundaries define the scope of the binding. Within the scope, the binding can be declared, initialized, and used.
The highest level for a scope is the top level: at this level the binding is not located within a function, and it is visible in all points of a file, starting from the point where the binding is declared:
fn area( radius: float): float = radius * radius * pi
val pi = 3.14
fn circle( radius: float ): flost = radius * 2 * pi
We can't use pi
from area
, so our implementation is an error; but we can use it from circle
.
At a lower level we have local bindings, which are defined within a segment of code. Local bindings can be used in two ways.
The first way is as a help to evaluate expressions. In this case the name used in the binding can be used to form other expressions. The generic structure in this case is:
val expression_name = let
 val name_1 = value_1 and name_2 = value_2 and ... and name_n = value_n in expression_to_evaluate
end
What we have in this case it that the different names name_1
,...,name_n
are used to evaluate the expression expression_to_evaluate
. That is, the bindings are valid between the in
and the end
. For example:
val area = let
val pi = 3.14 and radius = 10 in pi * radius * radius
end
A different construct but with similar results is the following:
val expression_name = expression_to_evaluate where {
val name_1 = value_1 and name_2 = value_2 and ... and name_n = value_n
} end
In this case we first define the expression and the declare the bindings. The bindings are effective between the '=
' and the where
. So the example above becomes:
val area = pi * radius * radius where {
pi = 3.14 and radius = 10
} end
The second way is to define one or more toplevel bindings:
local val name_1 = value_1 and name_2 = value_2 and ... and name_n = value_n in val expression_name = expression_to_evaluate end
Although the local bindings can be used only between the 'in
' and the end
, the binding of the resulting expression is a toplevel binding. So, for example:
local
val pi = 3.14 and radius = 10
in
val area = pi * radius * radius
val circle = pi * 2 * radius
end