# ATS (llenguatge de programació)

ATS (Applied Type System) és un llenguatge de programació dissenyat per Hongwei Xi a la Universitat de Boston que incorpora "Tipus dependents de valors" i altres sistemes de tipus avançats així com construccions per assegurar la correcta finalització de les funcions entre les quals hi ha anotacions de mètrica i un sistema de proposicions i proves (predicats).
El llenguatge parteix del cos del llenguatge ML Estàndard incorporant-hi construccions per a proveir els mecanismes avançats.

## Història

ATS deriva d'una versió anterior anomenada DML ó Dependent ML
També hi ha antecedents en el "De Caml" versió de Caml Light amb "tipus dependents de valors" del mateix autor.

## Eficiència

Segons l'autor Hongwei Xi la seva eficiència és deguda a la representació de dades i optimització de la recursivitat final. Els tipus són principalment per a assegurar la correcció.

## Un cas introductori
### proposicions

dataprop expressa predicats com un tipus algebraic
Predicats:
    FACT(n, r) =
       FACTbase (0, 1)
       | FACTinductiu (n, r) si i només si FACT (n-1, r1) i MUL (n, r1, r) ∀ n,r,r1 ∈ Int; n > 0
       // expressa r = fact(n) si i només si r = n * r1 i r1 = fact(n-1)
en codi ATS

### aplicació

L'avaluació de fact1(n-1) torna un parell (predicat_n_menys_1 | resultat_n_menys_1) que es fa servir en el càlcul de fact1(n).
rutines i principal:
Compilació (compila mitjançant gcc, sense recollidor de memòria brossa excepte si s'especifica explícitament amb l'opció -D_ATS_GCATS
dona el resultat esperat

## Característiques
### Detalls comuns

ATS utilitza quantificadors universals i existencials així com tipus d'un sol valor (anomenats tipus singleton)

### Tipus bàsics

* bool (true, false)
* int (255, 0377, 0xFF) El signe menys és ~
* double
* char 'a'
* string "abc"

### Tuples i registres
#### amb allotjament indirecte (anomenat boxed)

    al munt (ang:heap), amb l'apòstrof de prefix

#### amb allotjament directe (anomenat flat)

    amb @ de prefix, obviable en la construcció @(a, b) = (a, b) però no en l'encaix de patrons.

#### especial
### Diccionari
#### sort

    univers o domini de valors

#### type (com a domini)

    domini polimòrfic associat a tipus que ocupen exactament una paraula de màquina (llargada d'un punter).

#### t@ype

    type lineal de llargada desconeguda o, dit d'una altra manera, amb abstracció de llargada
    l'univers t@ype inclou els type

#### view

    és una relació d'una posició de memòria i un tipus que l'interpreta, amb caràcter de prova o predicat.
    El constructor de views més freqüent és el @ en posició infix. Així T @ L és una prova de la relació interpretativa de la posició L amb el tipus T.
    El tipus de ptr_get0[T] és ∀ l : addr . (T @ l | ptr (l)) -> (T @ l | T) // vegeu manual, secció 7.1. Safe Memory Access through Pointers

#### viewtype

    sort "type" amb associació a memòria (view).

#### viewt@ype

    viewtype de llargada desconeguda o, dit d'una altra manera, amb abstracció de llargada.
    l'univers viewt@ype inclou els viewtype

### sorts

Univers o domini de valors
ús en especificació de paràmetre:tipus
algebraics

### datatypes a la ML

llistes:

### exhaustivitat en l'encaix de patrons (sufixos + -)

com a case+, val+, type+, viewtype+, ...
* El sufix + genera un error, en cas que les alternatives de l'encaix no siguin exhaustives
* La manca de sufix genera un missatge d'atenció (literal warning) si no hi ha exhaustivitat
* El sufix - evita la comprovació d'exhaustivitat

## Extensions dels fitxers
### .sats

    signatura o interfície, també anomenada fitxer d'estàtics

### .dats

    implementació, també anomenada fitxer de dinàmics

### .hats

    fitxer a incloure, el contingut pot ser tant d'interfície com d'implementació

### .cats

    fitxer amb continguts de codi C

## Mòduls

Codi dels mòduls:

## vectors

Diverses construccions i proves
* del manual
* de la web->Tutorial->Linear Arrays
* : @[VT][N] és un viewtype de vectors d'elements del tipus VT, la seva llargada és N vegades la llargada de VT
* : Un viewt@ype és un viewtype de llargada desconeguda o, dit d'una altra manera, amb abstracció de llargada
* de la web->Tutorial->Dataviews
Una dataview (vista) és una proposició de lògica lineal que es fa servir per especificar relacions recursives en recursos d'estructura lineal.

## Referències

* ↑ ATS - anotacions de mètrica Arxivat 2010-04-13 a Wayback Machine.(anglès)
* ↑ Programant amb Prova de Teoremes Arxivat 2009-08-06 a Wayback Machine.(anglès)
* 1 2 DML (Dependent ML) i "De Caml" Arxivat 2009-12-13 a Wayback Machine.(anglès)
* ↑ «Compilació - Recollidor de memòria brossa». Arxivat de l'original el 2009-08-04. [Consulta: 30 gener 2010].
* ↑ Safe Programming with Pointers through Stateful Views Arxivat 2011-12-28 a Wayback Machine.(anglès)
* ↑ Manual Arxivat 2011-09-04 a Wayback Machine.(anglès)
* ↑ Linear Arrays Arxivat 2010-04-13 a Wayback Machine.(anglès)
* 1 2 ATS-lang.org - Dataviews - vectors Arxivat 2010-04-13 a Wayback Machine.(anglès)

## Enllaços externs

* Pàgina inicial del llenguatge ATS (anglès)
* Manual Arxivat 2011-09-04 a Wayback Machine. (anglès) Esborrany (conté exemples amb rutines o característiques no implementades en la versió actual (Anairiats-0.1.6))
* Shootout a Debian.org - ATS contra C++ Arxivat 2012-12-18 a Wayback Machine. (anglès) Banc de proves de llenguatges com a reptes un contra un
* ATS per a programadors en llenguatge ML i altres articles (anglès)
* Combining programming with theorem proving Arxivat 2009-12-22 a Wayback Machine. (anglès) Combinant programació amb comprovació de teoremes.
Viccionari