Czy FreeT zachowuje równania rozumowania korzyści Free?

Question

W tym blog post autor wyjaśnia korzyści z racjonalnego rozumowania oczyszczania kodu z Free monad. Czy darmowy transformator monad FreeT zachowuje te zalety, nawet jeśli jest zawarty w IO?

Answer 1

Tak. FreeT nie zależy od żadnych szczególnych właściwości monady podstawowej, poza tym, że jest monadą. Każde równanie, które można wydedukować dla Free f ma równoważny dowód dla FreeT f m.

Aby wykazać, że, powiedzmy, powtórz ćwiczenie w moim blogu, ale tym razem przy użyciu 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 

Użyjmy następujące definicje dla wolnych transformatorów monady:

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) 

Możemy użyć rozumowanie równania w celu dedukcji, co exitSuccess zmniejsza się do:

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)) 

Teraz możemy ganić że 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 

Blok w dowodzie do należał do monady bazowej, jeszcze nigdy nie musiał korzystać z żadnego konkretnego kodu źródłowego lub właściwości monady bazowej w celu manipulowania to równanie. Jedyną własnością, którą musieliśmy wiedzieć, była monada (jakakolwiek monada!) I była ona posłuszna prawom monady.

Korzystając tylko z praw monady, wciąż byliśmy w stanie wywnioskować, że exitSuccess >> m = exitSuccess. To jest powód, dla którego prawa monady mają znaczenie, ponieważ pozwalają nam rozumować o kodzie nad polimorficzną podstawową monadą, wiedząc tylko, że jest to monada.

Mówiąc ogólnie, ludzie twierdzą, że klasy typów powinny mieć zawsze powiązane prawa (np. Prawa monad, prawa funktora lub prawa kategorii), ponieważ pozwalają ci na rozumowanie o kodzie, który używa tego wpisz klasę bez sprawdzania konkretnych instancji klasy tego typu. Bez tego rodzaju praw interfejs typu typu nie byłby naprawdę luźno sprzężonym interfejsem, ponieważ nie byłbyś w stanie zrównoważyć go bez konsultacji z oryginalnym kodem źródłowym instancji.

Ponadto, jeśli chcesz uzyskać dodatkową dawkę teorii kategorii, możemy łatwo dowieść, że każda właściwość, która ma wartość Free, musi również zawierać FreeT, jeśli podstawowa monada jest polimorficzna. Wszystko, co musimy zrobić, to udowodnić, że:

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

~ symbol oznacza "jest izomorficzna", co oznacza, że ​​musimy udowodnić, że istnieją dwie funkcje, fw i 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) 

... takie, że:

fw . bw = id 

bw . fw = id 

Jest to interesujący dowód i pozostawiam go jako ćwiczenie!