ATS (programming language)

In computing, ATS is a multi-paradigm, general-purpose, high-level, functional programming language. It is a dialect of the programming language ML, designed by Hongwei Xi to unify computer programming with formal specification. ATS has support for combining theorem proving with practical programming through the use of advanced type systems. A past version of The Computer Language Benchmarks Game has demonstrated that the performance of ATS is comparable to that of the languages C and C++. By using theorem proving and strict type checking, the compiler can detect and prove that its implemented functions are not susceptible to bugs such as division by zero, memory leaks, buffer overflow, and other forms of memory corruption by verifying pointer arithmetic and reference counting before the program runs. Also, by using the integrated theorem-proving system of ATS, the programmer may make use of static constructs that are intertwined with the operative code to prove that a function conforms to its specification.
ATS consists of a static component and a dynamic component. The static component is used for handling types, whereas the dynamic component is used for programs. While ATS primarily relies on a call-by-value functional language at its core, it possesses the ability to accommodate diverse programming paradigms, such as functional, imperative, object-oriented, concurrent, and modular.

History

According to the author, ATS was inspired by Per Martin-Löf's constructive type theory, which was originally developed for the purpose of establishing a foundation for mathematics. Xi designed ATS “in an attempt to combine specification and implementation into a single programming language.”
ATS is derived mostly from the languages ML and OCaml. An earlier language, Dependent ML, by the same author has been incorporated into ATS.
The first implementation, ATS/Proto, was written in OCaml and was released in 2006. This was the pre-first edition of ATS and is no longer maintained. A year later, ATS/Geizella, the first implementation of ATS1, was released. This version was also written in OCaml and is no longer used actively.
The second version of ATS1, ATS/Anairiats, released in 2008, was a major milestone in the development of the language, as the language was able to bootstrap itself. This version was written almost completely in ATS1. The current version, ATS/Postiats was released in 2013. Like its predecessor, this version is also almost entirely written in ATS1. The most recently released version is ATS2-0.4.2.

Future

, ATS is used mostly for research; fewer than 200 GitHub repositories contain code written in ATS. This is far less than other functional languages, such as OCaml and Standard ML, which have over 16,000 and 3,000 repositories, respectively. This is likely due to the steep learning curve associated with ATS, which is present because of the language's use of dependent type-checking and template instance resolution. These features usually require the use of explicit quantifiers, which demand further learning.
, ATS/Xanadu is being developed actively in ATS2, with the hope of reducing the learning needed by two main improvements:

Adding an extra layer to ATS2 to support ML-like algebraic type-checking
Type-based metaprogramming using algebraic types only

With these improvements, Xi hopes for ATS to become much more accessible and easier to learn. The main goal of ATS3 is to transform ATS from a language mainly used for research, into one strong enough for large-scale industrial software development.

Theorem proving

The main focus of ATS is to support formal verification via automated theorem proving, combined with practical programming. Theorem proving can prove, for example, that an implemented function produces no memory leaks. It can also prevent other bugs that might otherwise be found only during testing. It incorporates a system similar to those of proof assistants which usually only aim to verify mathematical proofs—except ATS uses this ability to prove that the implementations of its functions operate correctly, and produce the expected output.
As a simple example, in a function using division, the programmer may prove that the divisor will never equal zero, preventing a division by zero error. Let's say, the divisor 'X' was computed as 5 times the length of list 'A'. One can prove, that in the case of a non-empty list, 'X' is non-zero, since 'X' is the product of two non-zero numbers. A more practical example would be proving through reference counting that the retain count on an allocated block of memory is being counted correctly for each pointer. Then one can know, and quite literally prove, that the object will not be deallocated prematurely, and that memory leaks will not occur.
The benefit of the ATS system is that since all theorem proving occurs strictly within the compiler, it has no effect on the speed of the executable program. ATS code is often harder to compile than standard C code, but once it compiles, it is certain that it is running correctly to the degree specified by the proofs.
In ATS proofs are separate from implementation, so it is possible to implement a function without proving it, if desired.

Data representation

According to the author, ATS's efficiency is largely due to the way that data is represented in the language and tail-call optimizations. Data can be stored in a flat or unboxed representation rather than a boxed representation.

Theorem proving: An introductory case

Propositions

dataprop expresses predicates as algebraic types.
Predicates in pseudo‑code somewhat similar to ATS source :
FACT iff fact = r
MUL iff n * m = prod

FACT =
FACT
| FACT iff FACT and MUL // for n > 0

// expresses fact = r iff r = n * r1 and r1 = fact

In ATS code:

dataprop FACT =
| FACTbas // basic case: FACT
| // inductive case
FACTind of, MUL )

where is a proof type

Example

Non tail-recursive factorial with proposition or "Theorem" proving through the construction dataprop.
The evaluation of returns a pair which is used in the calculation of. The proofs express the predicates of the proposition.

Part 1 (algorithm and propositions)

implies
implies
FACT
FACT iff FACT and MUL forall n > 0

To remember:
universal quantification
existential quantification

@ flat tuple or variadic function parameters tuple
.<...>. termination metric

include "share/atspre_staload.hats"

Part 2 (routines and test)

implement main0 =

This can all be added to a single file and compiled as follows. Compiling should work with various back end C compilers, e.g., GNU Compiler Collection

$ patscc fact1.dats -o fact1
$./fact1 4

compiles and gives the expected result

Features

Basic types

bool
int, unary minus as ~
double
char 'a'
string "abc"
Tuples and records
prefix @ or none means direct, flat or unboxed allocation
:

val x : @ = @ // x.0 = 15 ; x.1 = 'c'
val @ = x // pattern matching binding, a= 15, b='c'
val x = @ // x.first = 15
val @ = x // a= 15, b='c'
val @ = x // with omission, b='c'

prefix ' means indirect or boxed allocation
:

val x : ' = ' // x.0 = 15 ; x.1 = 'c'
val ' = x // a= 15, b='c'
val x = ' // x.first = 15
val ' = x // a= 15, b='c'
val ' = x // b='c'

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

val = myfunct params

Common

universal quantification
existential quantification
parenthetical expression or tuple

.<...>. termination metric
@ flat tuple or variadic function parameters tuple
@ type of an array of BUFLEN values of type byte
@ array instance
@ array initialized to 0

Dictionary

sortdef nat = // from prelude: ∀ a ∈ int...
typedef String = string // : ∃ a ∈ nat...

generic sort for elements with the length of a pointer word, to be used in type parameterized polymorphic functions. Also "boxed types"

// : ∀ a,b ∈ type...
fun swap_type_type : @ =

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

fun ptr_get0 : @
fun ptr_set0 : @

viewdef array_v = @ @ l

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