tipi esistenziale e trasformatori monade

Question

Contesto: Sto cercando di produrre una monade errore che tiene anche traccia di un elenco di avvisi, qualcosa di simile:

data Dangerous a = forall e w. (Error e, Show e, Show w) => 
    Dangerous (ErrorT e (State [w]) a) 

cioè Dangerous a è un'operazione con conseguente (Either e a, [w]) dove e è un errore visibile e w è visualizzabile.

Il problema è che non riesco a eseguire effettivamente la cosa, soprattutto perché non capisco molto bene i tipi esistenziali. Osservare:

runDangerous :: forall a e w. (Error e, Show e, Show w) => 
    Dangerous a -> (Either e a, [w]) 
runDangerous (Dangerous f) = runState (runErrorT f) [] 

Questo non si compila, perché:

Could not deduce (w1 ~ w) 
from the context (Error e, Show e, Show w) 
... 
`w1' is a rigidtype variable bound by 
    a pattern with constructor 
    Dangerous :: forall a e w. 
       (Error e, Show e, Show w) => 
       ErrorT e (State [w]) a -> Dangerous a 
... 
`w' is a rigid type variable bound by 
    the type signature for 
    runDangerous :: (Error e, Show e, Show w) => 
        Dangerous a -> (Either e a, [w]) 

Mi sono perso. Cosa c'è w1? Perché non possiamo dedurre che è ~ w?

Answer 1

Un esistenziale probabilmente non è quello che vuoi qui; non è possibile "osservare" i tipi effettivi associati a e o w in un valore Dangerous a, quindi si è completamente limitati alle operazioni fornite da Error e Show.

In altre parole, l'unica cosa che sai di w è che si può trasformarlo in un String, quindi potrebbe anche essere solo un String (ignorando la precedenza per semplificare le cose), e l'unica cosa che conosci e è possibile trasformarlo in un String, è possibile attivare String s e si dispone di un valore distinto di esso (noMsg). Non c'è modo di affermare o verificare che questi tipi siano uguali a tutti gli altri, quindi una volta che li hai inseriti in un Dangerous, non c'è modo di recuperare alcuna struttura speciale di quei tipi.

Quello che il messaggio di errore sta dicendo è che, in sostanza, il tipo di runDangerous crediti che è possibile trasformare un Dangerous in un (Either e a, [w]) per qualsiasie e w che hanno le istanze competenti. Questo chiaramente non è vero: puoi solo convertire un Dangerous in quel tipo per uno scelta di e e w: quello con cui è stato creato. Il w1 è solo perché il tuo tipo Dangerous è definito con una variabile di tipo w, e così è runDangerous, quindi GHC rinomina uno di essi per evitare conflitti di nome.

Il tipo è necessario dare runDangerous assomiglia a questo:

runDangerous 
    :: (forall e w. (Error e, Show e, Show w) => (Either e a, [w]) -> r) 
    -> Dangerous a -> r 

che, data una funzione che accetta un valore di tipo (Either e a, [w]) per eventuali scelte di e e w fintanto che hanno la istanze fornite e un Dangerous a produce il risultato di quella funzione. Questo è abbastanza difficile da capire!

L'implementazione è semplice come

runDangerous f (Dangerous m) = f $ runState (runErrorT m) [] 

che è un cambiamento banale per la vostra versione. Se questo funziona per te, ottimo; ma dubito che un esistenziale sia il modo giusto per ottenere qualunque cosa tu stia cercando di fare.

Nota che è necessario il {-# LANGUAGE RankNTypes #-} per esprimere il tipo di runDangerous. In alternativa, è possibile definire un altro esistenziale per il vostro tipo di risultato:

data DangerousResult a = forall e w. (Error e, Show e, Show w) => 
    DangerousResult (Either e a, [w]) 

runDangerous :: Dangerous a -> DangerousResult a 
runDangerous (Dangerous m) = DangerousResult $ runState (runErrorT m) [] 

ed estrarre il risultato con case, ma dovrete stare attenti, o GHC inizierà lamentando che hai lasciato e o w fuga - che è l'equivalente del tentativo di passare una funzione insufficientemente polimorfica all'altra forma di runDangerous; cioè uno che richiede più vincoli su ciò che e e w sono oltre ciò che garantisce il tipo di runDangerous.

Answer 2

Ok, credo di aver capito quello che stavo dibatte dopo: (. instance Monad Dangerous e data DangerousT aiuto troppo)

data Failure = forall e. (Error e, Show e) => Failure e 

data Warning = forall w. (Show w) => Warning w 

class (Monad m) => Errorable m where 
    warn :: (Show w) => w -> m() 
    throw :: (Error e, Show e) => e -> m() 

instance Errorable Dangerous where 
    warn w = Dangerous (Right(), [Warning w]) 
    throw e = Dangerous (Left $ Failure e, []) 

Questo permette di avere il seguente codice:

foo :: Dangerous Int 
foo = do 
    when (badThings) (warn $ BadThings with some context) 
    when (worseThings) (throw $ BarError with other context) 

data FooWarning = BadThings FilePath Int String 
instance Show FooWarning where 
... 

e quindi nel modulo principale è possibile definire istanze personalizzate di Show Failure, Error Failure e Show Warning a ND avere un modo centralizzato per formattare i messaggi di errore, ad esempio

instance Show Warning where show (Warning s) = "WARNING: " ++ show s 
instance Show Failure where ... 

let (result, warnings) = runDangerous function 
in ... 

Il che, a mio parere, è un modo abbastanza freddo per gestire gli errori e gli avvisi. Ho un modulo funzionante che è qualcosa del genere, ora sono pronto per ripulirlo e magari metterlo sul hackage. Suggerimenti apprezzati.