haskell - 单子的自由单子

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单子态射（不去）。Free 是函子类别中的函子，但它不是单子类别中的单子（尽管看起来很像并且看起来很像）。returnreturnretractjoinliftFreturn

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

 ~ : 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因此，一个单子上的自由单子就是那个单子加上一些额外的数据。这与当is是一个幺半群时[m]“本质上相同”的声明完全相同。mmm

Answer 2

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

不。任何函子上的自由单子都是单子。因此，它不能神奇地知道 Monad 实例何时存在。它也不能“猜测”它，因为同一个函子可能以不同的方式成为 Monad（例如，不同幺半群的 writer monad）。

另一个原因是问这两个 monad 是否有等价的实例没有多大意义，因为它们甚至不是同构的类型。例如，考虑一下 writer monad 上的 free 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 (*)