Nonostante il refrain “Java è un linguaggio morto” sia di moda anche nel 2020, nelle ultime versioni di Java, rilasciate attualmente al ritmo di una ogni sei mesi, sono comparse delle features interessanti. Ne abbiamo accennato nei precedenti post, qui e qui, relativamente a JDK 14.

Ma le novità non si fermano qui: nella JSR 390, la cui implementazione di riferimento sarà la JDK 15, è prevista l’implementazione della JEP 360 relativa ai sealed type, vale a dire a classi o interfacce che possono essere estese, ma solo da un insieme limitato e dichiarato di classi o interfacce.

In questo modo sarà raggiunto un grande obiettivo.

L’obiettivo consiste nel restringere le classi/interfacce che possono estendere una data classe/interfaccia, offrendo quindi una estensione – nonostante si tratti di una limitazione nella gerarchia di classi – del design Object Oriented: si può dire che un oggetto che implementa una interfaccia X è A oppure B ma non può essere altro. E chi usa una libreria saprà che l’oggetto che implementa X è A o B; e anche che chi progetta una libreria sa che nessuno potrà estendere le eventuali sealed classes che ha disegnato. Il fatto che si possa esprimere che un oggetto appartenga ad una classe A oppure ad una classe B ci riconduce alla teoria dei tipi e, in questo caso in particolare, ai disjoint union types.

Ma cosa è la teoria dei tipi?

Una teoria che consente di definire i fondamenti della matematica e che è alternativa alla teoria degli insiemi e alla logica.

In questa teoria, la classica relazione della teoria degli insiemi “a ∈ A” (a appartiene all’insieme A) è sostituita dalla relazione a:A, vale a dire a ha il tipo A.

Se A e B sono tipi, sono tipi anche

AxB: prodotto di tipi

A u B: Unione di tipi

A -> B, tipo funzione

T e F, tipi costanti

E’ stata introdotta da Bertrand Russel ai primi del 1900 come risposta alla contraddizione che lo stesso Russel aveva individuato nella teoria degli insiemi di Cantor. Di che natura era questa contraddizione?

Il teorema di Cantor dice che dato un insieme di N oggetti, l’insieme di tutti i sottoinsiemi ha cardinalità 2^N

Ma possiamo considerare gli insiemi – detti normali – che non sono membri di sé stessi. Ad esempio l’insieme di tutte le tazze da thè, che non è una tazza da thè. (Gli insiemi che sono membri di sé stessi sono chiamati anormali).

L’insieme R di tutti gli insiemi normali, appartiene a sé stesso? In caso affermativo, dovrebbe soddisfare la condizione per cui dovrebbe appartenere all’insieme di tutti gli insiemi che non sono membri di sé stessi e quindi non lo è; in caso negativo, se non appartenesse a sé stesso, dovrebbe soddisfare la condizione per cui dovrebbe essere membro si sé stesso. Da qui la contraddizione.

Per superare tale contraddizione, che ha il suo fondamento nella natura estensionale e semantica della teoria degli insiemi, Russel elabora la teoria dei tipi come formalismo che ha natura sintattica e intensionale.

Ma cosa vuol dire che la teoria degli insiemi ha natura estensionale e semantica e la teoria dei tipi ha natura intensionale e sintattica?

In breve, gli insiemi sono collezioni di oggetti e l’appartenenza ad un insieme è definita mediante una funzione caratteristica, e quindi può essere indecidibile. La teoria dei tipi, invece, ha una forma sintattica perché è improntata a come gli elementi sono costruiti.

Alla prossima per un approfondimento.