Problemi nel sistema tipo di Haskell

Question

Ive incontra alcune risposte (qui in SO) che affermano che Haskell ha molti "angoli bui" nel suo sistema di tipi e anche alcuni buchi disordinati. Qualcuno potrebbe elaborare su questo?

Grazie in anticipo

Answer 1

Credo che dovrei rispondere a questa, soprattutto perché due persone finora hanno mal interpretato le mie osservazioni ...

Per quanto riguarda la non-terminazione, l'osservazione in questione era leggera iperbole per effetto drammatico, e di cui non terminazione al livello valore. Questo è stato nel contesto del confronto tra Haskell e teoremi dimostratori, in una risposta a qualcuno che ha menzionato le proprietà di correttezza di tipo come qualcosa che ha particolarmente apprezzato. In questo senso, la presenza di ⊥ che abita tipi altrimenti vuoti è un "difetto", perché cambia il significato di un tipo come A -> B da "dato un A, produce un B" in "dato un A, o produce un B o si blocca il programma "che è, per ovvi motivi, un po 'meno soddisfacente dal punto di vista della prova di correttezza.

È anche completamente irrilevante per quasi tutta la programmazione quotidiana e non peggio di qualsiasi altro linguaggio generico poiché, naturalmente, per la completezza di Turing è richiesta la possibilità di non terminare.

Non ho alcun problema con UndecidableInstances. In realtà, mi infastidisce meno di ⊥ a livello di valore, perché si blocca solo GHC durante la compilazione, non il programma finito. OverlappingInstances è un'altra questione, però, e il guazzabuglio ad hoc delle estensioni di GHC per fornire piccole parti di cose che richiederebbero naturalmente dei tipi dipendenti certamente si qualifica come "disordinato".

Ma tieni presente che la maggior parte delle cose di cui mi lamento in Haskell sono solo un problema a causa delle fondamenta altrimenti molto solide. La maggior parte dei sistemi di tipi in altri linguaggi tipizzati staticamente non sono nemmeno abbastanza coerenti da essere chiamati "sbagliati" in confronto, e ripulire il materiale che sto chiamando "disordinato" è un'area di ricerca attiva e continua.

Answer 2

Quindi ti riferisci Camccann dicendo "Sistema tipo di Haskell è pieno di buchi, a causa di nontermination e altri compromessi disordinato"? Penso che stia parlando dell'estensione UndecidableInstances e probabilmente di altre.

Poi hai fatto riferimento a Norman, posso solo supporre, dicendo "Il sistema di tipo di Haskell è ambizioso e potente, ma viene continuamente migliorato, il che significa che c'è una certa incoerenza come risultato della storia.". Sono sicuro che avesse in mente qualcosa, ma gli permetterà di chiarire quando vedrà questa domanda.

Answer 3

Il sistema di tipo Haskell non presenta problemi o buchi disordinati. Haskell 98 può essere completamente dedotto dal tipo. Possiede quella che è conosciuta come la proprietà del "tipo principale", vale a dire che ogni espressione data ha al massimo un singolo tipo più generale. Ci sono, tuttavia, una serie di espressioni che sono buone, utili e valide ma che non si digita in Haskell 98. La maggior parte di questi sono tipi di alto livello. forall a b. (a -> b) -> a -> b è un esempio (poco interessante) di tipo rank-one, il che significa che lo forall è solo all'esterno. forall b. -> (forall a. a -> a) -> b -> b è un esempio di tipo inutile ma possibile che non è di primo grado e non può essere espresso in Haskell98. I tipi di classificazione più alti sono una delle molte cose che infrangono la proprietà del tipo principale.

Come si aggiungono sempre più estensioni al sistema Haskell98 di base, cominciano a esserci dei compromessi tra la capacità di scrivere tipi veramente potenti che esprimono sia i diversi tipi di polimorfismo che i diversi tipi di vincoli e la capacità di avere tanto codice il più possibile completamente desunto dal tipo. Ai margini di ciò che è possibile, i tipi possono diventare complicati e, occasionalmente, è possibile imbattersi in cose che sembrano funzionare, ma non farlo. Ma a quel punto, si sta generalmente facendo ciò che è noto come "programmazione a livello di testo", in cui gran parte della logica dell'applicazione è stata incorporata nei tipi stessi e attraverso una combinazione di trucchi per la classe di tipizzazione in cui è stato inserito il compilatore, essenzialmente, eseguendo i tipi come programma in fase di compilazione.

Non sono d'accordo, tra l'altro, con l'affermazione di Camccann che la potenziale non-conclusione è un compromesso disordinato nel controllo del testo. Penso che sia una funzionalità perfettamente utile, in effetti un prerequisito per la tornitura-completezza a livello di tipo, e si rischia solo se si chiede esplicitamente al compilatore di iniziare a consentire molte cose oscure.