Some Basics on ATS

ATS consists of a static component (statics), where types are formed and reasoned about, and a dynamic component (dynamics), where programs are constructed and evaluated.

Some Primitive Sorts and Constants

The statics of ATS is a simply typed language. The types for terms in the statics are called sorts (so as to avoid potential confusion with the types for terms in the dynamics) and the terms in it are called static terms. We use sigma (or $srt) for sorts and s (or $strm) for static terms. The primitive sorts in ATS include bool, char, int, prop, type, view and viewtype.

There are also some primitive constants c in the statics, each of which is assigned a constant sort (or c-sort, for short) of the following form:

(sigma_1,...,sigma_n) => sigma

Intuitively, given static terms s_1,...,s_n of sorts sigma_1,...,sigma_n, respectively, c(s_1,...,s_n) is a static term of sort sigma if c is assigned the c-sort (sigma_1,...,sigma_n) => sigma. For instance, each boolean value is given the sort () => bool and each integer is given the c-sort () => int. In the following table, we list some of the commonly used constants in the statics of ATS:

~   :   (int) => int
+   :   (int, int) => int
-   :   (int, int) => int
*   :   (int, int) => int
/   :   (int, int) => int
<   :   (int, int) => bool
<=   :   (int, int) => bool
>   :   (int, int) => bool
>=   :   (int, int) => bool
==   :   (int, int) => bool
<>   :   (int, int) => bool
~   :   (bool) => bool
&&   :   (bool, bool) => bool
||   :   (bool, bool) => bool
bool   :   () => type
bool   :   (bool) => type
int   :   () => type
int   :   (int) => type

Note that many symbols are overloaded in ATS. For instance, ~ is for negation on integers as well as on booleans; bool and int are both sorts and static constants. In ATS, a type refers to a static term s of sort type. For instance, bool and bool(true) are types, and int and int(2+3) are types, too.

Subset Sorts

A subset sort is essentially a sort constrained by a predicate. For instance, we can define a subset sort nat as follows: 
sortdef nat = {a:int | a >= 0}
It is important to note that a subset sort is not regarded as a (regular) sort. The sole purpose of introducing subset sorts is to provide a form of syntactic sugar (to be used together with quantifiers), which is to be explained shortly. Following are some commonly used subset sorts: 
sortdef two = {a:nat | a < 2}
sortdef sgn = {a:int | -1 <= a && a <= 1}
sortdef sgn = {a:int | a == -1 || a == 0 || a == 1} // another definition
sortdef pos = {a:int | a > 0}
sortdef neg = {a:int | a < 0}
where && and || stand for conjunction and disjunction, respectively. Note that we may also use semicolon ; for conjunction. For instance, the subset sort sgn can be defined as follows: 
sortdef sgn = {a:int | -1 <= a; a <= 1}

Some Primitive Types and Values

We use the name dynamic term for a term in the dynamics of ATS and a value is a dynamic term in a special form (which is to be made clear later). We have primitive types bool, char, int and string for booleans, characters, integers and strings, respectively. Also, we have types float and double for floating point numbers with single and double precision, respectively.

The syntax for literal characters, literal integers, literal floats and literal strings is the same as that specified in the ANSI C.

The use of dependent types in ATS is ubiquitous. Given a boolean b, we can form a type bool(b) and the only value that can be assigned this type is the boolean value b. In other words, bool(b) is a singleton type. Similarly, we can form a type int(i) for each integer i and the only value that can be assigned this type is the integer value i. The dependent types Bool and Int, which are for boolean values and integer values, respectively, can be defined as follows in ATS: 

typedef Bool = [a:bool] bool(a)
typedef Int = [a:int] int(a)
where we use [...] for existential quantification. Given an integer i, we can form a type string(i) for strings of length i. The type String for strings is defined as follows: 
typedef String = [a:nat] string (a)

Guarded and Asserting Types

