ATS

What is ATS?

• Functional programming, both eager and lazy (available)
• Object-oriented programming (available)
• Imperative programming with pointers (available)
• Concurrent programming with pthreads (available)
• Modular programming (available)
• Meta programming (available)
• Assembly programming (planned)

Also, ATS contains a component ATS/LF that supports a form of (interactive) theorem proving. With this component, we can readily 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 properties, and some of such examples can be found here.

Mailing List

Some sample code in ATS:

• (Functional Programming) The following is a short example demonstrating that a zip function can be implemented such that the type assigned to the function mandates that the two arguments of the function be of the same length. We first declare a datatype constructor list as follow:

  datatype list (a:type, n:int) =
    | {a:type} nil (a, 0)
    | {a:type, n:nat} cons (a, n+1) of (a, list (a, n))
  

  The declaration introduces a type constructor list that takes a type and an integer to form a type. In addition, there are two value constructors nil and cons associated with list, which are given the following types:

  nil : {a:type} list (a, 0)
  cons : {a:type, n:nat} (a, list (a, n)) -> list (a, n+1)
  

  Note that we use {...} for universal quantification. The implementation of the zip function is given as follows:

  fun zip {a:type, b:type, n:nat}
     (xs: list (a, n), ys: list (b, n)): list ('(a, b), n) =
    case (xs, ys) of
      | (nil (), nil ()) => nil
      | (cons (x, xs), cons (y, ys) => cons ( '(x, y),  zip (xs, ys) )
  

  We use '(a, b) for a tuple type such that the first and the second components of the tuple type are a and b, respectively. Similarly, we use '(x, y) for a tuple such that the first and the second components of the tuple are x and y, respectively. The quote symbol is solely for the purpose of parsing. The header of the above function definition indicates that the function zip is given the following type:

  zip : {a:type, b:type, n:nat} (list (a, n), list (b, n)) -> list ('(a, b), n)
  

  Therefore, the function zip can only be applied to two lists of the same length n for some natural number n, and it returns a list of length n as well.

• (Functional Programming) We also often encounter existentially quantified types in practice. The following concrete syntax implements a function in ATS that filters out elements of a lists according to a given predicate:

  fun filter {a:type, m:nat}
     (p: a -> Bool, xs: list (a, m)): [n:nat | n <= m] list (a, n) =
    case xs of
      | nil () => nil
      | cons (x, xs) =>
        if p (x) then cons (x, filter (p, xs)) else filter (p, xs)
  

  The header of the above function definition means that the defined function filter is assigned the following type:

  filter : {a:type, m:nat} (a -> Bool, list (a, m)) -> [n:nat | n <= m] list (a, n)
  

  Note that we use [n:nat | n <= m] list (a, n) as the type for lists with length less than or equal to m.

• (Functional Programming) With dependent types, we can often capture interesting invariants in various data structures. For instance, a red-black tree is a binary tree that satisfies the following invariants:
  • Each node in the tree is either red or black;
  • Each path from the root to a leaf contains the same number of black nodes, which is often called black height;
  • Each red node can only be followed by two black nodes.
  We can declare a datatype in ATS as follows that is precisely for red-black trees:

  (* element type, color, black height, violation, size *)
  datatype rbt (type, int, int, int, int) =
    | {a:type} E(a, 0, 0, 0, 0)
    | {a:type, cl:color, cr:color, bh:nat, sl:nat, sr:nat}
      B(a, 0, bh+1, 0, sl+sr+1) of
        (rbt (a, cl, bh, 0, sl), a, rbt (a, cr, bh, 0, sr))
    | {a:type, cl:color, cr:color, bh:nat, sl:nat, sr:nat}
      R(a, 1, bh, cl+cr, sl+sr+1) of
        (rbt (a, cl, bh, 0, sl), a, rbt (a, cr, bh, 0, sr))
  

  We use 0 and 1 for the black and red colors, respectively, and the empty tree E is considered black. We use rbt(elt, c, bh, v, s) as the type for a binary tree such that its elements are of type elt its root node is of color c, its black height is bh, its violation number is n, and its size is s. Note that one violation is counted if a red node is followed by another red node. Therefore, the type for a red-black tree can be defined as follows:

  typedef rbtree (elt: type) = [c:color,bh:nat,s:nat] rbt (elt, c, bh, 0, s)
  

  Some code for manipulating red-black trees can be found here.

• (Functional Programming) The following example shows how a type-preserving evaluator for a simply typed langauge can be implemented in ATS:

  // stp: sort for indexes representing simple types
  datasort stp = STPbool | STPint | STParr of (stp, stp) | STPtup of (stp, stp)
  
  // ctx: sort for contexts
  datasort ctx = CTXnone | CTXsome of (stp, ctx)
  
  // exp (ctx, stp): type for values that represent derivations of simply typed expressions
  
  datatype exp (ctx, stp) =
    | {ts: ctx} EXPbool (ts, STPbool) of Bool
    | {ts: ctx} EXPint (ts, STPint) of Int
    | {ts: ctx, t: stp} EXPone (CTXsome (t, ts), t)
    | {ts: ctx, t1: stp, t2: stp} EXPlam (ts, STParr (t1, t2)) of exp (CTXsome (t1, ts), t2)
    | {ts: ctx, t1: stp, t2: stp} EXPapp (ts, t2) of (exp (ts, STParr(t1, t2)), exp (ts, t1))
    | {ts: ctx, t1: stp, t2: stp} EXPtup (ts, STPtup (t1, t2)) of (exp (ts, t1), exp (ts, t2))
    | {ts: ctx, t1: stp, t2: stp} EXPfst (ts, t1) of exp (ts, STPtup (t1, t2))
    | {ts: ctx, t1: stp, t2: stp} EXPsnd (ts, t2) of exp (ts, STPtup (t1, t2))
  
  datatype env (ctx) =
    | ENVnone (CTXnone)
    | {ts: ctx, t: stp} ENVsome (CTXsome (t, ts)) of (value t, env ts)
  
  and value (stp) =
    | VALbool (STPbool) of Bool
    | VALint (STPint) of Int
    | {ts: ctx, t1: stp, t2: stp} VALclo (STParr (t1, t2)) of (env ts, exp (CTXsome (t1, ts), t2))
    | {t1: stp, t2: stp} VALtup (STPtup (t1, t2)) of (value (t1), value (t2))
  
  fun eval {ts: ctx, t: stp} (env: env ts, exp: exp (ts, t)): value t =
    case exp of
      | EXPbool b => VALbool b
      | EXPint i => VALint i
      | EXPlam exp => VALclo (env, exp)
      | EXPapp (exp1, exp2) => evalApp (eval (env, exp1), eval (env, exp2))
      | EXPtup (exp1, exp2) => VALtup (eval (env, exp1), eval (env, exp2))
      | EXPfst (exp) => let val VALtup (v1, _) = eval (env, exp) in v1 end
      | EXPsnd (exp) => let val VALtup (_, v2) = eval (env, exp) in v2 end
  
  and evalApp {t1: stp, t2: stp} (v1: value (STParr (t1, t2)), v2: value t1): value t2 =
    let
       val VALclo (env, exp) = v1
    in
       eval (ENVsome (v2, env), exp)
    end
  
  // a type-preserving evaluator for *closed* simply typed expressions
  
  fun evaluate {t: stp} (exp: exp (CTXnone, t)): value t = eval (ENVnone, exp)
  

• (Functional Programming) The notion of guarded recursive datatypes is supported in ATS. The following is an example that makes use of guarded recursive datatypes, and we encourage the reader to compare this example with the previous one.

  datasort ctx = nil | :: of (type, ctx)
  
  datatype FOAS (ctx, type) = // first-order abstract syntax
    | {G:ctx, a:type} FOASlift (G, a) of a
    | {G:ctx, a:type} FOASone (a :: G, a)
    | {G:ctx, a:type, b: type}
      FOASshi (a :: G, b) of FOAS (G, b)
    | {G:ctx, a:type, b:type}
      FOASlam (G, a -> b) of FOAS (a :: G, b)
    | {G:ctx, a:type, b:type}
      FOASapp (G, b) of (FOAS (G, a -> b), FOAS (G, a))
    | {G:ctx, a:type, b:type} FOASfix (G, a) of FOAS (a :: G, a)
  
  datatype ENV (ctx) =
    | ENVnone (nil)
    | {G:ctx, a:type} ENVsome (a :: G) of (a, ENV (G))
  
  fun compile {G:ctx, a:type} (e: FOAS (G, a)): ENV (G) -> a =
      case e of
        | FOASlift v => lam env => v
        | FOASone () => lam (ENVsome (v, _)) => v
        | FOASshi e =>
          let
              val c = compile e
          in
              lam (ENVsome (_, env)) => c (env)
          end
        | FOASlam (e) =>
          let
              val c = compile e
          in
              lam env => lam v => c (ENVsome (env, v))
          end
        | FOASapp (e1, e2) =>
          let
              val c1 = compile e1 and c2 = compile e2
          in
              lam env => c1 env (c2 env)
          end
  
  fun run e = compile e ENVnone
  withtype {a:type} FOAS (nil, a) -> a
  

  An approach to meta-programing through typeful code representation is availabe here, where an interesting application of the above typeful code representation can be found.

• (Imperative Programming) The notion of stateful view is employed in ATS to guarantee safe use of pointers. Generally speaking, a view is like a type, but it is linear. We use views to capture or describe memory layouts. Given a type T and an address L, we write T@L for a (primitive) view that indicates a value of type T is stored at address L. The following concrete syntax implements a function in ATS that swaps the values stored at two given addresses:

  fun swap {a1:type, a2:type, l1:addr, l2:addr}
     (pf1: a1 @ l1, pf2: a2 @ l2 | p1: ptr l1, p2: ptr l2): '(a2 @ l1, a1 @ l2 | unit) =
    let
       val '(pf1' | v1) = getVar (pf1 | p1) // pf1' : a1 @ l1
       val '(pf2' | v2) = getVar (pf2 | p2) // pf2' : a2 @ l2
       val '(pf1'' | _) = setVar (pf1' | p1, v2) // pf1'' : a2 @ l1
       val '(pf2'' | _) = setVar (pf2' | p2, v1) // pf2'' : a1 @ l2
    in
       '(pf1'', pf2'' | '())
    end
  

  Given an address L, we use ptr(L) as the singleton type for the pointer that points to L. The header of the above function definion indicates that swap is assigned the following type:

  swap : {a1:type, a2:type, l1:addr, l2:addr}
           (a1 @ l1, a2 @ l2 | ptr l1, ptr l2) -> '(a2 @ l1, a1 @ l2 | unit)
  

  The functions getVar and setVar are the built-in functions assgined the following types:

  getVar : {a:type, l:addr} (a @ l | ptr l) -> '(a @ l | a)
  setVar : {a1:type, a2:type, l:addr} (a1 @ l | ptr l, a2) -> '(a1 @ l | unit)
  

  Essentially, getVar reads through a given pointer while setVar writes through a given pointer.

