FreeT是否保持Free的等價推理優勢？

Question

在此blog post中，作者解釋了使用Free monad淨化代碼的等式推理優勢。 Free monad變壓器FreeT是否保留了這些好處，即使它包裹了IO？

Answer 1

是的。 FreeT不依賴於基本monad的任何特定屬性，除了它是monad的事實。你可以推導出的每個等式對Free f都有FreeT f m的等價證明。

爲了演示，讓我們重複在我的博客文章鍛鍊，但使用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 

讓我們用以下定義爲免費單子變壓器：

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) 

我們可以使用等式推理推導出什麼exitSuccess簡化爲：

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

現在我們可以數落該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 

在證明的do塊屬於基地單子，但我們從來不需要使用基單子的任何特定的源代碼或屬性，以操縱它是等價的。我們需要知道的唯一財產是它是一個monad（任何monad！）並且遵守monad法則。

僅使用monad法則，我們仍然能夠推斷出exitSuccess >> m = exitSuccess。這就是爲什麼monad法律很重要的原因，因爲它們允許我們在多態基本monad上推理代碼，只知道它是monad。更一般地說，這就是人們認爲類型類應該總是有相關法則（如單子法，仿函數法或類別法）的原因，因爲這些類允許你推理使用該類的代碼類型的類而不諮詢該類型的特定實例。沒有這些類型的規則，類型類接口就不會真正成爲一個鬆散耦合的接口，因爲如果不諮詢原始實例源代碼，您將無法以等同方式推理它。另外，如果你想要額外劑量的類別理論，我們可以很容易地證明，如果基本monad是多態的，那麼對於Free持有的每個屬性也必須適用FreeT。我們所要做的就是證明：

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

的~符號表示「同構」，這意味着我們必須證明有兩個功能，fw，並且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) 

...這樣的：

fw . bw = id 

bw . fw = id 

這是一個有趣的證明，我把它作爲一個練習！