Haskell robusto senza errori

Question

Attualmente sto imparando Haskell. Una delle motivazioni per cui ho scelto questo linguaggio è stata quella di scrivere software con un grado molto alto di robustezza, cioè funzioni completamente definite, matematicamente deterministiche e mai in crash o che producono errori. Non intendo il fallimento causato dai predicati del sistema ("sistema esaurito", "computer acceso" ecc.), Quelli non sono interessanti e possono semplicemente bloccare l'intero processo. Inoltre, non intendo comportamenti errati causati da dichiarazioni non valide (pi = 4).

Invece mi riferisco ad errori causati da stati errati che voglio rimuovere rendendo quegli stati non rappresentabili e non compilabili (in alcune funzioni) tramite una tipizzazione statica rigorosa. Nella mia mente ho chiamato queste funzioni "pure" e ho capito che il sistema di tipo forte mi avrebbe permesso di realizzare questo. Tuttavia Haskell non definisce "puro" in questo modo e consente ai programmi di bloccarsi tramite error in qualsiasi contesto.

Why is catching an exception non-pure, but throwing an exception is pure?

Questo è del tutto accettabile e non affatto strano. Tuttavia, la cosa deludente è che Haskell non sembra fornire alcune funzionalità per vietare definizioni di funzioni che potrebbero portare a rami usando error.

Ecco un esempio inventato il motivo per cui ho trovato questo deludente:

module Main where 
import Data.Maybe 

data Fruit = Apple | Banana | Orange Int | Peach 
    deriving(Show) 

readFruit :: String -> Maybe Fruit 
readFruit x = 
    case x of 
     "apple" -> Just Apple 
     "banana" -> Just Banana 
     "orange" -> Just (Orange 4) 
     "peach" -> Just Peach 
     _ -> Nothing 

showFruit :: Fruit -> String 
showFruit Apple = "An apple" 
showFruit Banana = "A Banana" 
showFruit (Orange x) = show x ++ " oranges" 

printFruit :: Maybe Fruit -> String 
printFruit x = showFruit $ fromJust x 

main :: IO() 
main = do 
    line <- getLine 
    let fruit = readFruit line 
    putStrLn $ printFruit fruit 
    main 

Diciamo che sono paranoico che le funzioni pure readFruit e printFruit davvero non fallire a causa di stati unhanded. Si può immaginare che il codice sia per lanciare un missile pieno di astronauti che in una routine assolutamente critica ha bisogno di serializzare e non serializzare i valori della frutta.

Il primo pericolo è naturalmente che abbiamo commesso un errore nel nostro modello di corrispondenza in quanto questo ci dà i terribili stati errati che non possono essere gestiti. Fortunatamente Haskell fornisce costruito in modi per prevenire quelli, abbiamo semplicemente compilare il nostro programma con -Wall che comprende -fwarn-incomplete-patterns e AHA:

src/Main.hs:17:1: Warning: 
    Pattern match(es) are non-exhaustive 
    In an equation for ‘showFruit’: Patterns not matched: Peach 

abbiamo dimenticato di serializzare Frutta della pesca e showFruit avrebbe gettato un errore. Questa è una soluzione semplice, aggiungiamo semplicemente:

showFruit Peach = "A peach" 

Il programma ora compila senza avvisi, pericolo evitato! Lanciamo il razzo, ma improvvisamente il programma si blocca con:

Maybe.fromJust: Nothing 

Il razzo è condannato e colpisce l'oceano causato dalla seguente riga guasta:

printFruit x = showFruit $ fromJust x 

Essenzialmente fromJust ha un ramo in cui si solleva un Error quindi non volevamo nemmeno che il programma si compilasse se provassimo ad usarlo dal printFruit assolutamente doveva essere "super" puro. Avremmo potuto fissa che ad esempio sostituendo la linea con:

printFruit x = maybe "Unknown fruit!" (\y -> showFruit y) x 

Trovo strano che Haskell decide di attuare la tipizzazione forte e rilevazione modello incompleto, tutto nel perseguimento Nobel di prevenire gli stati non validi di essere rappresentabile ma cadute proprio di fronte al traguardo non dando ai programmatori un modo per rilevare i rami su error quando non sono consentiti.In un certo senso ciò rende Haskell meno robusto di Java, il che ti obbliga a dichiarare le eccezioni che le tue funzioni sono autorizzate a sollevare.