Given a proposition B, that is, a static term of sort bool and a type T, we use the name guarded type for a type of the form B =) T and the name asserting type for a type of the form B /\ T. Intuitively, in order for a value of type B =) T to be used, which is most likely a function, the guard B needs to be discharged first. On the other hand, if an expression of type B /\ T evaluates to a value v, then we know that the assertion B holds (at the point where v is obtained) and v is of type T.

Elements of Programming

We use $exp and $typ as meta-variables ranging over expressions (dynamic terms) and types in ATS.

  • Naming and the Environment

    A critical aspect in programming is to be able to bind names to (complex) computational objects. For instance, we can bind names to values through the following syntax: 

    val radius = 1.0
val pi = 3.1415926
val area = pi * radius * radius
    We can also bind a name to a function value: 
    val square = lam (x: double): double => x * x
val area = pi * square (radius)
  • Tuples

    Given expressions $exp_1,..., $exp_n, we can form a tuple: 

    '($exp_1,...,$exp_n)
    of length n such that the ith component of the tuple is $exp_i for 1 <= i <= n. The use of the quote symbol ' is to indicate that the tuple is boxed. For instance, a pair zero_and_one is formed through the following syntax: 
    val zero_and_one: '(int, int) = '(0, 1)
    We can extract the components of a tuple by pattern matching. For instance, the following syntax binds x and y to 0 and 1: 
    val '(x, y) = zero_and_one
    If values $exp_1,...,$exp_n are assigned types $typ_1,...,$typ_n, respectively, then the tuple 
    '($exp_1,...,$exp_n)
    can be assigned the type 
    '($typ_1,...,$typ_n)
    There is another kind of tuple in ATS, which is referred to as a flat or an unboxed tuple. A tuple of this kind is like a struct in C. For instance, a flat tuple two_and_three is constructed as follows: 
    val two_and_three: @(int, int) = @(2, 3)
    and its components can be selected through pattern matching as follows: 
    val @(x, y) = two_and_three
    If values $exp_1,...,$exp_n are assigned types $typ_1,...,$typ_n, respectively, then the tuple 
    @($exp_1,...,$exp_n)
    can be assigned the type 
    @($typ_1,...,$typ_n).
    Note that the use of the symbol @ is optional.

  • Records

    A label $lab is an alphanumeric identifier or an integer. Given n labels $lab_1, ..., $lab_n and n expressions $exp_1, ..., $exp_n, we can form a boxed record: 

    '{ $lab_1=$exp_1,...,$lab_n=$exp_n }
    If the types of $exp_1, ..., $exp_n are $typ_1, ..., $typ_n, then this record can be assgined the following type: 
    '{ $lab_1=$typ_1,...,$lab_n=$typ_n }
    The use of the quote symbol ' is to indicate that the record is boxed.

    The symbol ' needs to be changed to @ (or simply dropped) in order to form flat or unboxed records.

  • Conditionals

    The syntax for forming a conditional is either 

    if $exp_1 then $exp_2 else $exp3
    or 
    if $exp_1 then $exp_2
    In either case, $exp_1 needs to be a boolean. In the former case, the conditional is of type $typ if both $exp_2 and $exp_3 are of type $typ. In the latter case, the conditional is of type void if $exp_2 is of type void.

  • Type Annotations

    The syntax for supplying a type annotation is 

    $exp : $typ
    For instance, we may write (1+1: Int) to indicate that the expression 1+1 can be assigned the type Int. The need for type annotations is indispensable when advanced programming features in ATS are involved.

  • Function Values

    We use $var a meta-variable ranging over (dynamic) variables in ATS. A function argument $funarg may be of the form $var (unannotated) or $var: $typ (annotated), and a function argument sequence $funargseq is of the form: 

    $funarg_1,...,$funarg_n
    where n may equal 0.

    A non-recursive function can be constructed based on the following syntactic form: 

    lam ($funargseq_1) ... ($funargseq_n) {: $typ} => $exp
    where we use {...} to indicate optional syntax. For instance, the following function adds two floating numbers of double precision: 
    lam (x: double, y: double): double => x + y
    The type of this function is (double, double) -> double, that is, it takes two doubles and returns a double. The curried version of this function is written as follows: 
    lam (x: double) (y: double): double => x + y
    The type of this function is double -> (double -> double), that is, it takes a double and returns a function that takes a double and returns a double.

    A recursive function can be constructed based on the following syntactic form: 

    fix $var ($funargseq_n) ... ($funargseq_n) {: $typ} => $exp
    As an example, the following function, which is of the type Nat -> Nat, computes the Fibonacci numbers: 
    fix fib (x: Nat): Nat => if x >= 2 then fib (x-1) + fib (x-2) else x
  • Function Declarations

    The following form of syntax declares a function named "foo": 

    fun foo ($funargseq_1) ... ($funargseq_n) {: $typ} = $exp
    In the case where the defined function is not recursive, the keyword fun may be replaced with the keyword fn. For instance, we can declare a function as follows to compute Fibonacci numbers: 
    fun fib (x: Nat): Nat = if x >= 2 then fib (x-1) + fib (x-2) else x
    Alternatively, we may write equivalent code as follows: 
    val fib = fix fib (x: Nat): Nat => if x >= 2 then fib (x-1) + fib (x-2) else x
    or as follows: 
    val rec fib: Nat -> Nat = lam x => if x >= 2 then fib (x-1) + fib (x-2) else x
    If we need to declare two functions "foo" and "bar" mutually recursively, we can use the following form of syntax: 
    fun foo ($funargseq_1_1) ... ($funargseq_1_n1) {: $typ_1} = $exp_1
