ATS (programming language)

In computing, ATS (Applied Type System) 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 (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 diverse programming paradigms, such as functional, imperative, object-oriented, concurrent, and modular. 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) = r iff r = n * r1 and r1 = fact(n-1) In ATS code: 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)) where is a proof type [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 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: 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) ) implement main0 (argc, argv) = { val () = if (argc != 2) then prerrln! ("Usage: ", argv[0], " ") 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) } 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 ) $ patscc fact1.dats -o fact1 $ ./fact1 4 compiles and gives the expected result 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 sortdef nat = {a: int | a >= 0 } // from prelude: ∀ a ∈ int ... typedef String = [a:nat] string(a) // [..]: ∃ 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 {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0) relation of a Type and a memory location. The infix is its most common constructor 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 viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l 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 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 workday = Mon | Tue | Wed | Thu | Fri lists datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a) 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 See val and var declarations

Text derived from https://en.wikipedia.org/w/index.php?oldid=1360574130 under CC BY-SA 4.0; modifications have been made.

Names in other languages