• (Imperative Programming) In order to model more sofphisticated memory layouts, we need to form recursive stateful views. For instance, we may use the concrete syntax as follows to declare a recursive view constructor arrayView:

  dataview arrayView (type, int, addr)
    | {a:type, l:addr} ArrayNone (a, 0, l)
    | {a:type, n:nat, l:addr} ArraySome (a, n+1, l) of (a, arrayView (a, n, l+1))
  

  Given a type T, an integer I and an address L, arrayView(T,I,L) is a view stating that there are I values of type T stored at addresses L, L+1, ..., L+I-1. There are two proof constructors ArrayNone and ArraySome associated with arrayView; ArrayNone is a proof of arrayView(T,0,L) for any type T and address L; ArraySome (pf1, pf2) is a proof of arrayView(T,I+1,L) for any type T, integer I and address L if pf1 and pf2 are proofs of views T@L and arrayView(T,I,L+1), respectively. For instance, the following is an implementation of a function in ATS that takes the first element out of a given nonempty array:

  fun arrayGetFirst {a:type, n:int, l:addr | n > 0}
     (pf: arrayView (a, n, l) | p: ptr l): '(arrayView (a, n, l) | a) =
    let
       prval ArraySome (pf1, pf2) = pf
       val '(pf1 | x) = getVar (pf1 | p)
    in
       '(ArraySome (pf1, pf2) | x)
    end
  

