Perché C # non è tipizzato staticamente ma F # e Haskell lo sono?

Sto affrontando la sovrapposizione tra Haskell e I sistemi di tipo F #. La parte che condividono è un sottoinsieme semplificato di un sistema noto a volte come System F. F # fornisce necessariamente bit e parti del sistema di tipo C #, ma questo non è ciò di cui parlava l'oratore.

Sia C # che Haskell / F # sono tipizzati staticamente, ma sono due gusti diversi.

Sottotipizzazione

In particolare, C # è una lingua tipizzata staticamente con sottotipizzazione . Ciò significa che se guardi le regole di digitazione per C # ce n'è una come

 Env |- x : T, T' <: T
 ---------------------
     Env |- x : T'

Ciò significa che ogni termine ben scritto ha più di un tipo potenziale. Questo non è il caso in (vaniglia) Haskell o F #. Ogni tipo ha un singolo tipo più generale, un tipo principale. Questo ha alcuni vantaggi come l'inferenza del tipo totale.

Espressioni ovunque

Oltre a questo, Haskell e F # hanno una maggiore enfasi sulle espressioni, le espressioni hanno tipi, ma le affermazioni no. Ciò significa che in C #, il compilatore sta controllando meno del tuo codice, perché meno del tuo codice ha tipi. In Haskell, tutto ha un tipo reale, controllabile.

In termini sostanziali, ogni singolo nodo su Haskell AST ha un tipo o tipo (o specie). Lo stesso non si può dire di un C #.

Tipi di somma

Oltre a questo, Haskell e F # hanno i tipi di sum .

data Bool = True | False

Ecco come viene definito un booleano in Haskell. Ciò fornisce alcune garanzie diverse rispetto a C #. Ad esempio, quando c'è un numero discreto di cose in C #, come dire, un AST. Possiamo modellarlo con una gerarchia ereditaria, ma questi sono aperti. Chiunque può venire e aggiungere qualcosa ad esso. Possiamo utilizzare Enum , ma non esiste un modo corretto per allegare i dati a ciascun tag in modo uniforme. Questo è ciò che viene chiamato unione taggata, e spetta a te implementarlo / usarlo correttamente, il compilatore non ti aiuterà.

Ciò rende molto difficile assicurare che abbiamo coperto tutti i possibili nodi di un AST. Ad esempio, supponi di avere una funzione

doStuff :: AST -> AST
doStuff (SomeExpr ..) = ...
doStuff (SomeStatement ..) = ...
--// doStuff (SomeIf ...) = Oh noes, we forgot a node

Il compilatore può avvisarti perché può dimostrare esattamente quanti nodi ci siano, in assoluto. In C #, l'equivalente dovrebbe essere fatto con downcasting, e quindi, poiché l'insieme di nodi nella nostra gerarchia è aperto, non c'è modo di emettere avvisi di compilazione in tempo.

Una società, Jane Street, è entusiasta dell'utilità di questa funzione nella loro codifica OCaml large . Guarda alcuni dei loro talk , ci parlano un po 'di come l'uso di OCaml li impatta nel mondo reale.

Soapbox

Ora ho delineato alcune differenze rispetto al sistema F su molti sistemi di tipo mainstream, ma sono tutti sistemi di tipo statico. Mi dà fastidio quando le persone chiamano Java / C # / C ++ "non sono tipizzate staticamente". E sicuramente ti danno più garanzie di tempo per compilare che dire, Python. Quindi è un po 'ingiusto respingerli nel modo giusto.

C'è molta "religione di marketing" e pochissime conoscenze qui.

Un laguage static_typed deve supportare la definizione dei tipi e il controllo del tipo in fase di compilazione e un linguaggio dinamico tipizzato deve supportare la modifica del tipo di variabile in fase di runtime.

Le due cose non sono necessariamente mutuamente esclusive: un linguaggio può supportare entrambi i paradigmi:

l'unica cosa importante è che ciò che viene definito come statico non può diventare silenzioso dinamico .

Leggermente parafrasato e abbreviato:

What I don't mean by static typing: C#. What I do mean: F#. Now with an actual solid definition …

Questa non è una definizione, per non dire una solida. Penso che la risposta al perché C # non sia tipizzata staticamente, ma F # è, è: Perché l'autore del discorso lo ha detto.

Una "definizione" del genere è completamente inutile, non dice assolutamente nulla. Ed è impossibile raggiungere conclusioni basate su questo.

Dopo aver visto il discorso: sembra fondamentalmente un elogio del sistema di tipi di Haskell.

Alcuni punti non si applicano alle lingue che presumibilmente hanno una digitazione statica (non è possibile implementare facilmente STM in F #, perché non è puro). Alcuni dei punti si applicano alle lingue che "non hanno" la tipizzazione statica (non devi preoccuparti di null molto nel moderno C ++, puoi scrivere% sicure per tipo% in C #).