ATS (programming language)

From Seo Wiki - Search Engine Optimization and Programming Languages

Jump to: navigation, search
ATS
Paradigm multi-paradigm: imperative, functional
Designed by Hongwei Xi at the Boston University
Influenced by ML, Objective Caml
Website http://www.ats-lang.org/

ATS (Applied Type System) is a programming language whose stated purpose is to support theorem proving in combination with practical programming through the use of advanced type systems. The performance of ATS has been demonstrated to be comparable to that of the C and C++ programming languages.[1]

Contents

History

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

Theorem proving

The primary focus of ATS is to support theorem proving in combination with practical programming.[2]

Data representation

According to the author (Hongwei Xi), ATS's efficiency[3] is largely due to the way that data is represented in the language and tail-call optimizations (which are generally important for the efficiency of functional programming languages). Data is stored in a flat or unboxed representation rather than a boxed representation.

Features

Basic types

  • bool (true, false)
  • int ( 255, 0377, 0xFF), unary minus as ~
  • 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_proof | value) = myfunct params

Common

{...} universal quantification
[...] existential quantification
(...) parentsized expression or tuple

(... | ...)   (proof | value)

@(...) flat tuple or variadic function parameters tuple (see example's printf)

Dictionary

sort
domain of a variable
sortdef nat = {a: int | a >= 0 } // from prelude
type (as sort)
sort class for elements with the length of a pointer word, to be used in polymorphic functions
fun {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0)
t@ype
sort class with length unknown or abstracted length. It supersets type
viewtype
a sort class like type with a view (memory association)
viewt@ype
viewtype with unknown or 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) // see manual, section 7.1. Safe Memory Access through Pointers[4]
viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l
T? 
possibly uninitialized type

propositions

dataprop expresses predicates as algebraic types

predicates:

FACT( n, r)    if and only if    fact(n) = r
MUL( n, m, prod)    iff    n * m = prod

given r = fact(n) ; r1 = fact(n-1)

FACT(n, r) = 
        FACT(0, 1) 
      | FACT(n, r) iff FACT (n-1, r1) and MUL (n, r1, r)   // for n > 0

in ATS code:

dataprop FACT (int, int) =
  | FACTbas (0, 1)                 // basic case: (fact(0) = 1)
  | {n:int | n > 0} {r,r1:int} FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r)) // inductive case

where FACT (int, int) is a proof type

Example

Non tail-recursive factorial with proposition or "Theorem" prooving through the construction dataprop.

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

// file fact1.dats
 
(*
  [FACT (n, r)] implies [fact (n) = r]
  [MUL( n, m, prod)] implies [n * m = prod]
 
  Given:
  fact(0) = 1 ;
  r1 = fact(n-1) ; r = fact(n) = n * r1 ; for n > 0
 
  FACT (0, 1)
  FACT (n, r) iff FACT (n-1, r1) and MUL (n, r1, r)
*)
 
(* to remember:
 {...} universal quantification
 [...] existential quantification
 (... | ...)   (proof | value)
 @(...) flat tuple or variadic function parameters tuple
*)
 
dataprop FACT (int, int) =
  | FACTbas (0, 1)                 // basic case: (fact(0) = 1)
  | {n:int | n > 0} {r,r1:int} FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r)) // inductive case
 
// [fact1] implements factorial without tail-recursion
 
fun fact1 {n:nat} .< n >. (num: int(n))
              (* {n:nat} domain
                 .< n >. metrics
                 (num: int(n)) parameter and type *)
  : [r:int] (FACT (n, r) | int(r))      // type of result as (proof | value)
  =
  if num > 0 then
    let
       val (pf_fact_n_minus_1 | r1) = fact1 (num-1)  // pf_fact_n_minus_1 = FACT( num-1, r1)  
 
       val (pf_mul | r) = num imul2 r1               // pf_mul = MUL( num, r1, r)
    in
       (FACTind (pf_fact_n_minus_1, pf_mul) | r)
    end
 
  else (FACTbas () | 1)
 
 
// ''fn'' introduces a non recursive function ; ''fun'' introduces a recursive one
 
fn abs {n:int} (num: int(n)): [r: nat] int(r) =
 
  if num >= 0 then num else ~num
 
 
implement main (argc, argv) : void =
 
  if (argc <> 2) then 
        printf ("usage: %s 9 (expected one argument only)\n", @(argv.[0]))
  else let
            val num = int1_of argv.[1]
            val nat_num = abs num
            val (pf_fact_n | res) = fact1 nat_num
       in
            printf ("factorial of %i = %i\n", @(nat_num, res))
       end

Compilation (compiles through gcc, without setting up garbage collection unless explicitly stated with -D_ATS_GCATS )[5]

atscc fact1.dats -o fact1
./fact1 4

compiles and gives the expected result

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

dataview

Dataviews are often declared to encode recursively defined relations on linear resources.[6]

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[7]

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.[8]

variables

local variables

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

on stack array allocation:

var !p_buf with pf_buf = @[byte][BUFLEN](0)    // pf_buf = @[byte][BUFLEN](0) @ p_buf   [9]

See val and var declarations[10]

External links

References

  1. ATS benchmarks | Computer Language Benchmarks Game
  2. Combining Programming with Theorem Proving
  3. Discussion about the language's efficiency (Language Shootout: ATS is the new top gunslinger. Beats C++.)
  4. Manual, section 7.1. Safe Memory Access through Pointers
  5. Compilation - Garbage collection
  6. Dataview construct
  7. Datatype construct
  8. Dataviewtype construct
  9. Manual - 7.3 Memory allocation on stack
  10. Val and Var declarations
ca:ATS (llenguatge de programació)

ru:ATS (язык программирования)

Personal tools

Served in 0.244 secs.