Come posso raccogliere un elenco di azioni ST all'interno di Either?

Question

Come posso convertire un [Either ST] in un Either [ST] e successivamente eseguire le azioni in sequenza? Il codice riportato di seguito sembra funzionare per l'esecuzione di un elenco di azioni ST, tuttavia quando si tenta di generare l'elenco di azioni in O (scambiando le definizioni test di seguito) i tipi non vengono più allineati. Mi sarei aspettato che i tipi di liste fossero identici, quindi avrei apprezzato molto qualsiasi spiegazione delle differenze.

{-# LANGUAGE RankNTypes #-} 

import qualified Data.STRef as ST 
import qualified Control.Monad.ST as ST 

run :: (forall s. [ST.STRef s Int -> ST.ST s Int]) -> Int 
run fs = 
    ST.runST $ do 
    x <- ST.newSTRef 0 
    mapM_ (\f -> 
     f x >>= ST.writeSTRef x 
    ) fs 
    ST.readSTRef x 

action :: ST.STRef s Int -> ST.ST s Int 
action = \x -> ST.readSTRef x >>= \y -> return (y + 1) 

-- test :: Either String Int 
-- test = mapM (const (return action)) [0..5] >>= \fs -> return (run fs) 

test :: Int 
test = run (map (const action) [0..5]) 

main = print test 

Answer 1

L'inferenza di tipo in presenza di tipi di rango superiore è indecidibile. L'algoritmo di inferenza del tipo di GHC semplifica alcune ipotesi, che lo rendono incompleto. Questi includono:

• GHC assumerà la variabile legata da una lambda è un monotipo (? Non contiene (leader) forall s)

• Quando si utilizza una funzione polimorfica, GHC assumerà che le variabili di tipo gratuiti a suo tipo saranno istanziati in monotipi

Entrambe queste ipotesi possono essere sovrascritti se chiedete GHC cortesemente di utilizzare un particolare polytype invece.

Ora, come prevedete che il vostro programma scriva check?

• Affinché run fs digitare controllare, faremmo meglio avere fs :: forall s. [ST.STRef s Int -> ST.ST s Int]
• Così, secondo il primo punto di cui sopra deve scrivere questa firma tipo sul lambda che lo lega: \(fs :: forall s. [ST.STRef s Int -> ST.ST s Int]) -> ... (usando ScopedTypeVariables)

• Considerare ora l'uso di >>=. Il suo tipo è Monad m => m a -> (a -> m b) -> m b. Ma, abbiamo bisogno di a = forall s. [ST.STRef s Int -> ST.ST s Int]. Quindi, in base al secondo punto di cui sopra abbiamo bisogno di dare a questo >>= una firma tipo, come in

  ... `op` (\(fs :: forall s. [ST.STRef s Int -> ST.ST s Int]) -> ...) 
      where op :: Monad m 
        => m (forall s. [ST.STRef s Int -> ST.ST s Int]) 
        -> ((forall s. [ST.STRef s Int -> ST.ST s Int]) -> m b) 
        -> m b 
        op = (>>=) 
  

• Ora ci imbattiamo in un nuovo tipo di problema. In questa applicazione di op, il primo argomento ha tipo Either String (forall s. [ST.STRef s Int -> ST.ST s Int]). L'applicazione di un costruttore di tipi (diverso da (->)) a un politipo non è consentita, a meno che non si attivino i tipi di errore (danneggiati). Tuttavia, possiamo accenderlo e continuare ...
• Immergersi nel primo argomento, possiamo vedere che avremo bisogno di return :: Monad m => a -> m a istanziato a a = forall s. ST.STRef s Int -> ST.ST s Int. Quindi, abbiamo bisogno di aggiungere un'altra firma tipo di return
• Allo stesso modo avremo bisogno mapM :: Monad m => (a -> m b) -> [a] -> m [b] un'istanza in b = forall s. ST.STRef s Int -> ST.ST s Int

• Se si sta prestando molta attenzione si nota ancora un altro problema: il risultato della mapM ha digitare

  Either String [forall s. ST.STRef s Int -> ST.ST s Int] 
  

  ma l'argomento di (>>=) deve essere di tipo

  Either String (forall s. [ST.STRef s Int -> ST.ST s Int]) 
  

  e si avrà bisogno di convertire tra questi.In realtà si tratta di un no-op, ma GHC non è abbastanza intelligente da sapere che, in modo da avere per fare una conversione lineare-tempo, qualcosa di simile a

  liftM (\x -> map (\(y :: forall s. ST.STRef s Int -> ST.ST s Int) -> y) x) 
  

  (tranne liftM avrà bisogno di ancora un altro firma tipo)

Morale della storia: puoi farlo, ma non dovresti.

È in genere hanno un tempo più facile se si nasconde il tuo forall s newtypes dentro come

newtype S s = S { unS :: forall s. ST.STRef s Int -> ST.ST s Int } 

che rende i punti in cui il polimorfismo viene introdotto più esplicito nel programma (tramite le occorrenze di S e unS).

Answer 2

È necessario disporre le funzioni in un newtype per conservare la quantificazione esistenziale senza dover utilizzare ImpredicativeTypes.

{-# LANGUAGE RankNTypes #-} 

import qualified Data.STRef as ST 
import qualified Control.Monad.ST as ST 

newtype STFunc = STFunc (forall s. ST.STRef s Int -> ST.ST s Int) 

run :: [STFunc] -> Int 
run fs = ST.runST $ do 
    x <- ST.newSTRef 0 
    mapM_ (\(STFunc f) -> 
     f x >>= ST.writeSTRef x 
    ) fs 
    ST.readSTRef x 

action :: STFunc 
action = STFunc $ \x -> ST.readSTRef x >>= \y -> return (y + 1) 

test :: Either String Int 
test = mapM (const (return action)) [0..5] >>= \fs -> return (run fs) 

main = print test