自由单子的Monad

Question

自由单子的Monad

haskellfree-monad

16

“x >>= f” 是否等同于 “retract (liftF x >>= liftF . f)”？也就是说，从一个同时满足 Functor 和 Monad 的自由 Monad 构建的 Monad 实例是否与原始的 Monad 实例等效？

- singpolyma

2个回答

4

即，从一个同时也是Monad的Functor构建的自由Monad实例，是否会有与原始Monad等效的Monad实例？

不会。任何Functor上的自由Monad都是一个Monad。因此，它不能在存在Monad实例时奇迹般地知道它。而且它也无法“猜测”，因为同一个Functor可能以不同的方式成为Monad（例如，对于不同的Monoid，可以使用Writer 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 (*)

- Roman Cheplyaka

1

是的，鉴于商数 Impure (a,mzero) = a，因此 Free (Writer m) a 同构于 Writer m a。Free (Writer m) a = Writer [m] a，如果您关心的是单子结构，则它们看起来相似。它们不同之处在于您可以编写一个函数来区分它们，另一方面，它们相同之处在于您可能不应该这样做 :)。 - Philip JF

1

我并不反对。这就是为什么它被称为撤销而不是同构。只是大多数情况下，你真的希望将Free m a视为与m a“相同”，将[m]视为与m“相同”。这可以很容易地通过使用商类型（在Haskell中我们只能假装存在）来形式化，并且是使用自由单子实现高效的Pipes的基础，即使该实现不遵守变换器定律（因为lift不是单子态射），即使你没有Haskell中使其“安全”的商类型。 - Philip JF

有多个可能的Monad实例似乎会破坏这个想法。你有一个好的例子吗？在不同的单子上编写是不同的实例，确实可以像我最初预期的那样工作。 - singpolyma

1

@RomanCheplyaka 这很好，但是retract仍然使用底层的Monad实例。Free monads应该始终比在functor上定义的任何其他monad更大。撤回应该是使Free成为通用的唯一映射，对吗？ - J. Abrahamson

我认为@tel是正确的。我们最终回到正确的“Monad”实例的原因是由于“retract”的实现方式。 - singpolyma

显示剩余7条评论

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Philip JF · Accepted Answer

我不知道你对“retract”的定义是什么，但考虑到IT技术，它通常指撤回、取消或撤销某个操作或决策。

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）。在函子范畴中，Free是一个函子，但它不是单子态范畴中的单子态（尽管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] "本质上是相同的"。