Si tratta di un uso sicuro di unsafeCoerce?

Question

Ho una situazione in cui sono al momento utilizzando la funzione estremamente spaventosa unsafeCoerce. Non è per niente importante per fortuna, ma mi chiedevo se questo sembra essere un uso sicuro di questa funzione, o se ci sarebbe un altro modo per risolvere questo particolare problema che altre persone conoscono.

Il codice che ho è qualcosa di simile al seguente:

data Token b = Token !Integer 

identical :: Token a -> Token b -> Bool 
identical (Token a) (Token b) = a == b 

data F a = forall b. F (Token b) (a -> b) 

retrieve :: Token b -> F a -> Maybe (a -> b) 
retrieve t (F t' f) = if identical t t' then Just (unsafeCoerce f) else Nothing 

Due cose aggiuntive da notare, sono che questi segnalini sono utilizzati all'interno di una monade che io uso per garantire che la fornitura di interi per loro è unico (cioè non faccio lo stesso token due volte). Io uso anche una variabile di tipo shadow foriforme quantificata, allo stesso modo della monade ST, per assicurarmi che (assumendo solo i metodi che espongo nel modulo vengano usati) non c'è modo di restituire un token (o in realtà anche un F) dalla monade senza che si tratti di un errore di tipo. Inoltre non espongo il costruttore di token.

Penso che, per quanto posso vedere, questo dovrebbe essere un uso sicuro di unsafeCoerce, come posso dire con (spero) abbastanza alta fiducia che il valore che sto costringendo è in realtà esattamente il tipo che io lo sto costringendo a, ma potrei sbagliarmi. Ho anche provato a usare Data.Typeable, che funziona bene, ma al momento sto cercando di evitare il vincolo Typeable, specialmente visto che gcast sembra fare qualcosa in molti modi simili, e comunque avrei comunque bisogno dei token per distinguere tra F diverse dello stesso tipo.

Grazie mille per qualsiasi aiuto/consiglio.

Answer 1

Non è sicuro per sé:

oops :: F Bool 
oops = F (Token 12) not 

bad :: Token Int 
bad = Token 12 

*Token> maybe 3 ($ True) $ retrieve bad oops 
1077477808 

F a è un tipo esistenzialmente quantificata, non si sa che tipo b andato in esso. Poiché identical non si preoccupa dei parametri di tipo su Token, non è in grado di verificare se il primo argomento fornito da retrieve dal retrieve ha qualcosa a che fare con ciò che è andato in F a.

Sia che la vostra protezione

Due cose aggiuntive da notare, sono che questi segni sono utilizzati all'interno di una monade che io uso per garantire che la fornitura di numeri interi per loro è unico (cioè non faccio il stesso token due volte). Io uso anche una variabile di tipo shadow foriforme quantificata, allo stesso modo della monade ST, per assicurarmi che (assumendo solo i metodi che espongo nel modulo vengano usati) non c'è modo di restituire un token (o in realtà anche un F) dalla monade senza che si tratti di un errore di tipo. Inoltre non espongo il costruttore di token.

è abbastanza forte da renderlo sicuro nella pratica, non posso dirlo senza vederlo. Se infatti non è possibile creare Token s al di fuori del calcolo e il valore Integer di Token caratterizza in modo univoco il parametro type, sarebbe sicuro.

Answer 2

È stata implementata una forma limitata di digitazione dinamica, seguendo ampiamente lo stile di Data.Dynamic, ovvero, un valore (opaco) di confronto con la prova del suo tipo. In fase di esecuzione è possibile eseguire una coercizione non sicura, in base alle prove fornite con i dati.

fromDyn (Dynamic t v) def 
    | typeOf def == t = unsafeCoerce v 
    | otherwise  = def 

Questo è l'approccio canoncial, con una lunga storia, che risale a:

Mart'ın Abadi, Luca Cardelli, Benjamin Pierce, e Gordon Plotkin. Digitazione dinamica in un linguaggio tipizzato staticamente. transazioni ACM su linguaggi di programmazione e sistemi, 13 (2): 237-268, aprile 1991.

La sicurezza del metodo si basa sulla unforgeability di tipo runtime gettoni. Nel tuo caso, chiunque può creare un token che equivalga a due tipi: è necessario garantire un 1-1 di mapping da tipi a token e assicurarsi che un utente malintenzionato non possa costruire token non corretti. Nel caso di GHC, ci fidiamo delle istanze Typeable (e dell'astrazione del modulo).