Try ATS on-line
The ATS Programming Language
Unleashing the Potentials of Types and Templates!

Hello, world!

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

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.

Copying files

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

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 implemented above is such a tail-recursive function.

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

Computing Fibonacci numbers

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:

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:

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:

fibc (
  n: int
) : int = let
loop(n: int, f0: int, f1: int): 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] // 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:

FIB0 : () -> FIB (0, 0)
FIB1 : () -> FIB (1, 1)
FIB2 : {n:nat}{r0,r1:int} (FIB (n, r0), FIB (n+1, 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:

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

Effective Programming in ATS

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:
Proving B├ęzout's identity
Proving Identities for tally-of-powers
Proving the principle of SMI
Proving the pigenhole principle
Proving that primes are unbounded
Solving the 8-queen puzzle
Solving the 8-queen puzzle (anim)
Solving the ferryman puzzle
Drawing a Sierpinski triangle
Drawing an analog clock (1)
Animating list-merge-sort (1)
Animating array-quick-sort (1)
Animating array-quick-sort (2)
Animating array-insertion-sort

This page is created by Hongwei Xi
with tools including ATS/weboxy, atscc2js and atscc2php.