Il modo più semplice per implementare questo sarebbe semplicemente non definito error in qualche modo, localmente per una funzione e qualsiasi funzione utilizzata dalla sua equazione tramite una qualche forma di dichiarazione associata. Tuttavia questo non sembra essere possibile.

The wiki page about errors vs exceptions menziona un'estensione denominata "Extended Static Checking" per questo scopo tramite contratti ma porta semplicemente a un collegamento interrotto.

Si riduce fondamentalmente a: Come faccio a ottenere il programma di cui sopra per non compilare perché utilizza fromJust? Tutte le idee, i suggerimenti e le soluzioni sono benvenute.

Answer 1

La risposta è stata che volevo un livello di controllo totale che Haskell purtroppo non fornisce (ancora?).

In alternativa, desidero i tipi dipendenti (ad esempio Idris) o un verificatore statico (ad esempio Liquid Haskell) o il controllo del lint della sintassi (ad esempio hlint).

Ora sto cercando Idris, sembra un linguaggio sorprendente. Ecco uno talk by the founder of Idris che posso consigliare di guardare.

I crediti per queste risposte vanno a @duplode, @chi, @ user3237465 e @luqui.

Answer 2

Il tuo reclamo principale è di circa fromJust, ma dato che è fondamentalmente contro ciò che i tuoi obiettivi sono, perché lo stai usando?

Ricorda che il motivo principale per error è che non tutto può essere definito in un modo che il sistema di tipi può garantire, quindi avere un "Questo non può accadere, fidati" ha senso. fromJust deriva da questa mentalità di "a volte lo so meglio del compilatore". Se non sei d'accordo con quella mentalità non usarla. In alternativa non abusarne come in questo esempio.

EDIT:

Per espandere il mio punto, pensare a come si potrebbe implementare ciò che si sta chiedendo (avvertenze sull'utilizzo delle funzioni parziali). Dove si applicherebbe l'avvertenza nel seguente codice?

a = fromJust $ Just 1 
b = Just 2 
c = fromJust $ c 
d = fromJust 
e = d $ Just 3 
f = d b 

Tutti questi sono staticamente non parziale, dopo tutto. (Scusate se questa prossima di una sintassi è fuori, è tardi)

g x = fromJust x + 1 
h x = g x + 1 
i = h $ Just 3 
j = h $ Nothing 
k x y = if x > 0 then fromJust y else x 
l = k 1 $ Just 2 
m = k (-1) $ Just 3 
n = k (-1) $ Nothing 

i qui è di nuovo al sicuro, ma non è j. Quale metodo dovrebbe restituire l'avviso? Cosa facciamo quando alcuni o tutti questi metodi sono definiti al di fuori della nostra funzione. Cosa fai nel caso di k dove è condizionatamente parziale? Se alcune o tutte queste funzioni falliscono?

Facendo in modo che il compilatore effettui questa chiamata, si stanno creando molti problemi complicati. Soprattutto se si considera che un'attenta selezione della biblioteca lo evita.

In entrambi i casi, la soluzione IMO per questi tipi di problemi consiste nell'utilizzare uno strumento dopo o durante la compilazione per cercare i problemi anziché modificare il compilatore. Un tale strumento può comprendere più facilmente "il tuo codice" rispetto a "il suo codice" e determinare meglio dove meglio avvisarti in caso di uso inappropriato. Potresti anche ottimizzarlo senza dover aggiungere un po 'di annotazioni al tuo file sorgente per evitare falsi positivi. Non conosco uno strumento a mano o ne suggerirei uno.

Answer 3

Haskell consente la ricorsione generale arbitraria, quindi non è come se tutti i programmi Haskell fossero necessariamente totali, se solo error nelle sue varie forme venissero rimossi. Cioè, puoi semplicemente definire error a = error a per occuparti di ogni caso che non vuoi comunque gestire. Un errore di runtime è solo più utile di un ciclo infinito.

Non si dovrebbe pensare a error come simile a un'eccezione Java di tipo giardino. error è un errore di asserzione che rappresenta un errore di programmazione e una funzione come fromJust che può chiamare error è un'asserzione.Non tentare di rilevare l'eccezione prodotta da error tranne in casi particolari come un server che deve continuare a essere eseguito anche quando il gestore di una richiesta riscontra un errore di programmazione.