| |
The ATS Programming Language
Unleashing the Potential of Types!
Installation through source code compilation
Installation through bootstrapping This installation method is
probably the best if you would like to keep abreast of the development of ATS.
Please find more details here.
Let 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 ()
end
By executing the following command line, we produce an excutable file named
"HelloWorld":
atscc -o HelloWorld HelloWorld.dats
What 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 Numbers
We now present a simple example to illustrate the idea of programming with
theorem-proving.
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 >= 0
A 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 (n-2) + fib(n-1)
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]
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))
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} .<n-i>. (
pf0: FIB (i, r0), pf1: FIB (i+1, r1) | r0: int (r0), r1: int (r1), ni: int(n-i)
) : [r:int] (FIB (n, r) | int (r)) =
if ni > 0 then
loop {n,i+1} (pf1, FIB2 (pf0, pf1) | r1, r0+r1, ni-1)
else (pf0 | r0)
in
loop (FIB0(), FIB1() | 0, 1, n)
end
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 while-loop in the body of fibc.
Lastly, we emphasize that proofs are completely erased after
typechecking. In particular, there is no proof construction at run-time.
List Quicksort This 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 Clock A 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 compile-time.
More Examples Please find more, more advanced and larger, examples
here.
Please 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.
|