Il cucchiaio non è sicuro in Haskell?

Question

Quindi c'è una biblioteca in Haskell chiamato spoon che mi permette di fare questo

safeHead :: [a] -> Maybe a 
safeHead = spoon . head 

ma permette anche a fare questo

>>> spoon True    :: Maybe Bool 
Just True 
>>> spoon (error "fork") :: Maybe Bool 
Nothing 
>>> spoon undefined  :: Maybe Bool 
Nothing 
>>> spoon (let x = x in x) :: Maybe Bool 
<... let's just keep waiting...> 

che sembra davvero utile in alcuni casi, ma viola anche la semantica denotazionale (a mio parere) poiché mi permette di distinguere tra cose diverse nella preimage semantico di ⊥. Questo è strettamente più potente di throw/catch poiché probabilmente hanno una semantica definita da continuazioni.

>>> try $ return (error "thimble") :: IO (Either SomeException Bool) 
Right *** Exception: thimble 

Quindi la mia domanda è: qualcuno può usare cucchiaio maliziosamente a rompere la sicurezza di tipo? La convenienza vale il pericolo? O, più realisticamente, c'è un modo ragionevole per usarlo potrebbe erodere la fiducia di qualcuno nel significato di un programma?

Answer 1

C'è un punto difficile in cui, se lo si utilizza, fare quello che sembra un refacting innocente può modificare il comportamento di un programma. Senza alcuna campane e fischietti, è questa:

f h x = h x 
isJust (spoon (f undefined)) --> True 

ma facendo forse la trasformazione Haskell più comune nel libro, eta contrazione, a f, dà

f h = h 
isJust (spoon (f undefined)) --> False 

Eta contrazione non è già la semantica conservazione a causa dell'esistenza di seq; ma senza una contrazione, eta può solo trasformare un programma di terminazione in un errore; con la contrazione del cucchiaio eta è possibile modificare un programma di terminazione in un programma di terminazione diverso.

Formalmente, il modo in cui lo spoon non è sicuro è che è non-monotone on domains (e quindi può essere definito in termini di funzioni); mentre senza spoon ogni funzione è monotona. Quindi tecnicamente si perde quella utile proprietà del ragionamento formale.

Venendo con un esempio reale di quando questo sarebbe importante è lasciata come esercizio per il lettore (leggi: Penso che è molto improbabile che la materia nella vita reale - a meno che non si avvia abusarne; es. usando undefined il modo in cui i programmatori Java usano null)

Answer 2

Non è possibile scrivere unsafeCoerce con spoon, se è quello che si ottiene. E 'proprio così infelice come sembra, e viola la semantica di Haskell esattamente come sembra. Tuttavia, non è possibile utilizzarlo per creare un segfault o qualcosa di simile.

Tuttavia, violando la semantica Haskell, è rendere il codice più difficile da ragionare in generale, e anche, ad es. uno safeHead con cucchiaio sarà necessariamente meno efficiente di uno safeHead scritto direttamente.