tìpo di dati

in informatica, definizione delle caratteristiche degli insiemi di dati che costituiscono i domini da cui ricavare valori per le variabili di un programma. I tipi di dati utilizzati nei comuni linguaggi di programmazione uniscono alla definizione (anche implicita) del dominio dei possibili valori, la specifica delle operazioni in cui tali valori sono coinvolti. Inoltre, i documenti ufficiali di definizione dei linguaggi possono anche richiedere che la memorizzazione fisica dei valori nella memoria del computer abbia certe particolarità. Per esempio, le stringhe sono memorizzate in C come vettori di caratteri terminate con il codice ASCII "\0", mentre in Java come istanze di una classe String. Per poter ragionare sulle proprietà di un tipo di dati, per esempio sulla possibilità di utilizzare un dato di un sottotipo quando viene richiesto uno del tipo principale, è opportuno averne una definizione matematica, su cui eventualmente condurre dimostrazioni. A questo scopo è stata introdotta la nozione di tipo di dati astratto, che permette di definire le caratteristiche di un tipo indipendentemente dalle particolari strutture dati utilizzate per memorizzarne i valori, come pure dall'implementazione delle operazioni da condurre su di essi. Esistono vari modi per spiegare i tipi di dati astratti. In generale, un tipo di dati astratto fornirà la segnatura delle operazioni, indicando le cosiddette sorte, cioè i nomi associati ai domini astratti, dei dati in ingresso e quelle dei dati prodotti come risultato. Si descriverà quindi in termini formali, secondo qualche linguaggio di specifica (non necessariamente di programmazione), i vincoli a cui deve sottostare qualsiasi implementazione delle operazioni, per potere essere ritenuta corretta. Nel metodo delle specifiche algebriche, questi vincoli sono forniti da un insieme di equazioni, dette assiomi, che stabiliscono l'equivalenza fra i termini costruiti con le diverse operazioni. Per esempio il tipo di dati NAT sarà caratterizzato dall'uso della costante zero, e della sorta nat, delle operazioni succ, +, * e del predicato eq. Inoltre, utilizza la segnatura del tipo BOOL. Gli elementi di questo tipo di dati vengono quindi costruiti o come la costante zero (indicato con zero: → nat), o come successori di un altro elemento (succ: nat → nat). Le segnature delle operazioni + e * sono del tipo nat ×nat → nat, mentre eq è un predicato di tipo nat × nat → bool. Si hanno quindi i seguenti assiomi, che devono essere validi per ogni valore di x e y: zero+y = y; succ(x)+y = succ(x+y); zero * y = zero; succ(x)*y = y+(x*y); eq(zero, zero) = true; eq(zero, succ(y)) = false; eq(succ(y), zero) = false; eq(succ(x), succ(y)) = eq(x, y). Si osservi che NAT corrisponde alla definizione dell'insieme dei numeri naturali secondo gli assiomi di Peano, così da definire i vincoli cui una qualsiasi implementazione del tipo dei numeri naturali deve adeguarsi. Ulteriori assiomi possono essere utilizzati per richiedere esplicitamente la commutatività delle operazioni di somma e prodotto. Le definizioni dei tipi di dati astratti non comportano nessun vincolo sulle forme della memorizzazione dei suoi valori, purché esse siano adeguate a supportare l'implementazione degli assiomi. Negli approcci legati al paradigma di programmazione funzionale, la spiegazione dei tipi di dati è fornita in maniera ricorsiva, e ogni espressione riceve un tipo in base alle operazioni che essa contiene. Per esempio, il tipo Lista può essere definito stabilendo che un elemento di un qualsiasi tipo è utilizzato per formare una lista di un solo elemento, e che è possibile ottenere una lista concatenando un elemento a una già esistente. Il tipo Lista si può specializzare a contenere solo elementi di un certo tipo, per esempio per definire una ListaDiInteri. Nei linguaggi funzionali, come ML si possono inoltre compiere inferenze di tipo, in cui, noti i tipi dei componenti di un'espressione o di una funzione, è possibile ricavarne quello complessivo. Per esempio, data la definizione di funzione fattoriale, fact x : if x == 1 then 1 else x * fact(x-1), si può concludere che essa associa numeri interi a numeri interi. Infatti, i due rami, then ed else, producono entrambi valori interi. Per il ramo then, questo è immediato in quanto 1 è un valore intero per definizione. Per il ramo else si consideri che x-1 richiede che x sia un intero (per cui l'ingresso deve risultare intero). Inoltre x-1 produce come risultato un intero, e l'operazione di moltiplicazione ha come argomenti due numeri interi e un numero intero. I linguaggi di programmazione forniscono un insieme di tipi primitivi, tipi numerici e booleani, ma anche dei costrutti sintattici per definire nuovi tipi. Esempi sono la possibilità di definire array di valori, tutti dello stesso tipo, o di costruire record in Pascal, struct in C o classi (e sottoclassi di classi esistenti) nei linguaggi a oggetti. In tutti questi casi, un nuovo tipo risulta dalla composizione di quelli esistenti. Dalle relazioni fra i tipi definibili in un linguaggio di programmazione si viene quindi a costituire un sistema di tipi, basato sulle relazioni fondamentali di composizione, nel senso visto sopra, e di sottotipo. La relazione di sottotipo è tale per cui un valore di un tipo type2 che sia un sottotipo del tipo type1 può essere usato ogni volta che in un'espressione sia richiesto un valore di type1. Tale relazione è transitiva, cioè se type2 è sottotipo di type1, e type3 è sottotipo di type2, allora anche type3 è sottotipo di type1. Nella maggior parte dei linguaggi di programmazione correnti, il sistema di tipi non è associato a regole di inferenza, così che il tipo delle variabili e delle funzioni deve essere assegnato staticamente, e il compilatore o l'interprete del linguaggio possono solo verificare la coerenza della definizione con l'uso della variabile o funzione nelle istruzioni in cui essa compare. Questo controllo viene effettuato dai compilatori nella fase di analisi semantica. In alcuni casi, il linguaggio si basa su un unico tipo di base, quale la classe Object in small talk, o il tipo lista in LISP. In small talk, la definizione di una nuova classe risulta in definitiva dalla specializzazione del tipo Object o di un suo sottotipo, cioè la dichiarazione di una classe definisce le caratteristiche strutturali e comportamentali delle sue istanze. In LISP, l'interpretazione del contenuto di una lista può dare origine sia a funzioni sia a valori. Linguaggi di questo genere hanno capacità riflessive, permettendo cioè di rappresentare le caratteristiche del linguaggio stesso al loro interno.