Following is a tiny 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. We
can generate an executable named hello by executing the following
command-line:

patscc -o hello hello.dats

If executed, hello does what is mentioned above. The command
patscc first compiles the ATS program contained in hello.dats
into some C code and then invokes a C compiler (gcc in this case) to
translate the generated C code into some binary object code.

Given an input channel and an output channel, the following function fcopy
writes to the latter the characters read from the former:

fun
fcopy (
inp:FILEref, out:FILEref):void=letval c = fileref_getc (inp)inif c >= 0thenletval()= 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 implemented above is such
a tail-recursive function.

Further reading about copying files in ATS can be found
on-line.

ATS advocates a programming paradigm in which programs and proofs can be
constructed in a syntactically intertwined manner. This paradigm is often
referred to as programming with theorem-proving (PwTP), and it
plays a central indispensible role in the development of ATS.
Let us now see a simple and concrete example that clearly illustrates PwTP
as is supported in ATS.

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 >= 2then 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):int=if n >0then loop(n-1, f1, f0+f1)else f0// end of [loop]//in
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:

datapropFIB (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] // end of [dataprop]

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:

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)|intr)=let//fun
loop
{i:nat | i <= n}{r0,r1:int}(pf0:FIB(i,r0),pf1:FIB(i+1,r1)| n_i:int(n-i), r0:intr0, r1:intr1):[r:int](FIB(n,r)|int(r))=(if(n_i >0)then
loop{i+1}(pf1,FIB2(pf0, pf1)| n_i-1, r1, r0+r1
)(* then *)else(pf0| r0)// end of [if])(* end of [loop] *)in
loop{0}(FIB0(*void*),FIB1(*void*)| n,0,1)end// end of [fibats]

Note that fibats is given the following declaration:

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

where the concrete syntax [...] is 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 they
pass typechecking. In particular, there is no proof construction at run-time.

Please click
here if you
are interested in compiling and running this example on-line.

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

Try examples on-line

In ATS, a single-file program refers to one fully contained in a
single file that does not make use of any other files except those
provided by ATS in its standard compilation environment.
Patsoptaas
(patsopt-as-a-service) is a free on-line service provided for compiling
single-file programs in ATS. In the case where Patsoptaas can successfully
compile a single-file program into JS code, then the JS code may be
evaluated inside the browser. Some interesting single-file programs in ATS
are listed as follows that can be serviced by Patsoptaas: