haskell - 单子(monad)的自由单子(monad)

Question

是 x >>= f相当于 retract (liftF x >>= liftF . f) ?

也就是说，从同样是 Monad 的 Functor 构建的自由 monad 的 monad 实例是否将具有与原始 Monad 等效的 monad 实例？

Answer 1

我不知道你对 retract 的定义是什么是，但给定

retract :: Monad m => Free m a -> m a
retract (Pure a) = return a
retract (Impure fx) = fx >>= retract

和

liftF :: Functor f => f a -> Free f a
liftF fx = Impure (fmap Pure fx)

请注意(证明可能是错误的，手工制作并且没有检查过)

retract $ liftF x
= retract (Impure (fmap Pure x))
= (fmap Pure x) >>= retract
= (x >>= return . Pure) >>= retract
= x >>= \y -> (return $ Pure y) >>= retract
= x >>= \y -> (retract (Pure y))
= x >>= \y -> return y
= x >>= return
= x

所以你有了

retract (liftF x >>= liftF . f)
= retract ((Impure (fmap Pure x)) >>= liftF . f)
= retract $ Impure $ fmap (>>= liftF . f) $ fmap Pure x
= (fmap (>>= liftF . f) $ fmap Pure x) >>= retract
= (fmap (\y -> Pure y >>= liftF . f) x) >>= retract
= (fmap (liftF . f) x) >>= retract
= (liftM (liftF . f) x) >>= retract
= (x >>= return . liftF . f) >>= retract
= x >>= (\y -> (return $ liftF $ f y >>=  retract)
= x >>= (\y -> retract $ liftF $ f y)
= x >>= (\y -> retract . liftF $ f y)
= x >>= (\y -> f y)
= x >>= f

这并不意味着 Free m a与 m a 同构, 就是 retract真是见证了一次撤退。请注意 liftF不是单子(monad)态射( return 不去 return )。 Free 是仿函数类别中的仿函数，但它不是单子(monad)类别中的单子(monad)(尽管 retract 看起来很像 join 和 liftF 看起来很像 return )。

编辑:请注意，撤回意味着一种等价。定义

 ~ : Free m a -> Free m a -> Prop
 a ~ b = (retract a) ==_(m a) (retract b)

然后考虑商类型 Free m a/~ .我断言这种类型与 m a 同构。 .由于 (liftF (retract x)) ~ x因为 (retract . liftF . retract $ x) ==_(m a) retract x .因此，一个单子(monad)上的自由单子(monad)就是那个单子(monad)加上一些额外的数据。这与 [m] 的主张完全相同。与 m“基本相同”当 m是 m是一个幺半群。