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ètricaATS - anotacions de mètrica i un sistema de proposicions i proves (predicats).Programant amb Prova de Teoremes
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 MLDML (Dependent ML) i "De Caml"
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) si i només si fact(n) = r MUL(n, m, prod) si i només si n * m = prod
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 dataprop FACT (int, int) = | FACTbas (0, 1) // cas base: (fact(0) = 1) // cas inductiu | {n:int | n > 0} {r,r1:int} FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r))
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).
// fitxer fact1.dats (1a. part)
(* [FACT (n, r)] és una proposició certa si i només si [fact (n) = r] [MUL(n, m, prod)] és una proposició certa si i només si [n * m = prod]
{...} indica quantificació universal […] indica quantificació existencial (...) tuples a (... | ...), | separa prova i valor les variables amb prefix pf_ responen a l'abreviació de l'anglès "proof" (cat: prova (predicat en aquest cas))
fact(0) = 1 ; r1 = fact(n-1); r = fact(n) = n * r1; per a n > 0 * )
dataprop FACT (int, int) = | FACTbas (0, 1) // cas base: (fact(0) = 1) | {n:int | n > 0} {r,r1:int} FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r)) // cas inductiu
// fact1 implementa la funció factorial sense recursivitat final // int(n) o també ''int n'' és el tipus enter monovalor de valor n
fun fact1 {n:nat} .< n >. (num: int(n)) (* {n:nat} univers .< n >. mètrica (num: int(n)) paràmetre i tipus *) : [r:int] (FACT (n, r) | int(r)) // tipus del resultat, retorna un parell (predicat | valor) = if num > 0 then let val (prova_fact_n_menys_1 | r1) = fact1 (num-1) // prova_fact_n_menys_1 = FACT(num-1, r1) val (prova_mul | r) = num imul2 r1 // prova_mul = MUL(num, r1, r) in (FACTind (prova_fact_n_menys_1, prova_mul) | r) end else (FACTbas () | 1)
rutines i principal:
// fitxer fact1.dats (2a. part) // ''fn'' introdueix funció no recursiva; ''fun'' introdueix funció recursiva (admet mètrica)
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 ("us: %s 99 (un argument i prou)\n", @(argv.)) else let val num = int1_of argv. val num_nat = abs num val (prova_fact_n | res) = fact1 num_nat in printf ("factorial de %i = %i\n", @(num_nat, res)) end
Compilació (compila mitjançant gcc, sense recollidor de memòria brossa excepte si s'especifica explícitament amb l'opció -D_ATS_GCATS atscc fact1.dats -o fact1 ./fact1 4 dona el resultat esperat factorial de 4 = 24
Característiques Detalls comuns ATS utilitza quantificadors universals i existencials així com tipus d'un sol valor (anomenats tipus singleton)Safe Programming with Pointers through Stateful Views
{...} quantificador universal […] quantificador existencial {n:nat | n > 2} univers o domini (anomenat ''sort'') dels naturals majors que 2 {n:nat} int(n) tipus de sencer corresponent a l'univers de n {n:nat} int n notació equivalent a l'anterior
// per exemple a la funció abs: // ∀ n de l'univers dels sencers, ∃ r de l'univers dels naturals
fn abs {n:int} (num: int(n)): [r: nat] int(r) = if num >= 0 then num else ~num
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 val x : '(int, char) = '(15, 'c') // x.0 = 15; x.1 = 'c' val '(a, b) = x // lligam per encaix, a= 15, b='c' val x = '{primer=15, segon='c'} // x.primer = 15 val '{primer=a, segon=b} = x // lligam per encaix, a= 15, b='c' val '{segon=b, ...} = x // lligam per encaix amb omissió, b='c'
amb allotjament directe (anomenat flat) amb @ de prefix, obviable en la construcció @(a, b) = (a, b) però no en l'encaix de patrons. val x : @(int, char) = @(15, 'c') // x.0 = 15; x.1 = 'c' val @(a, b) = x // lligam per encaix, a= 15, b='c' val x = @{primer=15, segon='c'} // x.primer = 15 val @{primer=a, segon=b} = x // lligam per encaix, a= 15, b='c' val @{segon=b, ...} = x // lligam per encaix amb omissió, b='c'
especial val (prova_de_predicat | valor) = expressió // resultat de funcions que, acompanyen el valor amb l'avaluació d'un predicat
Diccionari sort univers o domini de valors sortdef nat = {a:int | a >= 0} // predefinit
type (com a domini) domini polimòrfic associat a tipus que ocupen exactament una paraula de màquina (llargada d'un punter). fun {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0) 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.
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)
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
viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l
sorts Univers o domini de valors
sortdef nat = {a:int | a >= 0} // predefinit al ''Prelude'' sortdef positius = {n:nat | n >= 1} sortdef positius_entre_deu_i_20 = {n:positius | n >= 10 && n <= 20}
ús en especificació de paràmetre:tipus {n:positius_entre_deu_i_20} num: int(n)
algebraics datasort alg_nats = Zero of () | Succ of alg_nats
datatypes a la ML datatype diaFeiner = Dl | Dt | Dm | Dj | Dv
llistes:
datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)
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: staload "foo.sats" // ''obre''/importa el mòdul foo.sats incorporant els identificadors a l'espai de noms actual
staload F "foo.sats" // requereix qualificador com ara $F.bar
dynload "foo.dats" // carrega el mòdul dinàmicament (en temps d'execució)
vectors Diverses construccions i proves
del manualManual val feiners = array0 $arrsz{string}("Dilluns", "Dimarts", "Dimecres", "Dijous", "Divendres")
de la web->Tutorial->Linear ArraysLinear 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 viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l
fun{a:viewt@ype} array_ptr_alloc {n:nat} (asz: int n):<fun> [l:addr | l <> null] (free_gc_v (a, n, l), array_v (a?, n, l) | ptr l) de la web->Tutorial->DataviewsATS-lang.org - Dataviews - vectors Una dataview (vista) és una proposició de lògica lineal que es fa servir per especificar relacions recursives en recursos d'estructura lineal.
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))
Referències
Enllaços externs Pàgina inicial del llenguatge ATS Manual 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++ Banc de proves de llenguatges com a reptes un contra un ATS per a programadors en llenguatge ML i altres articles Combining programming with theorem proving Combinant programació amb comprovació de teoremes.
Categoria:Llenguatge de programació ML Categoria:Llenguatges de programació funcional Categoria:Llenguatges de programació multiparadigma