ATS (programming language)

ATS

Paradigm	multi-paradigm: imperative, functional
Designed by	Hongwei Xi at the Boston University
Influenced by	ML, Objective Caml
Website	http://www.ats-lang.org/

ATS (Applied Type System) is a programming language whose stated purpose is to support theorem proving in combination with practical programming through the use of advanced type systems. The performance of ATS has been demonstrated to be comparable to that of the C and C++ programming languages.

History

ATS is derived mostly from the ML and Objective Caml programming languages. An earlier language, Dependent ML, by the same author has been incorporated by the language.

Theorem proving

The primary focus of ATS is to support theorem proving in combination with practical programming.

Data representation

According to the author (Hongwei Xi), ATS's efficiency is largely due to the way that data is represented in the language and tail-call optimizations (which are generally important for the efficiency of functional programming languages). Data is stored in a flat or unboxed representation rather than a boxed representation.

Features

Basic types

• bool (true, false)
• int ( 255, 0377, 0xFF), unary minus as ~
• double
• char 'a'
• string "abc"

Tuples and records

prefix @ or none means direct, flat or unboxed allocation

val x : @(int, char) = @(15, 'c')                // x.0 = 15 ; x.1 = 'c'
val @(a, b) = x                                  // pattern matching binding, a= 15, b='c'
val x = @{first=15, second='c'}                  // x.first = 15
val @{first=a, second=b} = x                     // a= 15, b='c'
val @{second=b, ...} = x                         // with omission, b='c'

prefix ' means indirect or boxed allocation

val x : '(int, char) = '(15, 'c')                // x.0 = 15 ; x.1 = 'c'
val '(a, b) = x                                  // a= 15, b='c'
val x = '{first=15, second='c'}                  // x.first = 15
val '{first=a, second=b} = x                     // a= 15, b='c'
val '{second=b, ...} = x                         // b='c'

special

With '|' as separator, some functions return wrapped the result value with an evaluation of predicates

val ( predicate_proof | value) = myfunct params

Common

{...} universal quantification
[...] existential quantification
(...) parentsized expression or tuple

(... | ...)   (proof | value)

@(...) flat tuple or variadic function parameters tuple (see example's printf)

Dictionary

sort

domain of a variable

sortdef nat = {a: int | a >= 0 } // from prelude

type (as sort)

sort class for elements with the length of a pointer word, to be used in polymorphic functions

fun {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0)

t@ype

sort class with length unknown or abstracted length. It supersets type

viewtype

a sort class like type with a view (memory association)

viewt@ype

viewtype with unknown or abstracted length. It supersets viewtype

view

relation of a Type and a memory location. The infix @ is its most common constructor

T @ L asserts that there is a view of type T at location L

fun {a:t@ype} ptr_get0 {l:addr} (pf: a @ l | p: ptr l): @(a @ l | a)

fun {a:t@ype} ptr_set0 {l:addr} (pf: a? @ l | p: ptr l, x: a): @(a @ l | void)

the type of ptr_get0 (T) is ∀ l : addr . ( T @ l | ptr( l ) ) -> ( T @ l | T) // see manual, section 7.1. Safe Memory Access through Pointers

viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l

T?

possibly uninitialized type

propositions

dataprop expresses predicates as algebraic types

predicates:

FACT( n, r)    if and only if    fact(n) = r

MUL( n, m, prod)    iff    n * m = prod

given r = fact(n) ; r1 = fact(n-1)

FACT(n, r) = 
        FACT(0, 1) 
      | FACT(n, r) iff FACT (n-1, r1) and MUL (n, r1, r)   // for n > 0

in ATS code:

dataprop FACT (int, int) =
  | FACTbas (0, 1)                 // basic case: (fact(0) = 1)
  | {n:int | n > 0} {r,r1:int} FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r)) // inductive case

where FACT (int, int) is a proof type

Example

Non tail-recursive factorial with proposition or "Theorem" prooving through the construction dataprop.

