| |
ATS -- 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!
Factorial (version 1) A simple recursive function fact1
is defined as follows to compute factorials.
// [fun] declares a recursive function
fun fact1 (x: int): int = if x > 0 then x * fact1 (x-1) else 1
The following code passes an integer read from the standard input to the
function fact1 and then prints the result returned from
fact1 onto the standard output.
// [fn] declares a non-recursive function; it is fine to replace [fn] with [fun]
// [@(...)] is used in ATS to group arguments for functions of variable arguments
fn fact1_usage (cmd: string): void =
prerrf ("Usage: %s [integer]\n", @(cmd)) // print an error message
implement main (argc, argv) =
if argc >= 2 then let
val n = int1_of argv.[1] // turning a string into an integer
val res = fact1 n
in
printf ("factorial of %i = %i\n", @(n, res))
end else begin
fact1_usage (argv.[0]); exit (1)
end
Note that the function exit is given the following type:
// [a:viewt@ype] means that [a] can be a linear type of any size
fun exit : {a:viewt@ype} int -> a
Also note that the type void should not be confused with the type
unit in languages like SML and OCaml; the former is of size 0 while
the latter is of size 1 (word).
The entire code for this example is available here.
Factorial (version 2)
Let us now see an example involving dependent types. In ATS, int is
a static constant of the following sort:
int -> type
Note that the symbol int is overloaded: it is both a static constant
and a sort. Given an integer
i (of sort int), int(i) is a singleton type
containing only the integer i. So int is often called a
type constructor. We now define a
type constant Int as follows:
typedef Int = [n:int] int n // type for integers
We use the syntax [n:int] to existentially quantify over
some variable n of sort int, that is, n
ranging over integers.
We define the type for natural number as follows:
typedef Nat = [n:int | n >= 0] int n // type for natural numbers
where the syntax [n:int | n >= 0] represents existential
quantification over some variable n of sort int that
satisfies n >= 0.
The factorial function can be implemented as follows:
fun fact2 {n:nat} (x: int n): Nat = if x > 0 then x nmul fact2 (x-1) else 1
The type assigned to fact2 indicates that the function returns a
natural number when applied to a natural number. It causes a type error
if fact2 is applied to a negative integer. The function
nmul (infix) is assumed to be of the following type:
(Nat, Nat) -> Nat
That is, nmul returns a natural number when applied to
two natural numbers.
The following code indicates the necessity to check that an integer read
from the standard input is nonngative when fact2 is called on it.
// [fn] declares a non-recursive function
// [@(...)] is used in ATS to group arguments for functions of variable arguments
fn fact2_usage (cmd: string): void =
prerrf ("Usage: %s [integer]\n", @(cmd)) // print an error message
implement main (argc, argv) =
if argc >= 2 then let
val n = int1_of argv.[1] // turning a string into an integer
val () = assert_errmsg
(n >= 0, "The integer argument needs to be nonnegative.\n")
val res = fact2 n
in
printf ("factorial of %i = %i\n", @(n, res))
end else begin
fact2_usage (argv.[0]); exit (1)
end
The entire code for this example is available here. One may want to see what happens
to typechecking if the call to assert_errmsg in the code is deleted.
Factorial (version 3)
If you are not afraid of being overwhelmed at this moment, please find an
implementation of the factorial function here that bears the signature of ATS:
programming with theorem proving. This is an implementation of
the factorial function whose correctness is formally verified in the type
system of ATS.
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.
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.
|