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.

Taula de continguts

Història [modifica]

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]

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

Un cas introductori [modifica]

proposicions [modifica]

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]

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]

Detalls comuns [modifica]

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]

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

Tuples i registres [modifica]

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]

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 linial 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]

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]

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]

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]

.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 de interfície com de implementació
.cats
fitxer amb continguts de codi C

Mòduls [modifica]

 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]

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 linial que es fa servir per especificar relacions recursives en recursos d'estructura linial.[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]

  1. ↑ ATS - anotacions de mètrica(anglès)
  2. ↑ Programant amb Prova de Teoremes(anglès)
  3. ↑ 3,0 3,1 DML (Dependent ML) i "De Caml"(anglès)
  4. ↑ Reddit.com - Language Shootout. ATS is the new top gunslinger. Beats C++(anglès) ATS és el nou millor tirador en el repte entre llenguatges. Guanya al C++ - Discussió sobre l'eficiència
  5. ↑ Compilació - Recollidor de memòria brossa
  6. ↑ Safe Programming with Pointers through Stateful Views(anglès)
  7. ↑ Manual(anglès)
  8. ↑ Linear Arrays(anglès)
  9. ↑ 9,0 9,1 ATS-lang.org - Dataviews - vectors(anglès)

Enllaços externs [modifica]

Vegeu aquesta plantilla
Llenguatges de programació
Ada  · ALGOL  · Assemblador  · ATS  · Awk  · Basic  · BCPL  · C  · C++  · C#  · Clean  · Clojure  · Cobol  · Cyclone  · D  · Delphi  · Frege  · Eiffel  · Erlang  · F#  · Forth  · Fortran  · Haskell  · Hume  · Java  · Javascript  · Lisp  · Logo  · MAGIC  · Mercury  · Miranda  · ML  · ML_Estàndard (SML)  · Modula-2  · Oberon  · Objective-C  · OCaml  · OpenCL  · Pascal  · PHP  · Perl  · Prolog  · Python  · Rexx  · Ruby  · Scala  · Smalltalk
Obtingut de «http://ca.wikipedia.org/w/index.php?title=ATS_(llenguatge_de_programació)&oldid=11403373»