问题 FreeT是否保留Free的等式推理优势？

是。 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

让我们使用以下定义免费monad变换器：

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！）并且遵守monad法律。

仅使用monad法则，我们仍然能够推断出这一点 exitSuccess >> m = exitSuccess。这就是为什么monad法则很重要的原因，因为它们允许我们在多态基monad上推理代码，只知道它是monad。

更一般地说，这就是人们说类型类应该始终具有相关法则（如monad法则，或者函子法则或类别法则）的原因，因为这些允许您在不咨询的情况下推理使用该类型类的代码该类型类的特定实例。如果没有这些类型的规则，类型类接口就不会真正成为松散耦合的接口，因为如果不咨询原始实例源代码，就无法对其进行等价推理。

此外，如果你想要额外的类别理论，我们可以很容易地证明每一个属性 Free 也必须坚持 FreeT 如果基础monad是多态的。我们所要做的就是证明：

(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

这是一个有趣的证据，我把它留作练习！