# ATS (programming language)

This page was last modified on 8 June 2016, at 21:49.

Paradigm | multi-paradigm: imperative, functional |
---|---|

Designed by | Hongwei Xi at the Boston University |

Stable release | ATS2-0.2.5 / 2015-12-22 |

License | GPLv3 |

Website | http://www.ats-lang.org/ |

## Contents

## What is ATS

**ATS** is a statically typed programming language that unifies implementation with formal specification. It is equipped with a highly expressive type system rooted in the framework Applied Type System, which gives the language its name. In particular, both dependent types and linear types are available in ATS.

The current implementation of ATS2 (ATS/Postiats) is written in ATS1 (ATS/Anairiats), consisting of more than 150K lines of code. ATS can be as efficient as C/C++ both time-wise and memory-wise and supports a variety of programming paradigms that include:

- Functional programming. The core of ATS is a call-by-value functional language inspired by ML. The availability of linear types in ATS often makes functional programs written in it run not only with surprisingly high efficiency (when compared to C) but also with surprisingly small (memory) footprint (when compared to C as well).

- Imperative programming. The novel approach to imperative programming in ATS is firmly rooted in the paradigm of programming with theorem-proving. The type system of ATS allows many features considered dangerous in other languages (such as explicit pointer arithmetic and explicit memory allocation/deallocation) to be safely supported in ATS, making ATS well-suited for implementing high-quality low-level systems.

- Concurrent programming. ATS can support multithreaded programming through safe use of pthreads. The availability of linear types for tracking and safely manipulating resources provides an effective approach to constructing reliable programs that can take great 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 subsystem ATS/LF that supports a form of (interactive) theorem-proving, where proofs are constructed as total functions. With this subsystem, ATS is able to advocate a programmer-centric approach to program verification that combines programming with theorem-proving in a syntactically intertwined manner. Furthermore, ATS/LF can also serve as a logical framework (LF) for encoding various formal systems (such as logic systems and type systems) together with proofs of their (meta-)properties.

## History

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

## Features

### Basic types

- bool (true, false)
- int (literals: 255, 0377, 0xFF), unary minus as ~ (as in ML)
- 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_proofs | values) = myfunct params`

### Common

{...} universal quantification [...] existential quantification (...) parenthetical expression or tuple (... | ...) (proofs | values)

.<...>. termination metric @(...) flat tuple or variadic function parameters tuple (see example'sprintf) @[byte][BUFLEN] type of an array of BUFLEN values of type byte @[byte][BUFLEN]() array instance @[byte][BUFLEN](0) array initialized to 0

### Dictionary

- sort
- domain

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

typedef String = [a:nat] string(a) // [..]: ∃a∈ nat ...

- type (as sort)
- generic
*sort*for elements with the length of a pointer word, to be used in type parameterized polymorphic functions.

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

- t@ype
- linear version of previous
*type*with abstracted length. Also unboxed types.

- viewtype
- a domain class like
*type*with a*view*(memory association)

- viewt@ype
- linear version of
*viewtype*with 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)

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

- T?
- possibly uninitialized type

### 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
```

### Variables

local variables

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

*on stack* array allocation:

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

## Присоединяйся к команде

ISSN:

## Следуй за Полисом

Оставайся в курсе последних событий

## License

Except as otherwise noted, the content of this page is licensed under the Creative Commons Creative Commons «Attribution-NonCommercial-NoDerivatives» 4.0 License, and code samples are licensed under the Apache 2.0 License. See Terms of Use for details.