 | This article has multiple issues. Please helpimprove it or discuss these issues on thetalk page.(Learn how and when to remove these messages) (Learn how and when to remove this message)
|
| ATS | |
|---|---|
 | |
| Paradigms | multi-paradigm:functional,imperative,object-oriented,concurrent,modular |
| Family | ML:Caml:OCaml:Dependent ML |
| Designed by | Hongwei Xi |
| Developer | Boston University |
| First appeared | 2006; 19 years ago (2006) |
| Stable release | |
| Typing discipline | static,dependent |
| License | GPLv3 |
| Filename extensions | .sats, .dats, .hats |
| Website | www |
| Influenced by | |
| Dependent ML,ML,OCaml,C++ | |
In computing,ATS (Applied Type System) is amulti-paradigm,general-purpose,high-level,functionalprogramming language. It is adialect of the programming languageML, designed by Hongwei Xi to unifycomputer programming withformal specification. ATS has support for combiningtheorem proving with practical programming through the use of advancedtype systems.[2] A past version ofThe Computer Language Benchmarks Game has demonstrated that the performance of ATS is comparable to that of the languagesC andC++.[3] By using theorem proving and strict type checking, the compiler can detect and prove that its implemented functions are not susceptible to bugs such asdivision by zero,memory leaks,buffer overflow, and other forms ofmemory corruption by verifyingpointer arithmetic andreference counting before the program runs. Also, 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.
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 diverseprogramming paradigms, such asfunctional,imperative,object-oriented,concurrent, andmodular.
According to the author, ATS was inspired byPer Martin-Löf'sconstructive 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.”[4]
ATS is derived mostly from the languagesML andOCaml. An earlier language,Dependent ML, by the same author has been incorporated into ATS.
The first implementation, ATS/Proto (ATS0), 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.[5]
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 tobootstrap itself. This version was written almost completely in ATS1. The current version, ATS/Postiats (ATS2) 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.[5]
As of 2024[update], ATS is used mostly for research; fewer than 200GitHub 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 associated with ATS, which is present because of the language's use ofdependent type-checking and template instance resolution. These features usually require the use of explicitquantifiers, which demand further learning.[6]
As of 2024[update], ATS/Xanadu (ATS3) is being developed actively in ATS2, with the hope of reducing the learning needed by two main improvements:
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.[5]
The main focus of ATS is to supportformal verification viaautomated theorem proving, combined with practical programming.[2] 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 ofproof 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 adivision 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 throughreference 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 thatmemory 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 standardC code, but once it compiles, it is certain that it is running correctly to the degree specified by the 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 desired.
According to the author, ATS's efficiency[7] is largely due to the way that data is represented in the language andtail-call optimizations (which are generally important for the efficiency of functional languages). Data can be stored in a flat or unboxed representation rather than a boxed representation.
dataprop expressespredicates asalgebraic types.
Predicates in pseudo‑code somewhat similar to ATS source (see below for valid ATS source):
FACT(n, r)iff fact(n) = r MUL(n, m, prod)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) = riff r = n * r1 and r1 = fact(n-1)
In ATS code:
datapropFACT(int,int)=|FACTbas(0,1)// basic case: FACT(0, 1)|{n:int|n>0}{r,r1:int}// inductive caseFACTind(n,r)of(FACT(n-1,r1),MUL(n,r1,r))
where FACT (int, int) is a proof type
Non tail-recursive factorial with proposition or "Theorem" proving through the constructiondataprop.
The evaluation offact1(n-1) returns a pair(proof_n_minus_1 | result_of_n_minus_1) which is used in the calculation offact1(n). The proofs express the predicates of the proposition.
[FACT(n,r)]implies[fact(n)=r][MUL(n,m,prod)]implies[n*m=prod]FACT(0,1)FACT(n,r)iffFACT(n-1,r1)andMUL(n,r1,r)foralln>0
To remember:
{...} universal quantification[...] existential quantification(... | ...) (proof | value)@(...) flat tuple or variadic function parameters tuple.<...>. termination metric[8]#include"share/atspre_staload.hats"datapropFACT(int,int)=|FACTbas(0,1)of()//basiccase|{n:nat}{r:int}//inductivecaseFACTind(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)) *)funfact{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))
implementmain0(argc,argv)={val()=if(argc!=2)thenprerrln!("Usage: ",argv[0]," <integer>")val()=assert(argc>=2)valn0=g0string2int(argv[1])valn0=g1ofg0(n0)val()=assert(n0>=0)val(_(*pf*)|res)=fact(n0)val((*void*))=println!("fact(",n0,") = ",res)}
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 (gcc).Garbage collection is not used unless explicitly stated with-D_ATS_GCATS )[9]
$patsccfact1.dats-ofact1$./fact14
compiles and gives the expected result
valx:@(int,char)=@(15,'c')// x.0 = 15 ; x.1 = 'c'val@(a,b)=x// pattern matching binding, a= 15, b='c'valx=@{first=15,second='c'}// x.first = 15val@{first=a,second=b}=x// a= 15, b='c'val@{second=b,...}=x// with omission, b='c'
valx:'(int,char)='(15,'c')// x.0 = 15 ; x.1 = 'c'val'(a,b)=x// a= 15, b='c'valx='{first=15,second='c'}// x.first = 15val'{first=a,second=b}=x// a= 15, b='c'val'{second=b,...}=x// b='c'
| as separator, some functions return wrapped the result value with an evaluation of predicatesval ( predicate_proofs | values) = myfunct params
{...} universal quantification[...] existential quantification(...) parenthetical expression or tuple(... | ...) (proofs | values).<...>. termination metric@(...) flat tuple orvariadic function parameters tuple (see example'sprintf)@[byte][BUFLEN] type of an array of BUFLEN values of typebyte[10]@[byte][BUFLEN]() array instance@[byte][BUFLEN](0) array initialized to 0
sortdefnat={a:int|a>=0}// from prelude: ∀ ''a'' ∈ int ...typedefString=[a:nat]string(a)// [..]: ∃ ''a'' ∈ nat ...
// {..}: ∀ a,b ∈ type ...fun{a,b:type}swap_type_type(xy:@(a,b)):@(b,a)=(xy.1,xy.0)
T @ L asserts that there is a view of type T at location Lfun{a:t@ype}ptr_get0{l:addr}(pf:a@l|p:ptrl):@(a@l|a)fun{a:t@ype}ptr_set0{l:addr}(pf:a?@l|p:ptrl,x:a):@(a@l|void)
ptr_get0 (T) is∀ l : addr . ( T @ l | ptr( l ) ) -> ( T @ l | T) // see manual, section 7.1. Safe Memory Access through Pointers[12]viewdefarray_v(a:viewt@ype,n:int,l:addr)=@[a][n]@l
as incase+,val+,type+,viewtype+, ...
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
Dataviews are often declared to encode recursively defined relations on linear resources.[13]
dataviewarray_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+sizeofa))
Datatypes[14]
datatype workday = Mon | Tue | Wed | Thu | Fri
lists
datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)
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.[15]
local variables
var res: int with pf_res = 1 // introduces pf_res as an alias ofview @ (res)
on stack array allocation:
#define BUFLEN 10var!p_bufwithpf_buf=@[byte][BUFLEN](0)// pf_buf = @[byte][BUFLEN](0) @ p_buf
Seeval andvar declarations[17]
ML programming | ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Software |
|  | ||||||||||||
| Community |
| |||||||||||||
 Book Category:Family:MLCategory:Family:OCamlCategory:Software:OCaml | ||||||||||||||