Examples
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.
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)
in
if c >= 0 then let
val () = fileref_putc (out, c) in fcopy (inp, out)
end end
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.
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
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
in
loop (n, 0, 1)
end
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))
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)
in
loop {0} (FIB0 (), FIB1 () | n, 0, 1)
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 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.
Please find
on-line
various programs in ATS plus detailed explanation that are written for the
purpose of advocating effective programming in ATS.
Please find
on-line
a large variety of programs written in ATS.
