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

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)

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

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

• 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

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

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

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