自由 monad 和自由操作

Question

描述 Free monad 的一种方法是说它是内函子类别中的 initial 幺半群（属于某些类别 C），其对象是内函子从C到C，箭头是它们之间的自然转换。如果我们把C变成Hask，endofunctor就是haskell中的Functor，它是* -> *中的函子，其中*代表Hask

的对象

根据初始值，从内函子 t 到 End(Hask) 中的幺半群 m 的任何映射都会导出从 Free t 到 m 的映射。

换句话说，从 Functor t 到 Monad m 的任何自然转换都会引起从 Free t 到 m

的自然转换

我本来希望能够编写一个函数

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta)

但这无法统一，而以下工作

free :: (Functor t, Monad m) => (t (m a) → m a) → (Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta)

或其带有签名的泛化

free :: (Functor t, Monad m) => (∀ a. t a → a) → (∀ a. Free t a → m a)

我是不是在范畴论中犯了错误，或者在翻译到 Haskell 时犯了错误？

我很想听听这里的一些智慧..

PS : 启用的代码

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
import Control.Monad.Free

Answer 1

Haskell 翻译好像有误。一个重要提示是您的 free 实现没有在任何地方使用单子绑定（或连接）。您可以通过以下定义找到 free 作为 foldFree：

free :: Monad m => (forall x. t x -> m x) -> (forall a. Free t a -> m a)
free f (Pure a)  = return a
free f (Free fs) = f fs >>= free f

重点是f专攻t (Free t a) -> m (Free t a)，一举消除一层Free

Answer 2

我不知道类别理论部分，但 Haskell 部分绝对不是 well-typed 您的原始实现和原始类型签名。

给定

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)

当您在 Free tfta 上进行模式匹配时，您会得到

tfta :: t (Free t a)
f :: forall a. t a -> m a 
free :: (forall a. t a -> m a) -> forall a. Free t a -> m a

因此

free f :: forall a. Free t a -> m a

导致

fmap (free f) :: forall a. t (Free t a) -> t (m a)

因此，为了能够将 t (m a) 折叠成您想要的 m a，您需要对其应用 f（至 "turn the t into an m"），然后利用这一事实m 是一个 Monad:

f . fmap (free f) :: forall a. t (Free t a) -> m (m a)
join . f . fmap (free f) :: forall a. t (Free t a) -> m a

这意味着您可以通过更改 free 的第二个分支来修复您的原始定义：

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

import Control.Monad.Free
import Control.Monad

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free tfta) = join . f . fmap (free f) $ tfta

这个类型检查，可能就是你想要的:)

自由 monad 和自由操作

Free monad and the free operation

monads

haskell

category-theory

free-monad