FreeT mantiene i vantaggi del ragionamento equazionale di Free?

Question

In questo blog post, l'autore spiega i vantaggi di ragionamento equo del codice di purificazione con la monade libera. Il trasformatore gratuito monad FreeT conserva questi benefici, anche se è avvolto su IO?

Answer 1

Sì. FreeT non dipende da alcuna proprietà specifica della monade di base, oltre al fatto che si tratta di una monade. Ogni equazione che è possibile dedurre per Free f ha una prova equivalente per FreeT f m.

Per dimostrare che, ripetiamo l'esercizio nel mio post sul blog, ma questa volta usando FreeT:

data TeletypeF x 
    = PutStrLn String x 
    | GetLine (String -> x) 
    | ExitSuccess 
    deriving (Functor) 

type Teletype = FreeT TeletypeF 

exitSuccess :: (Monad m) => Teletype m r 
exitSuccess = liftF ExitSuccess 

Usiamo le seguenti definizioni gratuitamente da trasformatori monade:

return :: (Functor f, Monad m) => r -> FreeT f m r 
return r = FreeT (return (Pure r)) 

(>>=) :: (Functor f, Monad m) => FreeT f m a -> (a -> FreeT f m b) -> FreeT f m b 
m >>= f = FreeT $ do 
    x <- runFreeT m 
    case x of 
     Free w -> return (Free (fmap (>>= f) w)) 
     Pure r -> runFreeT (f r) 

wrap :: (Functor f, Monad m) => f (FreeT f m r) -> FreeT f m r 
wrap f = FreeT (return (Free f)) 

liftF :: (Functor f, Monad m) => f r -> FreeT f m r 
liftF fr = wrap (fmap return fr) 

Possiamo usare ragionamento equo per dedurre quello che exitSuccess si riduce a:

exitSuccess 

-- Definition of 'exitSuccess' 
= liftF ExitSuccess 

-- Definition of 'liftF' 
= wrap (fmap return ExitSuccess) 

-- fmap f ExitSuccess = ExitSuccess 
= wrap ExitSuccess 

-- Definition of 'wrap' 
= FreeT (return (Free ExitSuccess)) 

Ora possiamo rimproverare che exitSuccess >> m = exitSuccess:

exitSuccess >> m 

-- m1 >> m2 = m1 >>= \_ -> m2 
= exitSuccess >>= \_ -> m 

-- exitSuccess = FreeT (return (Free ExitSuccess)) 
= FreeT (return (Free ExitSuccess)) >>= \_ -> m 

-- use definition of (>>=) for FreeT 
= FreeT $ do 
    x <- runFreeT $ FreeT (return (Free ExitSuccess)) 
    case x of 
     Free w -> return (Free (fmap (>>= (\_ -> m)) w)) 
     Pure r -> runFreeT ((\_ -> m) r) 

-- runFreeT (FreeT x) = x 
= FreeT $ do 
    x <- return (Free ExitSuccess) 
    case x of 
     Free w -> return (Free (fmap (>>= (\_ -> m)) w)) 
     Pure r -> runFreeT ((\_ -> m) r) 

-- Monad Law: Left identity 
-- do { y <- return x; m } = do { let y = x; m } 
= FreeT $ do 
    let x = Free ExitSuccess 
    case x of 
     Free w -> return (Free (fmap (>>= (\_ -> m)) w)) 
     Pure r -> runFreeT ((\_ -> m) r) 

-- Substitute in 'x' 
= FreeT $ do 
    case Free ExitSuccess of 
     Free w -> return (Free (fmap (>>= (\_ -> m)) w)) 
     Pure r -> runFreeT ((\_ -> m) r) 

-- First branch of case statement matches 'w' to 'ExitSuccess' 
= FreeT $ do 
    return (Free (fmap (>>= (\_ -> m)) ExitSuccess)) 

-- fmap f ExitSuccess = ExitSuccess 
= FreeT $ do 
    return (Free ExitSuccess) 

-- do { m; } desugars to 'm' 
= FreeT (return (Free ExitSuccess)) 

-- exitSuccess = FreeT (return (Free ExitSuccess)) 
= exitSuccess 

Il do blocco nella dimostrazione apparteneva alla monade di base, eppure abbiamo mai avuto bisogno di usare qualsiasi codice sorgente specifico o proprietà della monade di base al fine di manipolare in modo equo L'unica proprietà che dovevamo sapere era che era una monade (qualsiasi monade!) E obbediva alle leggi della monade.

Utilizzando solo le leggi della monade, siamo ancora in grado di dedurre che exitSuccess >> m = exitSuccess. Questo è il motivo per cui le leggi della monade sono importanti, perché ci permettono di ragionare sul codice su una monade di base polimorfa, sapendo solo che è una monade.

Più in generale, questo è il motivo per cui le persone dicono che le classi di tipi dovrebbero sempre avere leggi associate (come le leggi monad, o le leggi sui funtori o le leggi di categoria), perché consentono di ragionare sul codice che usa quello scrivi una classe senza consultare le istanze specifiche di quella classe di tipi. Senza questo tipo di leggi, l'interfaccia di classe del tipo non sarebbe veramente un'interfaccia liberamente accoppiato dato che non sarebbe in grado di ragionare in modo equo senza consultare il codice sorgente dell'istanza originale.

Inoltre, se si desidera una dose aggiuntiva di teoria delle categorie, si può facilmente provare che ogni proprietà valida per Free deve essere valida anche per FreeT se la monade di base è polimorfa. Tutto ciò che dobbiamo fare è dimostrare che:

(forall m. (Monad m) => FreeT f m r) ~ Free f r 

Il simbolo ~ significa "è isomorfo a", il che significa che dobbiamo dimostrare che ci sono due funzioni, fw e bw:

fw :: (forall m . (Monad m) => FreeT f m r) -> Free f r 

bw :: Free f r -> (forall m . (Monad m) => FreeT f m r) 

... tale che:

fw . bw = id 

bw . fw = id 

È una prova interessante, e lo lascio come un esercizio!