and bar ($funargseq_2_1) ... ($funargseq_2_n2) {: $typ_2} = $exp_2
    This form can be further generalized to declare n mutual recursive functions for n >= 2 . As an example, the follow code implements two mutually recursive functions: 
    fun is_even (x: int): bool = if x > 0 then is_odd  (x-1) else true
and is_odd  (x: int): bool = if x > 0 then is_even (x-1) else false
  • Local Bindings

    A common way to introduce local bindings is through the use of the keyword let. As an example, the following code defines a function that computes the roots of a quadratic equation in terms of the efficients of the equation: 

    // computing roots for [Axx + Bx + C]
fn foo (A: double, B: double, C: double): @(double, double) = let
  val Delta = B * B - 4.0 * A * C
  val () = if Delta < 0.0 then (prerr "no real roots!\n"; exit {void} 1)
  val Delta_sqrt = sqrt (Delta)
  val root1 = (~B + Delta_sqrt) / (2.0 * A)
  val root2 = (~B - Delta_sqrt) / (2.0 * A)
in
  @(root1, root2) // this a flat tuple
end // end of [foo]
    Note that the variables Delta, Delta_sqrt, root1 and root2 are introduced for use only inside the let-expression. Another form of local binding is introduced through the keyword where as is shown below: 
    val fact10 = fact 10 where {
  fun fact (x: int): int = if x > 0 then x * fact (x-1) else 1
} // end of [fact10]
    This code is just an equivalent form of the following code: 
    val fact10 = let
  fun fact (x: int): int = if x > 0 then x * fact (x-1) else 1
in
  fact 10
end // end of [fact10]
  • Sequencing

    Given expressions $exp_1, ..., $exp_n, $exp_{n+1}, where n is some natural number, we can sequence them to form the expression ($exp_1; ...; $exp_n; $exp_{n+1}); this expression is essentially equivalent to the following one in terms of both static and dynamic semantics: 

    let val () = $exp_1 ... val () = $exp_n in $exp_{n+1} end
    So it is clear that the expressions $exp_1, ..., $exp_n are required to be of the void type; the type of the sequence expression is the type of its last component $exp_{n+1}. If $exp_{n+1} is omitted, the default is the expression (), which represents the void value, that is, the only value of the void type.

    • Comments

    There are currently three forms of comments in ATS/Anairiats. As in C, it is also possible to comment out a piece of code in ATS as follows: 
    #if 0 #then // [#then] is optional

(all the code here is commented out)

#endif
    The only requirement is that the code that is commented out must represent a list of syntactically correct declarations in ATS.

    The code used for illustration is available here.