Wikipedia

Teoria dei tipi: differenze tra le versioni

Naviga nella cronologia in modo interattivo
← Differenza precedente
Contenuto cancellato Contenuto aggiunto
VisualeWikitesto
Alexbot (discussione | contributi)
111 532 modifiche
m Bot: Aggiungo: nl:Typentheorie
m →Altri progetti: Aggiunto il parametro "Preposizione" nel template "Interprogetto"
 
(21 versioni intermedie di 16 utenti non mostrate)
Riga 1:
{{F|teorie dell'informatica|maggio 2014}}
Dal punto di vista più generale, la '''teoria dei tipi''' è la branca della [[matematica]] e della [[logica]] che si occupa di classificare generiche ''entità'', raggruppandole in collezioni chiamate ''tipi''. Sotto questo punto di vista vi sono punti di contatto con la [[Tipo (metafisica)|nozione di tipo della metafisica]]. La moderna formulazione della teoria dei tipi è, in parte, nata dal tentativo di dare una risposta al cosiddetto [[Paradosso di Russell]], ed è estesamente trattata nei ''[[Principia Mathematica]]'' di [[Bertrand Russell|Russell]] e [[Alfred North Whitehead|Whitehead]].
 
==Descrizione==
Con la diffusione di [[computer]] sempre più potenti, e l'introduzione di [[Linguaggio di programmazione|linguaggi di programmazione]] per lo sviluppo di [[Programma (informatica)|programmi]] da installare su di essi, la teoria dei tipi ha trovato un significativo campo di applicazione, soprattutto nell'ambito della progettazione degli stessi linguaggi di programmazione. In questo contesto, esistono diverse definizioni applicabili ada un ''[[sistema didei tipi]]'', ma la seguente, dovuta a [[Benjamin C. Pierce]] è probabilmente quella che raccoglie il maggiore consenso:
 
:''"Un sistema di tipi è un metodo sintattico modificabile[[Teoria della complessità computazionale|trattabile]], in grado di dimostrare l'assenza di determinati comportamenti nei programmi mediante la classificazione di espressioni fatta in base alla natura dei valori sottopostiche adesse elaborazioneelaborano."''<br>
::(''Types and Programming Languages'', MIT Press, [[2002]])
 
In altre parole, un sistema di tipi divide i valori manipolati dai programmi in ''insiemi'' chiamati ''tipi'' - eseguendo un'operazione chiamata ''assegnazione del tipo'' o ''tipizzazione'' - e fa sì che certi determinati comportamenti del programma siano, o non siano, possibili in base al tipo dei valori coinvolti in questi comportamenti.
 
Per esempio, supponiamo che un sistema di tipi classifichi il valore <code>ciao</code> come [[stringa (informatica)|stringa]] ede il valore <code>5</code> come [[intero]] e, sulla base di tali diverse assegnazioni, ''proibisca'' al programmatore di [[Addizione|sommare]] <code>ciao</code> a <code>5</code>. All'interno di questo sistema, sarebbe "illegale" l'istruzione di programma:
 
:<code>ciao</code> + <code>5</code>
 
sarebbe ''illegale''. Il vantaggio di questa ''"proibizione''", ovvero dell'impossibilità di far eseguire al programma questa operazione, consiste nel fatto che non potrà mai capitare di sommare stringhe a numeri, operazione che produrrebbe risultati privi di senso.
 
La progettazione e l'implementazione di un sistema di tipi è un argomento vasto e complesso, quasi come lo stesso linguaggio di programmazione che lo utilizza. Gli ideatori e gli studiosi dei sistemi di tipi si spingono ad effermareaffermare che si tratta dell'essenza stessa del linguaggio:<br>
:''"{{Citazione|{{Senza fonte|Progettate correttamente il sistema dei tipi e vedrete che il linguaggio si progetterà da sèsé!"''}}}}
È importante notare che la trattazione fin qui fatta si riferisce ai [[Tipo statico|tipi statici]]:. I sistemi di tipi ed i linguaggi che fanno uso di [[Tipo dinamico|tipi dinamici]] non sono in grado di verificare a priori che un programma faccia un uso corretto dei valori, e quindi generano un [[Eccezione (informatica)|errore]] ogni volta che il programma si comporta in modo da farne un uso scorretto. Per questa ragione, {{Senza fonte|secondo alcuni}}, la definizione "tipo dinamico" è intrinsecamente poco appropriata. Comunque, in molti linguaggi [[Linguaggio orientato agli oggetti|orientati agli oggetti]] che fanno uso di tipi dinamici, un tipo è qualcosa di più di un '[[Interfaccia (informatica)|interfaccia]] e, finché le classi condividono interfacce, non è necessario preoccuparsi di sapere a quale classe appartiene un dato oggetto.▼
 
▲È importante notare che la trattazione fin qui fatta si riferisce ai [[Tipo statico|tipi statici]]: I sistemi di tipi ed i linguaggi che fanno uso di [[Tipo dinamico|tipi dinamici]] non sono in grado di verificare a priori che un programma faccia un uso corretto dei valori, e quindi generano un [[Eccezione (informatica)|errore]] ogni volta che il programma si comporta in modo da farne un uso scorretto. Per questa ragione, secondo alcuni, la definizione "tipo dinamico" è intrinsecamente poco appropriata. Comunque, in molti linguaggi [[Linguaggio orientato agli oggetti|orientati agli oggetti]] che fanno uso di tipi dinamici, un tipo è qualcosa di più di un [[Interfaccia (informatica)|interfaccia]] e, finché le classi condividono interfacce, non è necessario preoccuparsi di sapere a quale classe appartiene un dato oggetto.
 
==Voci correlate==
* [[Paradosso di Russell]]
* [[Principia Mathematica]]
* [[Sistema dei tipi]]
* [[Teoria dei linguaggi di programmazione]]
*[[Teoria dei tipi intuizionista]]
 
==Altri progetti==
{{interprogetto|preposizione=sulla}}
 
==Collegamenti esterni==
* {{Collegamenti esterni}}
* {{en}}cita [web|http://www.nist.gov/dads/HTML/abstractDataType.html |Tipi di dati astratti]|lingua=en}}
 
[[Categoria:Logica {{Portale|filosofia|informatica|matematica]]}}
 
[[Categoria:Teoria dei tipi| ]]
[[ar:نظرية النمط]]
[[de:Typentheorie]]
[[en:Type theory]]
[[eo:Teorio de tipoj]]
[[fa:نظریه نوع‌ها]]
[[fr:Théorie des types]]
[[he:טיפוס (לוגיקה מתמטית)]]
[[ja:型理論]]
[[nl:Typentheorie]]
[[pt:Teoria dos tipos]]
[[ru:Теория типов]]
[[zh:类型论]]
Estratto da "https://it.wikipedia.org/wiki/Teoria_dei_tipi"