ATS (llenguatge de programació)

ATS

Tipus	llenguatge de programació declaratiu, llenguatge de programació funcional, dependently typed programming language (en) i llenguatge de programació
Paradigma de programació	Programació declarativa i programació funcional
Influenciat per	Dependent ML (en) , ML, OCaml i C++
Llicència	GNU GPL 3.0
Pàgina web	ats-lang.org

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^[1] i un sistema de proposicions i proves (predicats).^[2]

El llenguatge parteix del cos del llenguatge ML Estàndard incorporant-hi construccions per a proveir els mecanismes avançats.

ATS deriva d'una versió anterior anomenada DML ó Dependent ML^[3]

També hi ha antecedents en el "De Caml" versió de Caml Light amb "tipus dependents de valors" del mateix autor.^[3]

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ó.^{[cal citació]}

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))  

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.[0]))  else let  val num = int1_of argv.[1]  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^[4]

atscc fact1.dats -o fact1 ./fact1 4 

dona el resultat esperat

factorial de 4 = 24 

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

 {...} 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 

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

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 

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 

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 

datatype diaFeiner = Dl | Dt | Dm | Dj | Dv 

llistes:

datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a) 

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

.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

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ó) 

Diverses construccions i proves

• del manual^[6]

val feiners = array0 $arrsz{string}("Dilluns", "Dimarts", "Dimecres", "Dijous", "Divendres")  

• de la web->Tutorial->Linear Arrays^[7]
• : @[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->Dataviews^[8]

Una dataview (vista) és una proposició de lògica lineal que es fa servir per especificar relacions recursives en recursos d'estructura lineal.^[8]

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)) 

• 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