Introduzione ai Tipi

Una definizione plausibile di sistema di tipi in informatica è:

Un metodo sintattico praticabile per dimostrare
l'assenza di determinati comportamenti del
programma, fatto classificando le unità sintattiche in
base ai tipi di valore che assumono.

Type-checking

Il vantaggio più famoso dei tipi è il type-checking, cioè la possibilità di usare i tipi per rilevare errori di programmazione.

Il type-checking e' una specie di dim di un teorema. Prende le dichiarazioni dei tipi come def di teoremi o regole su quello che succede nel programma. Controllando ogni passaggio del programma (staticamente) se non ho errori la prova ha avuto successo, altrimenti errore.

Safety

la “safety” si riferisce alla capacità di un linguaggio di garantire l'integrità delle sue astrazioni (ovvero effettua i controlli sulle sue astrazioni). I linguaggi “safe” sono anche detti a tipizzazione forte o strongly typed (e quelli non sicuri a tipizzazione debole o weakly typed).

Un ling strongly typed significa che le astrazioni sono garantite da linguaggio Il c e' weakly typed es. negli array posso accedere a pos che non fanno parte degli array (es accedo alla pos 5 di un array di 4 elem) In java (strongly typed) ha controllo su enum e controllo su array (out of bound exception) typescript e' strongly typed Un ling strongly typed ti impedisce di fare cose, uno weakly typed no (meno)

I tipi possono contribuire a migliorare l'efficienza dei programmi. Nei linguaggi safe, i tipi aiutano a migliorare l'efficienza eliminando molti dei controlli dinamici per garantire la sicurezza. I moderni compilatori ad alte prestazioni si basano molto sulle informazioni raccolte dal type-checker per ottimizzare la generazione del codice.

Nota: in java un bool occupa 2 byte (colpa della jvm)

Dynamic vs Static Typing

Un ling e' tipato staticamente se possiamo controllare i tipi sul testo del programma, senza doverlo eseguire (es. in fase di compilazione). Il compilatore puo' eliminare le annotazioni di tipo (e i relativi controlli) dal codice generato (perche' tanto sono giusti e quindi non devono essere controllati a runtime).

Si parla di linguaggi tipati dinamicamente quando il controllo dei tipi avviene durante l'esecuzione del programma. In particolare, il controllo dinamico dei tipi richiede che ogni valore abbia un descrittore di esecuzione che ne specifichi il tipo e che, a ogni operazione, il runtime verifichi che il programma esegua operazioni solo su operandi del tipo corretto.

Manifest vs Inferred typing

La tipizzazione statica o dinamica riguarda il momento in cui un ling (interpretato o compilato) esegue il controllo dei tipi. Il tipaggio manifesto o inferito determina la quantita' di informazioni sui tipi che il programma deve inserire nei suoi programmi. Un linguaggio con manifest typing richiede che il programma annoti tutti i tipi di variabili e operazioni. Un linguaggio con inferred typing non ha bisogno di annotazioni, in quanto dispone di algoritmi che deducono i tipi dal contesto.

Il tipaggio manifesto e inferito sono uno spettro determinato da fattori ergonomici e algoritmici. Ad esempio,leggendo il programma x=5 noi (come programmatori) possiamo dedurre che il tipo di x potrebbe essere intero. il bilanciamento tra tipi manifesti e tipi inferiti non è una decisione netta e riguarda il bilanciamento tra supporto/impegno che un linguaggio offre/richiede ai programmatori.

Dynamic vs Static Typing

I linguaggi a tipaggio dinamico non sono per forza interpretati. Quindi, la richiesta di scegliere tra un linguaggio a tipaggio dinamico e uno a tipaggio statico non riguarda la quantità di informazioni che i programmatori devono fornire sui tipi (manifesti o inferiti) o se i programmi sono interpretati o compilati (implementazione). Invece, i fattori principali che possono orientare la scelta tra i due approcci sono la correttezza, le prestazioni e l'espressività del programma.

Il tipaggio statico significa trovare gli errori prima di eseguire il programma. Questo elimina la necessità di annotare i termini e di eseguire controlli a tempo di esecuzione e permette alcune ottimizzazioni, aumentando le prestazioni. Tuttavia, i linguaggi a tipaggio statico hanno un “difetto” comune: a seconda dell'espressività dei tipi e dell'accuratezza dell'algoritmo di type-checking, possono rifiutare programmi che verrebbero eseguiti correttamente (ad esempio, il codice sulla destra). Ciò è dovuto all'indecidibilità dei programmi (terminazione), che rende impossibile sapere quali rami verranno eseguiti o meno e costringe il type- checking a considerare tutti i possibili stati di calcolo.

int x
if(e) x=“A”
else x = 5

se e e' falsa, questo codice verrebbe eseguito correttamente ma il controllo statico boccia questa implementazione.