38

我们从范畴论中知道，并非Set中的所有内函子都承认一个自由单子。典型的反例是幂集函子。

但是 Haskell 可以将任何函子变成一个自由的单子。

data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Monad (Free f) where
  return = Pure
  Pure a >>= f = f a
  Free m >>= f = Free ((>>= f) <$> m)

是什么让这个构造适用于任何 Haskell 仿函数但在Set中分解？

4

2 回答 2

4

很明显，这个答案是错误的。我把它留在这里是为了在评论中保留有价值的讨论，直到有人提出正确的答案。

考虑设置在 中的功率Set。如果我们有一个函数f : S -> T，我们可以f' : PS S -> PS T通过f' X = f [X]. 很好的协变函子（我认为）。我们也可以形成f'' X = f^(-1) [X]一个很好的逆变函子（我认为）。

让我们看一下 Haskell 中的“幂集”：

newtype PS t = PS (t -> Bool)

这不是一个Functor，而只是一个Contravariant：

instance Contravariant PS where
  contramap f (PS g) = PS (g . f)

我们认识到这一点t是因为处于负面地位。与 不同Set，我们无法获得构成幂集的特征函数的“元素”，因此协变函子不可用。

因此，我猜想，Haskell 承认每个协变函子都有一个自由单子的原因是它排除了那些对Set.

于 2016-01-02T18:18:30.670 回答
1

我（相当）怀疑这不完全是一个定义。比如说，这个递归公式指定了一个固定点；现在，我们怎么知道这个固定点存在？我们怎么知道只有一个固定点？还有更多，如何Free m >>=定义任何东西，除非我们假设我们只有有限的应用序列Free？

于 2016-01-03T17:47:35.263 回答