Monad中的自由Monad

Question

x >>= f是否等同于retract (liftF x >>= liftF . f)

也就是说，从函数器构建的免费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不是一元态射(return不会转到return)。自由是函数式中的函数式，但它不是单元式中的单元式(尽管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“本质上相同”的说法完全相同。

Answer 2

也就是说，从函数器构建的免费Monad的monad实例是否将具有与原始monad相同的Monad实例？

不是的。任何函数器上的自由单子都是单子。因此，当Monad实例存在时，它不能神奇地知道它。而且它也不能“猜测”它，因为同一个函数器可能会以不同的方式成为Monad (例如，不同monad的写入器monad)。

另一个原因是，询问这两个monad是否具有等价的实例没有多大意义，因为它们甚至不与类型同构。例如，考虑免费monad而不是writer monad。它将是一个类似列表的结构。这两个实例相等意味着什么？

不同monad实例的示例

如果上面的描述不清楚，这里有一个包含许多可能的Monad实例的类型示例。

data M a = M Integer a

bindUsing :: (Integer -> Integer -> Integer) -> M a -> (a -> M b) -> M b
bindUsing f (M n a) k =
  let M m b = k a
  in M (f m n) b

-- Any of the below instances is a valid Monad instance
instance Monad M where
  return x = M 0 x
  (>>=) = bindUsing (+)

instance Monad M where
  return x = M 1 x
  (>>=) = bindUsing (*)