The ATS Programming Language
Unleashing the Potentials of Types and Templates!


Hello, world!

Following is a complete program in ATS for printing out the string "Hello, world!" plus a newline:

implement main0 () = print ("Hello, world!\n")

Assume that the program is stored in a file named hello.dats. By executing the following command-line:

atscc -o hello hello.dats

we can generate an executable named hello, which does what is mentioned above if executed. The command atscc first compiles the ATS program contained in hello.dats into some C code and then invokes a C compiler (e.g., gcc) to translate the C code into binary object code.

Copying files

Following is a simple and complete program in ATS for copying from an input channel to an output channel:

fun fcopy
  inp: FILEref, out: FILEref
) : void = let
  val c = fileref_getc (inp)
  if c >= 0 then let
    val () = fileref_putc (out, c) in fcopy (inp, out)
  end // end of [if]
end (* end of [fcopy] *)

Note that loops in imperative languages such as C and Java are often implemented as tail-recursive functions in ATS, which are then compiled back into loops in C. For instance, fcopy as is presented above is such a tail-recursive function.

Also, some detailed explanation about copying files in ATS is available on-line.

Computing Fibonacci numbers

The paradigm of programming with theorem-proving (PwTP) is a cornerstone of ATS, and a simple example to illustrate this programming paradigm is presented here.

A function fib can be specified as follows for computing Fibonacci numbers:

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

Following is a direct implementation of this specified function in ATS:

fun fib (n: int): int =
  if n >= 2 then fib (n-2) + fib (n-1) else n
// end of [fib]

Clearly, this is a terribly inefficient implementation of exponential time-complexity. An implementation of fib in C is given as follows that is of linear time-complexity:

int fibc (int n) {
  int tmp, f0 = 0, f1 = 1 ;
  while (n-- > 0) { tmp = f1 ; f1 = f0 + f1 ; f0 = tmp ; } ; return f0 ;
} // end of [fibc]
If translated into ATS, the function fibc can essentially be implemented as follows:
fun fibc (n: int): int = let
  fun loop (n: int, f0: int, f1: int) =
    if n > 0 then loop (n-1, f1, f0+f1) else f0
  // end of [loop]
  loop (n, 0, 1)
end // end of [fibc]
There is obviously a logic gap between the defintion of fib and its implementation as is embodied in fibc. In ATS, an implementation of fib can be given that completely bridges this gap. First, the specification of fib needs to be encoded into ATS, which is fulfilled by the declaration of the following dataprop:
dataprop FIB (int, int) =
  | FIB0 (0, 0) | FIB1 (1, 1)
  | {n:nat} {r0,r1:int} FIB2 (n+2, r0+r1) of (FIB (n, r0), FIB (n+1, r1))
// end of [FIB]

This declaration introduces a type FIB for proofs, and such a type is referred to as a prop in ATS. Intuitively, if a proof can be assgined the type FIB(n,r) for some integers n and r, then fib(n) equals r. In other words, FIB(n,r) encodes the relation fib(n)=r. There are three constructors FIB0, FIB1 and FIB2 associated with FIB, which are given the following types corresponding to the three equations in the definition of fib:

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

Note that {...} is the concrete syntax in ATS for universal quantification. For instance, FIB2(FIB0(), FIB1()) is a term of the type FIB(2,1), attesting to fib(2)=1.

A fully verified implementaion of the fib function in ATS can now be given as follows:

fun fibats
  {n:nat} (n: int n)
  : [r:int] (FIB (n, r) | int r) = let
  fun loop {i:nat | i <= n} {r0,r1:int} (
    pf0: FIB (i, r0), pf1: FIB (i+1, r1) | ni: int (n-i), r0: int r0, r1: int r1
  ) : [r:int] (FIB (n, r) | int r) =
    if ni > 0 then
      loop {i+1} (pf1, FIB2 (pf0, pf1) | ni - 1, r1, r0 + r1)
    else (pf0 | r0)
  // end of [loop]
  loop {0} (FIB0 (), FIB1 () | n, 0, 1)
end // end of [fibats]

Note that fibats is assigned the following type:

fibats : {n:nat} int(n) -> [r:int] (FIB(n,r) | int(r))

where [...] is the concrete syntax in ATS for existential quantification and the bar symbol (|) is just a separator (like a comma) for separating proofs from values. For each integer I, int(I) is a singleton type for the only integer whose value equals I. When fibats is applied to an integer of value n, it returns a pair consisting of a proof and an integer value r such that the proof, which is of the type FIB(n,r), asserts fib(n)=r. Therefore, fibats is a verified implementation of fib as is encoded by FIB. Note that the inner function loop directly corresponds to the while-loop in the body of the function fibc (written in C).

Lastly, it should be emphasized that proofs are completely erased after typechecking. In particular, there is no proof construction at run-time.

Effective ATS

Please find on-line various programs in ATS plus detailed explanation that are written for the purpose of advocating effective programming in ATS.

Further Examples

Please find on-line a large variety of programs written in ATS.

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. Logo