Home
Tutorial
Examples
Implementation
Documentation
Libraries
Papers
FAQ
Changes
Mailing List

ATS -- unleashing the power of types!

  • What is ATS?

    ATS is a programming language with a highly expressive type system rooted in the framework Applied Type System. In particular, both dependent types and linear types are available in ATS. ATS/Geizella, the current implementation of ATS, is as efficient as C/C++ (see SHOOTOUT for concrete evidence) if not more so, and it supports a variety of programming paradigms that include:

    • 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).

    • Object-oriented programming

    • 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 still 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.

      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, we can advocate a programming style that combines programming with theorem proving. Furthermore, we may use this component as a logical framework to encode various deduction systems and their (meta-)properties.

  • Acknowledgments

    The development of ATS has been funded in part by National Science Foundation under the grants no. CCR-0081316/CCR-0224244, no. CCR-0092703/0229480 and no. CNS-0202067. As always, any opinions, findings, and conclusions or recommendations expressed here are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.

  • Mailing List

    Here is the current official mailing-list for ATS programmers.

  • Installation

    The current implementation of ATS is given the name ATS/Geizella or simply Geizella. It is written in Objective Caml. In order to install Geizella, the following requirements need to be met:
    • OS requirement: Linux. We have so far only tested Geizella under Linux, and we plan to port it to other platforms in the future.
    • PL requirements: ocaml (version 3.08 or later) and gcc.
    Also the library [libgmp.a] is required, which is in general included in a Linux distribution.

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

    Step 1:

    After downloading the tarball ATS.tar.gz, please untar it in a directory, say "FOO/", of your choice. This, for instance, can be done by executing the following command: 
    tar -zvxf ATS.tar.gz
    All the files and directories extracted from the tarball are now in the directory "FOO/ATS/".

    Step 2:

    Please set the shell environmental variable ATSHOME to be "FOO/ATS/". For instance, if you use CSH (or TCSH), this can be done by executing the following command: 
    setenv ATSHOME FOO/ATS/
    You also need to put the directory "FOO/ATS/bin/" in your execution path. This can be done in CSH (or TCSH) as follows: 
    setenv PATH ${PATH}:${ATSHOME}/bin
    You may want to put these commands in a file (e.g., .cshrc) that is executed each time a shell is started.

    Step 3:

    You can now go into the directory "FOO/ATS/" and execute 
    make all
    This generates an executable "atscc" in the directory "FOO/ATS/bin/", which is the command you need for compiling ATS programs. Also, this generates a library file "libats.a" in the directory "FOO/ATS/CCOMP/lib/".

  • Some Simple ATS Programs

    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 (argc, argv) = begin
  print ("Hello, world!"); print_newline ()
end
    By executing the following command, 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 on the standard output: 
    << Hello, world!
    Note that we use >> and << as prompts to indicate input and output, respectively.

    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.

    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.

    More Examples

    Please find more, more advanced and larger, examples here.

  • Tutorial on ATS/Geizella

    A tutorial on ATS/Geizella is available here. It is expanding monthly if not weekly.

    • This page is maintained by Hongwei Xi. As always, your comments are welcome.