Monad的免费Monad

Question

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

也就是说,一个免费monad构建的monad实例是一个Functor,它也是一个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是不是一个单子射(return不进入return).自由是仿函数类的仿函数,但它不是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是一个幺半群.