ATS -- unleashing the potential of types!

What is ATS?

• Functional programming. While ATS is primarily a language based on eager call-by-value evaluation, it also supports lazy call-by-need evaluation. The availability of linear types in ATS can often make functional programs in ATS not only run with surprisingly high efficiency (when compared to C) but also run with surprisingly small (memory) footprint (when compared to C as well)

• Imperative programming. The novel and unique approach to imperative programming in ATS is firmly rooted in the paradigm of programming with theorem proving. While features considered dangerous in other languages (e.g, explicit pointer arithmetic and explicit memory allocation/deallocation) are allowed in ATS, the type system of ATS is able to guarantee that no run-time errors can occur that may lead to memory corruption.

• Concurrent programming. ATS, equipped with a multicore-safe implementation of garbage collection, can support multithreaded programming through the use of pthreads. There is also high-level support in ATS for parallel let-binding, which provides a simple and effective means to constructing programs that can take advantage of multicore architectures.

• Modular programming. The module system of ATS is largely infuenced by that of Modula-3, which is both simple and general as well as effective in supporting large scale programming.

In addition, ATS contains a component ATS/LF that supports a form of (interactive) theorem proving, where proofs are written as total functions. With this component, ATS advocates a programming style that combines programming with theorem proving. Furthermore, this component may be used as a logical framework to encode various deduction systems and their (meta-)properties.

Acknowledgments

Mailing List

Download and Installation

The current implementation of ATS is given the name ATS/Anairiats or simply Anairiats. It is written in ATS itself. In order to install Anairiats, the following requirements need to be met:

The GMP library (libgmp.a), which is often included in a GNU/Linux distribution, is currently optional and it may be required for installing a release of ATS in the future. Please see http://gmplib.org for more details on GMP.

Once these requirements are met, you can readily install Anairiats in 3 steps as described below:

Step 1:

please untar it in a directory, say "FOO", of your choice. This, for instance, can be done by executing the following command line:

tar -zvxf ATS.tgz 

Step 2:

setenv ATSHOME FOO/ATS

setenv PATH ${PATH}:${ATSHOME}/bin

Step 3:

make all

Bootstrapping

svn co https://ats-lang.svn.sourceforge.net/svnroot/ats-lang/trunk FOO

svn co https://ats-lang.svn.sourceforge.net/svnroot/ats-lang/bootstrap/anairiats-x.x.x \
  FOO/bootstrap0

It is also possible to use the ATS/Geziella compiler (written in Objective Caml) for bootstrapping ATS/Anairiats. This can be done by checking out the following svn directory and name it as the local directory "FOO/bootstrap0":

svn co https://ats-lang.svn.sourceforge.net/svnroot/ats-lang/bootstrap/geizella-x.x.x \
  FOO/bootstrap0

Some Simple ATS Programs

Hello, world!

// compilation command:
//   atscc -o HelloWorld HelloWorld.dats

implement main () = begin
  print ("Hello, world!"); print_newline ()
end

atscc -o HelloWorld HelloWorld.dats

Hello, world!

Factorial (version 1)

// [fun] declares a recursive function
fun fact1 (x: int): int = if x > 0 then x * fact1 (x-1) else 1

// [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

// [a:viewt@ype] means that [a] can be a linear type of any size
fun exit : {a:viewt@ype} int -> a

The entire code for this example is available here.

Factorial (version 2)

int -> type

typedef Int = [n:int] int n // type for integers

typedef Nat = [n:int | n >= 0] int n // type for natural numbers

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

(Nat, Nat) -> Nat

// [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

Factorial (version 3)

List Quicksort

More Examples

Tutorial on ATS/Anairiats