The evaluation of fact1(n-1) returns a pair (proof_n_minus_1 | result_of_n_minus_1) which is used in the calculation of fact1(n). The proofs express the predicates of the proposition.

<source lang="ocaml"> // file fact1.dats

(*

 [FACT (n, r)] implies [fact (n) = r]
 [MUL( n, m, prod)] implies [n * m = prod]
 
 Given:
 fact(0) = 1 ;
 r1 = fact(n-1) ; r = fact(n) = n * r1 ; for n > 0

 FACT (0, 1)
 FACT (n, r) iff FACT (n-1, r1) and MUL (n, r1, r)

• )

(* to remember:

{...} universal quantification
[...] existential quantification
(... | ...)   (proof | value)
@(...) flat tuple or variadic function parameters tuple

• )

dataprop FACT (int, int) =

 | FACTbas (0, 1)                 // basic case: (fact(0) = 1)
 | {n:int | n > 0} {r,r1:int} FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r)) // inductive case

// [fact1] implements factorial without tail-recursion

fun fact1 {n:nat} .< n >. (num: int(n))

             (* {n:nat} domain
                .< n >. metrics
                (num: int(n)) parameter and type *)
 : [r:int] (FACT (n, r) | int(r))      // type of result as (proof | value)
 =
 if num > 0 then
   let
      val (pf_fact_n_minus_1 | r1) = fact1 (num-1)  // pf_fact_n_minus_1 = FACT( num-1, r1)  

      val (pf_mul | r) = num imul2 r1               // pf_mul = MUL( num, r1, r)
   in
      (FACTind (pf_fact_n_minus_1, pf_mul) | r)
   end

 else (FACTbas () | 1)

// fn introduces a non recursive function ; fun introduces a recursive one

fn abs {n:int} (num: int(n)): [r: nat] int(r) =

 if num >= 0 then num else ~num

implement main (argc, argv) : void =

 if (argc <> 2) then 
       printf ("usage: %s 9 (expected one argument only)\n", @(argv.[0]))
 else let
           val num = int1_of argv.[1]
           val nat_num = abs num
           val (pf_fact_n | res) = fact1 nat_num
      in
           printf ("factorial of %i = %i\n", @(nat_num, res))
      end

</source>

Compilation (compiles through gcc, without setting up garbage collection unless explicitly stated with -D_ATS_GCATS )

atscc fact1.dats -o fact1
./fact1 4

compiles and gives the expected result

pattern matching exhaustivity

as in case+, val+, type+, viewtype+, ...

• with suffix '+' the compiler issues an error in case of non exhaustive alternatives
• without suffix the compiler issues a warning
• with '-' as suffix, avoids exhaustivity control

modules

 staload "foo.sats" // foo.sats is loaded and then opened into the current namespace

 staload F "foo.sats" // to use identifiers qualified as $F.bar

 dynload "foo.dats" // loaded dynamically at run-time

dataview

Dataviews are often declared to encode recursively defined relations on linear resources.

dataview array_v (a: viewt@ype+, int, addr) =

  | {l:addr} array_v_none (a, 0, l)
  | {n:nat} {l:addr} array_v_some (a, n+1, l) of (a @ l, array_v (a, n, l+sizeof a))

datatype / dataviewtype

Datatypes

datatype workday = Mon | Tue | Wed | Thu | Fri

lists

datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)

dataviewtype

A dataviewtype is similar to a datatype, but it is linear. With a dataviewtype, the programmer is allowed to explicitly free (or deallocate) in a safe manner the memory used for storing constructors associated with the dataviewtype.

variables

local variables

var res: int with pf_res = 1   // introduces pf_res as an alias of view @ (res)

on stack array allocation:

var !p_buf with pf_buf = @[byte][BUFLEN](0)    // pf_buf = @[byte][BUFLEN](0) @ p_buf   

See val and var declarations

External links

• ATS home page
• Manual Draft. Some examples refer to features or routines not present in the release (Anairiats-0.1.6) (e.g.: print overload for strbuf, and using its array examples gives errmsgs like "use of array subscription is not supported".)
• ATS for ML programmers and other articles