The ATS Programming Language

Unleashing the Potential of Types!


Before you proceed ...

You may want to visit http://www.ats-lang.org instead as this page is primarily for use by the ATS development team.


  • What is ATS?
  • Download and Installation: the current unstable version is ats-lang-anairiats-0.2.8-unstable
  • Bootstrapping
  • Some Simple ATS Programs

  • 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. The current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can be as efficient as C/C++ (see The Computer Language Benchmarks Game for concrete evidence) and 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)

    • 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

    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, no. CNS-0202067, and no.CCR-0702665. 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

    The mailing-list for ATS users is available here.

  • Download and Installation

    ATS is Open Source and Free Software, and it is freely available under the GNU GENERAL PUBLIC LICENSE version 3 (GPL 3.0) as is published by the Free Software Foundation.

    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:

  • Operating System requirement: ATS is supported under the following operating systems:
    • Linux
    • Windows with Cygwin
    • MacOS X (currently no GC support for pthreads)
    • SunOS (currently no GC support for pthreads)
    We plan to port it to other platforms in the future. If you have succeeded in porting ATS to a platform not listed here, please drop us a note.
  • Programming Language requirement: GNU C Compiler (GCC).
  • 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:

    After downloading the compressed tarball containing a release of ATS from the following site:

    http://sourceforge.net/projects/ats-lang/download

    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 
    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" (not "FOO/ATS/"). For instance, if you use CSH (or TCSH), this can be done by executing the following command line:
    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/".

  • Bootstrapping

    In order to bootstrap ATS/Anairiats, one needs to first check out the following svn directory and name it as a local directory, say, "FOO":
    svn co https://ats-lang.svn.sourceforge.net/svnroot/ats-lang/trunk FOO
    
    Then one needs to check out another svn directory directory and name it as the local directory "FOO/bootstrap0":
    svn co https://ats-lang.svn.sourceforge.net/svnroot/ats-lang/bootstrap/anairiats-x.x.x \
      FOO/bootstrap0
    
    Currently, anairiats-0.1.3 is available for bootstrapping. After this is done, please go into the directory "FOO" and execute the command 'autoconf' and then do 'make all'.

    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
    
    Currently, geizella-0.1.3 is available for bootstrapping. After this is done, please go into the directory "FOO" and execute the command 'autoconf' and then do 'make all'.

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

  • Tutorial on ATS/Anairiats

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


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