ATS: Programming with Theorem-Proving/Language Basics

Primitive Types

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.14F is a float.

Functions

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

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

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

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 non-recursive 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 accumulator
    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 non-tail recursive function can be converted to tail recursive.

Simple Control Flow: if - then - else

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

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

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 circumference( radius: float ): float = radius * 2 * pi

We can't use pi from area, so our implementation is an error; but we can use it from circumference.
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 circumference = pi * 2 * radius
end