• (Object-Oriented Programming) In the following example, we first declare a class for equality and then implement various objects of this class. Some detailed explanation on OOP in ATS is available in a tutorial (pdf) (ps) on ATS.

  class isEqual (elt: type) = { // declaring a class tag constructor
  
    super: (* none *)
  
    method == (elt, elt): Bool
    method <> (elt, elt): Bool
  
    method eq: (elt, elt) -> Bool
    method neq: (elt, elt) -> Bool
  }
  
  fun isEqual {elt: type}: sup (isEqual elt) = super { // implementing a super function
    super: (* none *)
  
    method == (x, y) = # eq (x, y)
    method eq = lam (x, y) => not (# neq (x, y))
  
    method <> (x, y) = # neq (x, y)
    method neq = lam (x, y) => not (# eq (x, y))
  }
  
  val BoolIsEqual: obj (isEqual Bool) = object {
    super: isEqual {Bool}
  
    method eq = lam (x, y) => if x then y else not y
  
  }
  
  val IntIsEqual: obj (isEqual Int) = object {
    super: isEqual {Int}
  
    method eq = lam (x, y) => x ieq y
  
  }
  
  fun ListIsEqual {elt: type} (eltIsEqual: obj (isEqual elt))
    : obj (isEqual (List elt)) = object {
  
    super: isEqual {List elt}
  
    method eq =
      fix aux (xs, ys) =>
        case (xs, ys) of
          | (nil (), nil ()) => true
          | (cons (x, xs), cons (y, ys)) =>
            if eltIsEqual # eq (x, y) then aux (xs, ys) else false
          | (_, _) => false
  }  
  
  

• (Meta Programming) In ATS, the programer can also construct meta-programs, i.e., programs that may generate program when executed. The type theory supporting meta-programming in ATS is explained in the following paper:

  • Meta-Programming through Typeful Code Representation (pdf) (ps)

  We use static terms of the sort types to represent a sequence of types. Given static terms G and T of sorts types and type, respectively, we use G |- T as the type for values representing code of type T in which free variables are assigned types according to G. We present as follows a simple example of meta-programming:

  fun genPower {G: types} (x: G |- Int, n: Nat): G |- Int =
    if n igt 0 then `[,[x] imul ,[genPower (x, ipred n)]] else `[1]
  
  val square = // as if defined as [ lam x => x * (x * 1) ]
    $exec `[lam (x: Int): Int => ,[genPower (`[x], 2)]]
  
  val cube = // as if defined as [ lam x => x * (x * (x * 1)) ]
    $exec `[lam (x: Int): Int => ,[genPower (`[x], 3)]]
  
  

  The function genPower takes a piece of code representing an integer and a natural number n, and then returns a piece of code that computes the nth power of the integer. For instance, we can readily use genPower to generate code for computing the square and the cube of a given integer. As such code is specialized, it may potentially run faster.

