Molte persone che non sono pratiche di studi matematici
ritengono che per il solo fatto che la macchina analitica
di Babbage fornisce i suoi risultati in notazione numerica,
la natura dei suoi processi deve conseguentemente essere
aritmetica e numerica piuttosto che algebrica ed analitica.
Questo è un errore. Questa macchina può combinare le
sue quantità numeriche esattamente come se fossero
lettere o qualsiasi altro simbolo in generale; ed infatti
essa potrebbe benissimo restituire i suoi risultati in notazione
algebrica se le fosse chiesto di farlo.
Lady Ada Augusta, Contessa di Lovelace (1844)
Nel 1954 John Backus inizia un progetto che lo porterà all’ideazione del FORTRAN: il primo vero e proprio linguaggio di programmazione imperativo ad alto livello. Già però all’inizio degli anni ’70 Backus si era accorto delle limitazioni del paradigma di programmazione imperativa. Sempre in quegli anni stava iniziando a prendere forma la teoria della programmazione ad oggetti, teoria che dalla metà degli anni ’90 avrebbe abbagliato milioni di programmatori che l’hanno accettata come la vera soluzione alla famosa “crisi del software” e che invece ha contribuito ancora di più a spostare l’attenzione dal vero problema che Backus aveva intravisto nel 1970. Nel 1977 John Backus ricevette il prestigioso ACM Turing Award principalmente per lo sviluppo del FORTRAN e come lettura durante la premiazione portò quella che a mio avviso è una delle sue pubblicazioni più illuminanti. Questo articoletto di appena 22 pagine si intitola: “Can programming be liberated from the von Neumann style?”. Il titolo già fa intuire la portata di questo scritto. Ma cosa intende Backus quando parla di “Stile di von Neumann”?
Dalla costruzione del primo computer che implementa la cosiddetta architettura di von Neumann, i programmi hanno ereditato il primitivo stile “a-word-at-time”. Questa architettura lega in maniera molto stretta la semantica del linguaggio alle transizioni di stato della macchina fisica, privando di fatto la programmazione della necessaria abilità di ragionamento matematico. Oggi programmare vuol dire passare la maggior parte del tempo a cambiare valore alle variabili cambiando continuamente lo stato del sistema complessivo. Ma la programmazione, in origine, non era questo, almeno non quella che avevano in mente persone come Backus, McCarthy, Naur o Hoare. In origine c’era il ragionamento matematico algoritmico alla base di tutto. Poi è arrivato il ponte, l’anello di congiunzione tra matematica (teoria delle dimostrazioni) e la Computer Science. Questo anello di congiunzione è l’isomorfismo di Curry-Howard. Tecnicamente questo isomorfismo si basa su tre osservazioni avvenute in periodi storici diversi da parte del logico Haskell Curry e dal matematico William Howard. La prima osservazione del 1938 è di Curry e afferma che i “tipi” dei combinatori possono essere visti come “schemi di assiomi” della logica intuizionistica. La seconda osservazione, sempre di Curry è del 1958 ed afferma che un certo tipo di sistema di dimostrazione chiamato “sistema di deduzione alla Hilbert”, coincide in alcune sue parti con alcuni frammenti del modello standard di calcolo conosciuto come “Logica Combinatoria”. La terza osservazione è di Howard ed è del 1969. Questa afferma che il sistema di dimostrazione ad alto livello conosciuto come “Sistema di deduzione naturale” può essere direttamente interpretato nella sua versione intuizionistica come una variante tipizzata del modello computazionale noto come “Calcolo-Lambda”.
Ed ecco il collegamento!!! In parole povere, tramite l’isomorfismo di Curry-Howard, noi possiamo interpretare un’espressione del tipo
p :: P sia come “
p è la dimostrazione di
P”, sia nella sua versione equivalente: “
p e di tipo
P”. Per una descrizione dettagliata di questo isomorfismo rimando chi è interessato alla lettura di libri ed articoli riguardanti la teoria dei tipi come ad esempio l’ottimo scritto del 1999 di Simon Thompson intitolato: “Type Theory & Functional Programming”.
Questo isomorfismo è di importanza estrema, di pari grandezza (a mio avviso) del principio di equivalenza di Einstein in Fisica.
La programmazione che si basa su queste idee si dice “Funzionale” e ha poco a che fare con il cambiare valore alle variabili e quindi modificare in continuazione lo stato del “mondo” fisico della macchina. Nella programmazione funzionale si ha invece a che fare con l’applicazione di funzioni a delle variabili. Qui il termine “funzioni” ed il termine “variabili” non va pensato in un contesto informatico, ma va collocato in un contesto matematico, quando si parla di funzione in programmazione funzionale ci si riferisce ad una vera e propria funzione matematica con il suo dominio ed il suo codominio. La dichiarazione di una funzione in un linguaggio funzionale è una vera e propria equazione dimensionale, un teorema con la sua dimostrazione. Ad esempio noi possiamo definire una funzione che somma fra di loro gli elementi di una lista nel seguente modo:
sum :: Num a => [a] -> a Questa ci dice che esiste un morfismo
sum che lega il dominio formato da liste di oggetti
a che sono numeri ed il codominio formato da oggetti
a.
In maniera equivalente (tramite l’isomorfismo di Curry-Howard) possiamo interpretare l’espressione qui sopra dicendo che
sum è una funzione che accetta come argomento una lista di oggetti
a di tipo numerico e restituisce come risultato un oggetto numerico di tipo
a.
Infatti in un linguaggio funzionale puro come Haskell la funzione
sum può essere scritta nel seguente modo:
sum :: Num a => [a] -> a
sum [] = 0
sum (x:xs) = x + sum xsNon sto qui a spiegare la sintassi di queste linee di codice, ma voglio solo far notare che nessuna variabile viene in qualche modo creata o modificata e che quindi la “purezza” di un linguaggio come Haskell preserva il sistema da qualsiasi tipo di cambiamento di stato.
Qui si ragiona in termini di teoremi e di dimostrazioni, di funzioni intese come equazioni e non come una sequenza di “statements” della forma “do-this-then-this-then-this…” come avviene nei linguaggi imperativi. Come afferma Philip Greenspun, i linguaggi funzionali sono quei linguaggi nei quali si passa molto più tempo a pensare che a digitare.
Questo è quello che aveva intuito Backus più di quarant’anni fa. La programmazione deve spingere il programmatore verso il ragionamento astratto per il quale, per sua natura è molto più portato, piuttosto che imprigionarlo in una fisicità che non gli appartiene. Che ci importa se una variabile viene immagazzinata in 0x73FBB piuttosto che in 0x73FBA. Non ci deve importare! Quello che ci deve importare è che se io penso ad una funzione
f :: X -> Y questa deve essere valida sia che io la esegua su un supercomputer massivamente parallelo, sia che la esegua sul pallottoliere che usavo alle elemetari.
John Backus è morto il 17 Marzo del 2007 senza vedere il cambiamento di rotta nell’Informatica che aveva auspicato per tutta la sua vita. Solo oggi si inizia a vedere qualche segnale. I linguaggi del cosiddetto “mainstream” industriale ormai hanno raggiunto un livello tale di mastodonticità e complicazione che alcuni ricercatori stanno veramente vagliando l’ipotesi di un cambiamento di direzione (anche se molto lento e graduale. Ricordiamoci che un linguaggio di programmazione deve far parte dello spazio delle soluzioni di un problema e non diventare parte del problema stesso).
Ad esempio un linguaggio imperativo come il C# che oggi va tanto di moda, fino alla versione 2.0 non aggiungeva niente di innovativo alla marea di linguaggi imperativi preesistenti se non qualche abbellimento sintattico e qualche scorciatoia di libreria, ma dalla versione 3.0 in poi ha iniziato ad orientarsi verso una impostazione sempre più funzionale (ad esempio incorporando l’estensione LinQ), e molti altri linguaggi si stanno orientando verso la stessa direzione. Che stia veramente cambiando qualcosa? Vedremo, ma mai come in questo caso un ritorno alle origini è gradito. Chiudo ricordando quello che diceva Hoare a proposito dell’Algol 60 e cioè che era un linguaggio molto più avanzato di tutti i suoi predecessori, ma anche di molti dei suoi successori.
