# ATS: Programming with Theorem-Proving/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 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 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 non-tail 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