Papers on or related to ATS:

• Chiyan Chen and Hongwei Xi, Combining Programming with Theorem Proving, April 2005. (pdf) (ps)

• Chiyan Chen and Hongwei Xi, ATS/LF: a type system for constructing proofs as total functional programs. November 2004. (pdf) (ps)

• Hongwei Xi and Dengping Zhu, Views, Types, and Viewtypes. October 2004. (pdf) (ps)

• Hongwei Xi and Dengping Zhu and Yanka Li, Applied Type System with Stateful Views. September 2004. (pdf) (ps)

• Hongwei Xi, Dependent Types for Practical Programming via Applied Type System, September 2004. (pdf) (ps)

• Dengping Zhu and Hongwei Xi, Safe Programming with Pointers through Stateful Views. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages (PADL '05), LNCS vol. 3350, pp. 83--97, Long Beach, CA, January 2005. (bibtex) (pdf) (ps)

• Chiyan Chen, Rui Shi and Hongwei Xi, A Typeful Approach to Object-Oriented Programming with Multiple Inheritance. In Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages (PADL '04), LNCS vol. 3057, pp. 239--254, Dallas, TX, June 2004. (bibtex) (pdf) (ps) (slides in ppt)

• Hongwei Xi, Applied Type System (extended abstract). In the post-workshop proceedings of TYPES 2003, Springer-Verlag LNCS vol. 3085, pp. 394--408, 2004. (bibtex) (pdf) (ps)

• Chiyan Chen and Hongwei Xi, Meta-Programming through Typeful Code Representation, September 2003. (pdf) (ps)

• Hongwei Xi, Chiyan Chen and Gang Chen, Guarded Recursive Datatype Constructors. In Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '03), pp. 224--235, New Orleans, Louisiana, January 2003. (bibtex) (pdf) (ps) (slides in ppt)

• Hongwei Xi and Frank Pfenning, Dependent Types in Practical Programming. In Proceedings of Symposium on Principles of Programming Languages (POPL '99), San Antonio, January 1999. (bibtex) (ps) (pdf)

• Hongwei Xi and Frank Pfenning, Eliminating Array Bound Checking Through Dependent Types. In Proceedings of Conference on Programming Language Design and Implementation (PLDI '98), pp. 249-257, Montreal, June 1998. (bibtex) (ps) (pdf)

Implementation:

Copyright (c) 2002-2006, Hongwei Xi, Boston University. All rights
reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

 o Redistributions of source code must retain the above copyright notice,
   this list of conditions and the following disclaimer.

 o Redistributions in binary form must reproduce the above copyright
   notice, this list of conditions and the following disclaimer in the
   documentation and/or other materials provided with the distribution.

 o The name of Boston University may not be used to endorse or promote
   products derived from this software without specific prior written
   permission.

 o The user may use this software for any teaching or research purpose, but
   may not sell or use it for any commercial purpose. To do so requires
   additional written permissions or license.
   
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.