
The ATS Programming LanguageUnleashing the Potential of Types!
Installation through source code compilationStep 1:After downloading a compressed tarball containing a release of ATS from the following site:
please untar it in a directory, say "FOO", of your choice. This, for instance, can be done by executing the following command line: tar zvxf ATS.tar.gzAll the files and directories extracted from the tarball are now in the directory "FOO/ATS". Step 2:Please execute the following command./configure prefix=DESTDIRwhere DESTDIR is the name of the directory where ATS is to be installed. If the argument [prefix=DESTDIR] is missing, then the default directory for installing ATS is "/usr/local". You can now go into the directory "FOO/ATS" and execute make allThis generates executables "atscc" and "atsopt" in the directory "FOO/ATS/bin", which are the commands you need for compiling ATS programs, and a library file "libats.a" in the directory "FOO/ATS/CCOMP/lib", which you need for linking. Step 3:Please set the environment variable ATSHOME to "FOO/ATS" and then set the environment variable ATSHOMERELOC to "ATSx.x.x", where x.x.x is the version number of the compiled ATS package.Step 4:Optionally, you may install ATS by executing the following command line:make installand then set ATSHOME to $DESTDIR/share/atsanairiatsx.x.x, which is the name of the directory where ATS is installed. The environment variable ATSHOMERELOC is still set to "ATSx.x.x".
Installation through bootstrappingThis installation method is probably the best if you would like to keep abreast of the development of ATS. Please find more details here.Some Simple ATS ProgramsLet us now construct and compile some simple ATS programs.Hello, world!In a file named HelloWorld.dats, we write the following lines of code// compilation command: // atscc o HelloWorld HelloWorld.dats implement main () = begin print ("Hello, world!"); print_newline () endBy executing the following command line, we produce an excutable file named "HelloWorld": atscc o HelloWorld HelloWorld.datsWhat happens here is that atscc first compiles HelloWorld.dats into HelloWorld_dats.c, which is then compiled by gcc to produce "HelloWorld". By running "HelloWorld", we can see the following line on the standard output: Hello, world! Computing Fibonacci NumbersWe now present a simple example to illustrate the idea of programming with theoremproving.We can specify a function fib as follows for computing Fibonacci numbers: fib(0) = 0 fib(1) = 1 fib(n+2) = fib(n) + fib(n+1) for n >= 0A direct implementation of this specification in ATS can be done as follows: fun fib (n: int): int = if n = 0 then 0 else if n = 1 then 1 else fib (n2) + fib(n1) // end of [fib]Clearly, this is a terribly inefficient implementation of exponential timecomplexity. An implementation of fib in C is given as follows that is of linear timecomplexity: 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]There is obviously a logic gap between the defintion of fib and its implementation fibc in C. In ATS, we can give an implementation of fib that completely bridges this gap. First, we need a way to encode the definition of fib 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. 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. We now implement a function in ATS as follows for computing Fibonacci numbers: fun fibats {n:nat} (n: int n) : [r:int] (FIB (n, r)  int r) = let fun loop {n,i:nat  i <= n} {r0,r1:int} .<ni>. ( pf0: FIB (i, r0), pf1: FIB (i+1, r1)  r0: int (r0), r1: int (r1), ni: int(ni) ) : [r:int] (FIB (n, r)  int (r)) = if ni > 0 then loop {n,i+1} (pf1, FIB2 (pf0, pf1)  r1, r0+r1, ni1) else (pf0  r0) in loop (FIB0(), FIB1()  0, 1, n) 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 is 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. Note that the loop function directly corresponds to the whileloop in the body of fibc. Lastly, we emphasize that proofs are completely erased after typechecking. In particular, there is no proof construction at runtime. List QuicksortThis one is for program verification enthusiasts: An implementation of list quicksort is given here that guarantees solely based on its type that the implmentation is terminating and the output list it returns is always a sorted permutation of its input list. This is considered a milestone example in the development of ATS.A GTK/cairo ClockA clock implementation based on GTK+ and cairo is available here, which demonstrates some simple and effective use of linear types in ATS for tracking resources statically, that is, at compiletime.More ExamplesPlease find more, more advanced and larger, examples here.
Resources for Programming in ATSPlease follow the link to find the User's Guide on ATS/Anairiats, an Emacs mode for ATS, a variety of contributed code, and more.
This page is maintained by Hongwei Xi. As always, your comments are welcome. 