View source for ATS (programming language)

{{short description|Programming language}}
{{Infobox programming language
| name                   = ATS
| logo                   = File:The ATS Logo.svg
| paradigm               = multi-paradigm: [[Functional programming|functional]], [[Imperative programming|imperative]]
| year                   = 
| designer               = Hongwei Xi at [[Organization:Boston University|Boston University]]
| developer              =
| latest release version = ATS2-0.4.2<ref>{{cite web |url=https://groups.google.com/g/ats-lang-users/c/ZlSW70S525Y |title=[ats-lang-users] ATS2-0.4.2 released |author=Hongwei Xi |website=ats-lang-users |date=14 Nov 2020 |access-date=17 Nov 2020}}</ref>
| latest release date    = {{Start date and age|2020|11|14}}
| typing                 = static
| implementations        = 
| dialects               = 
| influenced_by          = [[Dependent ML]], [[ML (programming language)|ML]], [[OCaml]], [[C++]]
| influenced             = 
| operating system       = 
| file ext               = .sats, .dats, .hats
| license                = [[Software:GNU General Public License|GPLv3]]
| website                = [http://www.ats-lang.org/ http://www.ats-lang.org/]
}}

In computing, '''ATS''' ('''Applied Type System''') is a [[Programming language|programming language]] designed to unify [[Computer programming|programming]] with [[Formal specification|formal specification]].  ATS has support for combining theorem proving with practical programming through the use of advanced [[Type system|type system]]s.<ref name="ats-lang.org">{{Cite web |url=http://www.ats-lang.org/MYDATA/CPwTP-icfp05.pdf |title=Combining Programming with Theorem Proving |access-date=2014-11-18 |archive-date=2014-11-29 |archive-url=https://web.archive.org/web/20141129050328/http://www.ats-lang.org/MYDATA/CPwTP-icfp05.pdf |url-status=dead }}</ref> A past version of [[The Computer Language Benchmarks Game]] has demonstrated that the performance of ATS is comparable to that of the [[C (programming language)|C]] and [[C++]] programming languages.<ref>[https://web.archive.org/web/20121218042116/http://shootout.alioth.debian.org/u64/ats.php ATS benchmarks | Computer Language Benchmarks Game] (web archive)</ref>  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|division by zero]], [[Memory leak|memory leak]]s, [[Buffer overflow|buffer overflow]], and other forms of [[Memory corruption|memory corruption]] by verifying pointer arithmetic and [[Reference counting|reference counting]] before the program compiles. Additionally, by using the integrated theorem-proving system of ATS (ATS/LF), the programmer may make use of static constructs that are intertwined with the operative code to prove that a function conforms to its specification.

== History ==
ATS is derived mostly from the [[ML (programming language)|ML]] and [[OCaml]] programming languages. An earlier language, [[Dependent ML]], by the same author has been incorporated by the language.

The latest version of ATS1 (Anairiats) was released as v0.2.12 on 2015-01-20.<ref>{{Cite web|url=https://sourceforge.net/projects/ats-lang/files/ats-lang/|title=The ATS PL System - Browse /Ats-lang at SourceForge.net}}</ref> The first version of ATS2 (Postiats) was released in September 2013.<ref>{{Cite web|url=https://github.com/githwxi/ATS-Postiats/commit/30fd556e649745f735eafbdace54373fa163862e|title=Updating: Adding a release file. · githwxi/ATS-Postiats@30fd556|website=[[GitHub]] }}</ref>

== Theorem proving ==
The primary focus of ATS is to support [[Formal verification|theorem proving]] in combination with practical programming.<ref name="ats-lang.org"/>  With theorem proving one can prove, for instance, that an implemented function does not produce memory leaks.  It also prevents other bugs that might otherwise only be found during testing.  It incorporates a system similar to those of [[Proof assistant|proof assistant]]s 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|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 (5 and the length of 'A'). A more practical example would be proving through [[Reference counting|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 leak|memory leak]]s 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 (programming language)|C]] code, but once it compiles the programmer can be certain that it is running correctly to the degree specified by their proofs (assuming the compiler and runtime system are correct).

In ATS proofs are separate from implementation, so it is possible to implement a function without proving it if the programmer so desires.

== Data representation ==
According to the author (Hongwei Xi), ATS's efficiency<ref>[https://www.reddit.com/r/programming/comments/72hmw/language_shootout_ats_is_the_new_top_gunslinger/ Discussion about the language's efficiency (Language Shootout: ATS is the new top gunslinger. Beats C++.)]</ref> is largely due to the way that data is represented in the language and [[Tail recursion|tail-call optimizations]] (which are generally important for the efficiency of functional programming languages). Data can be stored in a flat or unboxed representation rather than a boxed representation.

== Theorem Proving: An introductory case ==

=== Propositions ===
<code>dataprop</code> expresses ''[[Predicate (mathematical logic)|predicates]]'' as algebraic types.

Predicates in pseudo‑code somewhat similar to ATS source (see below for valid ATS source):

  FACT(n, r)         [[If and only if|iff]]    fact(n) = r
  MUL(n, m, prod)    [[If and only if|iff]]    n * m = prod
   
  FACT(n, r) = 
        FACT(0, 1) 
      | FACT(n, r) iff FACT(n-1, r1) and MUL(n, r1, r)   // for n > 0
  
  ''// expresses fact(n) = r  [[If and only if|iff]]  r = n * r1  and  r1 = fact(n-1)''

In ATS code:
<source lang="ocaml">
 dataprop FACT (int, int) =
   | FACTbas (0, 1)             // basic case: FACT(0, 1)
   | {n:int | n > 0} {r,r1:int} // inductive case
     FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r))
</source>

where FACT (int, int) is a proof type

=== Example ===
Non tail-recursive factorial with proposition or "[[Theorem]]" proving through the construction ''dataprop''.

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

==== Part 1 (algorithm and propositions) ====

  [FACT (n, r)] implies [fact (n) = r]
  [MUL (n, m, prod)] implies [n * m = prod]

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

To remember:

 {...} universal quantification
 [...] existential quantification
 (... | ...)   (proof | value)
 @(...) flat tuple or variadic function parameters tuple
 .<...>. termination metric<ref>{{Cite web |url=https://www.cs.bu.edu/~hwxi/ATS/TUTORIAL/contents/termination-metrics.html |title=Termination metrics |access-date=2017-05-20 |archive-date=2016-10-18 |archive-url=https://web.archive.org/web/20161018010907/http://www.cs.bu.edu/~hwxi/ATS/TUTORIAL/contents/termination-metrics.html |url-status=dead }}</ref>

<source lang="ocaml">
#include "share/atspre_staload.hats"

dataprop FACT (int, int) =
  | FACTbas (0, 1) of () // basic case
  | {n:nat}{r:int}       // inductive case
    FACTind (n+1, (n+1)*r) of (FACT (n, r))

(* note that int(x) , also int x, is the monovalued type of the int x value.

 The function signature below says:
 forall n:nat, exists r:int where fact( num: int(n)) returns (FACT (n, r) | int(r)) *)

fun fact{n:nat} .<n>. (n: int (n)) : [r:int] (FACT (n, r) | int(r)) =
(
  ifcase
  | n > 0 => ((FACTind(pf1) | n * r1)) where 
  { 
    val (pf1 | r1) = fact (n-1)
  }
  | _(*else*) => (FACTbas() | 1)
)
</source>

==== Part 2 (routines and test) ====

<source lang="ocaml">
implement main0 (argc, argv) =
{
  val () = if (argc != 2) then prerrln! ("Usage: ", argv[0], " <integer>")

  val () = assert (argc >= 2)
  val n0 = g0string2int (argv[1])
  val n0 = g1ofg0 (n0)
  val () = assert (n0 >= 0)
  val (_(*pf*) | res) = fact (n0)

  val ((*void*)) = println! ("fact(", n0, ") = ", res)
}
</source>

This can all be added to a single file and compiled as follows. Compilation should work with various back end C compilers, e.g. [[Software:GNU Compiler Collection|gcc]]. [[Garbage collection (computer science)|Garbage collection]] is not used unless explicitly stated with {{code|-D_ATS_GCATS}} )<ref>[http://www.ats-lang.org/TUTORIAL/contents/compilation.html Compilation - Garbage collection] {{webarchive |url=https://web.archive.org/web/20090804092735/http://www.ats-lang.org/TUTORIAL/contents/compilation.html |date=August 4, 2009 }}</ref>
<source lang="console">
$ patscc fact1.dats -o fact1
$ ./fact1 4
</source>
compiles and gives the expected result

== Features ==

=== Basic types ===
* bool (true, false)
* int (literals: 255, 0377, 0xFF), unary minus as ~ (as in [[ML (programming language)|ML]])
* double
* char 'a'
* string "abc"

=== Tuples and records ===
; prefix @ or none means direct, ''flat'' or unboxed allocation
<source lang="ocaml">
  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'
</source>
; prefix ' means indirect or boxed allocation
<source lang="ocaml">
  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'
</source>

; 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|variadic function]] parameters tuple (see example's ''printf'')
 
 @[byte][BUFLEN]     type of an array of BUFLEN values of type ''byte''<ref>[http://www.ats-lang.org/DOCUMENTATION/MISC/manual_main.pdf#page=65 type of an array] {{webarchive |url=https://web.archive.org/web/20110904160146/http://www.ats-lang.org/DOCUMENTATION/MISC/manual_main.pdf#page=65 |date=September 4, 2011 }} types like  @[T][I]</ref>
 @[byte][BUFLEN]()   array instance
 @[byte][BUFLEN](0)  array initialized to 0

=== Dictionary ===
{{glossary begin}}
{{term|sort:domain}}
<dd><div>
 sortdef nat = {a: int | a >= 0 }     // from prelude: ∀ ''a'' ∈ int ...

 typedef String = [a:nat] string(a)   // [..]: ∃ ''a'' ∈ nat ...
</div></dd>
{{term|type (as sort)}}<dd>generic ''sort'' for elements with the length of a pointer word, to be used in type parameterized polymorphic functions. Also "boxed types"<ref name="introdep">{{Cite web |url=http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/c2232.html |title=Introduction to Dependent types |access-date=2016-02-13 |archive-url=https://web.archive.org/web/20160312024014/http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/c2232.html |archive-date=2016-03-12 |url-status=dead }}</ref>
<div>
 // {..}: ∀ a,b ∈ type ...
 fun {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0)
</div>
</dd>
{{term|t@ype}}{{defn| linear version of previous ''type'' with abstracted length. Also unboxed types.<ref name="introdep"/>}}

{{term|viewtype}}{{defn| a domain class like ''type'' with a ''view'' (memory association)}}

{{term|viewt@ype}}{{defn| linear version of ''viewtype'' with abstracted length. It supersets ''viewtype''}}

{{term|view}}<dd>relation of a Type and a memory location. The infix {{mono|@}} is its most common constructor
:{{code|T @ L}} asserts that there is a view of type T at location L
<source lang="ocaml">
 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)
</source>
:the type of <code>ptr_get0 (T)</code> is <code>∀ l : addr . ( T @ l | ptr( l ) ) -> ( T @ l | T)    // see manual, section 7.1. Safe Memory Access through Pointers</code><ref>[http://www.ats-lang.org/htdocs-old/DOCUMENT/MISC/manual_main.pdff#page=61 Manual, section 7.1. Safe Memory Access through Pointers]{{dead link|date=October 2016 |bot=InternetArchiveBot |fix-attempted=yes }} (outdated)</ref>
<div>
 viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l
</div>
</dd>
{{term|T? }}{{defn|possibly uninitialized type}}
{{glossary end}}

=== 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 ===
<pre>
 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
</pre>

=== dataview ===
Dataviews are often declared to encode recursively defined relations on linear resources.<ref>[http://www.ats-lang.org/TUTORIAL/contents/dataviews.html Dataview construct] {{webarchive |url=https://web.archive.org/web/20100413053430/http://www.ats-lang.org/TUTORIAL/contents/dataviews.html |date=April 13, 2010 }}</ref>

 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<ref>[http://www.ats-lang.org/TUTORIAL/contents/datatypes.html Datatype construct] {{webarchive |url=https://web.archive.org/web/20100414020420/http://www.ats-lang.org/TUTORIAL/contents/datatypes.html |date=April 14, 2010 }}</ref>
 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.<ref>[https://github.com/githwxi/ATS-Postiats/wiki/dataviewtype Dataviewtype construct]</ref>

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

''on stack'' array allocation:
 #define BUFLEN 10
 var !p_buf with pf_buf = @[byte][BUFLEN](0)    // pf_buf = @[byte][BUFLEN](0) @ p_buf<ref>[http://www.ats-lang.org/htdocs-old/DOCUMENT/MISC/manual_main.pdf#page=64 Manual - 7.3 Memory allocation on stack] {{webarchive |url=https://web.archive.org/web/20140809193400/http://www.ats-lang.org/htdocs-old/DOCUMENT/MISC/manual_main.pdf#page=64 |date=August 9, 2014 }} (outdated)</ref>

See ''val'' and ''var '' declarations<ref>[http://www.ats-lang.org/htdocs-old/TUTORIAL/contents/val-and-var.html Val and Var declarations] {{webarchive |url=https://web.archive.org/web/20140809193101/http://www.ats-lang.org/htdocs-old/TUTORIAL/contents/val-and-var.html |date=August 9, 2014 }} (outdated)</ref>

== References ==
<references/>

== External links ==
* [http://www.ats-lang.org/ ATS home page]
* [http://www.ats-lang.org/Documents.html The ATS Programming Language] {{Webarchive|url=https://web.archive.org/web/20141205101556/http://www.ats-lang.org/Documents.html |date=2014-12-05 }} Documentation for ATS2
* [http://ats-lang.sourceforge.net/DOCUMENT/ The ATS Programming Language] Old documentation for ATS1
* [http://ats-lang.sourceforge.net/htdocs-old/DOCUMENT/MISC/manual_main.pdf Manual] Draft (outdated). 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".)
* [http://cs.likai.org/ats/ml-programmers-guide-to-ats ATS for ML programmers]
* [http://bluishcoder.co.nz/tags/ats/ Learning examples and short use‑cases of ATS]

[[Category:Multi-paradigm programming languages]]
[[Category:Declarative programming languages]]
[[Category:Functional languages]]
[[Category:Dependently typed languages]]
[[Category:Systems programming languages]]

{{Sourceattribution|ATS (programming language)}}