ATS (llenguatge de programació)

De Viquipèdia
Dreceres ràpides: navegació, cerca

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 proveïr els mecanismes avançats.

Història[modifica | modifica el codi]

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]

Eficiència[modifica | modifica el codi]

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ó.[4]

Un cas introductori[modifica | modifica el codi]

proposicions[modifica | modifica el codi]

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ó[modifica | modifica el codi]

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

atscc fact1.dats -o fact1
./fact1 4

dóna el resultat esperat

factorial de 4 = 24

Característiques[modifica | modifica el codi]

Detalls comuns[modifica | modifica el codi]

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

 {...} 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[modifica | modifica el codi]

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

Tuples i registres[modifica | modifica el codi]

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[modifica | modifica el codi]

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[modifica | modifica el codi]

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[modifica | modifica el codi]

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 + -)[modifica | modifica el codi]

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[modifica | modifica el codi]

.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[modifica | modifica el codi]

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[modifica | modifica el codi]

Diverses construccions i proves

  • del manual[7]
val feiners = array0 $arrsz{string}( "Dilluns", "Dimarts", "Dimecres", "Dijous", "Divendres") 
  • de la web->Tutorial->Linear Arrays[8]
    @[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[9]

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

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[modifica | modifica el codi]

Enllaços externs[modifica | modifica el codi]