如何为 Free Monads 使用 Church 编码？

Question

我一直在使用 free 包中的 Control.Monad.Free 中的 Free 数据类型。现在我正在尝试将其转换为在Control.Monad.Free.Church 中使用F，但不知道如何映射函数。

例如，使用Free 的简单模式匹配函数如下所示 -

-- Pattern match Free
matchFree
  :: (a -> r)
  -> (f (Free f a) -> r)
  -> Free f a
  -> r
matchFree kp _ (Pure a) = kp a
matchFree _ kf (Free f) = kf f

我可以通过与Free 相互转换，轻松地将其转换为使用F 的函数-

-- Pattern match F (using toF and fromF)
matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r
matchF kp kf = matchF' . fromF
  where
    matchF' (Pure a) = kp a
    matchF' (Free f) = kf (fmap toF f)

但是，如果不使用 toF 和 fromF，我无法弄清楚如何完成它 -

-- Pattern match F (without using toF)???
-- Doesn't compile
matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r
matchF kp kf f = f kp kf

一定有我遗漏的一般模式。你能帮我弄清楚吗？

Answer 1

您要求提供“您缺少的一般模式”。让我自己尝试解释一下，尽管 Petr Pudlák 的回答也很好。正如 user3237465 所说，我们可以使用两种编码，Church 和 Scott，而您使用的是 Scott 而不是 Church。所以这里是一般评论。

编码的工作原理

通过继续传递，我们可以通过一些独特的类型函数来描述x 类型的任何值

data Identity x = Id { runId :: x } 
{- ~ - equivalent to - ~ -} 
newtype IdentityFn x = IdFn { runIdFn ::  forall z. (x -> z) -> z }

这里的“forall”非常重要，它表示该类型将z 作为未指定的参数。双射是Id . ($ id) . runIdFn 从IdentityFn 变为Identity，而IdFn . flip ($) . runId 则相反。等价的出现是因为对于forall z. z 类型基本上没有什么可以做的，没有任何操作是足够通用的。我们可以等价地声明newtype UnitFn = UnitFn { runUnitFn :: forall z. z -> z }只有一个元素，即UnitFn id，这意味着它以类似的方式对应于单元类型data Unit = Unit。

现在，(x, y) -> z 与 x -> y -> z 同构的 currying 观察是继续传递的冰山一角，它允许我们用纯函数表示数据结构，没有数据结构，因为显然类型 @987654334因此@ 等价于forall z. (x -> y -> z) -> z。因此，将两个项目“粘合”在一起与创建这种类型的值相同，只是将纯函数用作“粘合”。

要看到这种等价性，我们只需要处理另外两个属性。

第一个是 sum 类型的构造函数，形式为Either x y -> z。看，Either x y -> z 与

同构

newtype EitherFn x y = EitherFn { runEitherFn :: forall z. (x -> z) -> (y -> z) -> z }

从中我们得到了模式的基本概念：

1. 获取一个未出现在表达式主体中的新类型变量z。
2. 对于数据类型的每个构造函数，创建一个函数类型，它将其所有类型参数作为参数，并返回一个z。调用与构造函数对应的这些“处理程序”。所以(x, y) 的处理程序是(x, y) -> z，我们将其转换为x -> y -> z，Left x | Right y 的处理程序是x -> z 和y -> z。如果没有参数，你可以只取一个值z 作为你的函数，而不是更麻烦的() -> z。
3. 将所有这些处理程序作为参数传递给表达式forall z. Handler1 -> Handler2 -> ... -> HandlerN -> z。
4. 一半的同构基本上只是将构造函数作为所需的处理程序提交；构造函数上的其他模式匹配并应用相应的处理程序。

微妙的缺失

同样，将这些规则应用于各种事物很有趣；例如，如上所述，如果将其应用于data Unit = Unit，您会发现任何单位类型都是标识函数forall z. z -> z，如果将其应用于data Bool = False | True，您会发现逻辑函数forall z. z -> z -> z，其中false = const而true = const id。但是，如果您确实使用它，您会发现仍然缺少一些东西。提示：如果我们看一下

data List x = Nil | Cons x (List x)

我们看到模式应该是这样的：

data ListFn x = ListFn { runListFn :: forall z. z -> (x -> ??? -> z) -> z }

对于一些???。上述规则并没有确定那里的内容。

有两个不错的选择：要么我们充分利用newtype 的强大功能，将ListFn x 放在那里（“Scott”编码），要么我们可以先发制人地使用我们提供的功能来减少它，在这种情况下，它使用我们已经拥有的函数（“Church”编码）变成z。现在，由于已经预先为我们执行了递归，因此 Church 编码仅对 finite 数据结构完全等效； Scott 编码可以处理无限列表等。也很难理解如何以 Church 形式对相互递归进行编码，而 Scott 形式通常更简单一些。

无论如何，Church 编码有点难以思考，但更神奇一些，因为我们可以用一厢情愿的想法来处理它：“假设这个 z 已经是你想要用 @987654363 完成的任何事情@，然后以适当的方式将其与 head list 结合起来。”而这种一厢情愿的想法正是人们难以理解foldr的原因，因为这个双射的一侧正是列表中的foldr。

还有一些其他的问题，比如“如果像Int 或Integer，构造函数的数量很大或无限？”。这个特定问题的答案是使用函数

data IntFn = IntFn { runIntFn :: forall z. (z -> z) -> z -> z }

你问这是什么？好吧，一个聪明的人（Church）发现这是一种将整数表示为重复组合的方法：

zero f x = x
one f x = f x
two f x = f (f x)
{- ~ - increment an `n` to `n + 1` - ~ -}
succ n f = f . n f

其实这个账号m . n是两者的产物。但我之所以提到这一点，是因为插入() 并翻转参数以发现这实际上是forall z. z -> (() -> z -> z) -> z，这是[()] 的列表类型，其值由length 给出并由@ 给出加法并不难987654376@ 和由>> 给出的乘法。

为了提高效率，您可以对 data PosNeg x = Neg x | Zero | Pos x 进行 Church 编码，并使用 [Bool] 的 Church 编码（保持有限！）来形成 PosNeg [Bool] 的 Church 编码，其中每个 [Bool] 隐含地以未声明的 @ 结尾987654382@ 位于最后的最高位，因此[Bool] 表示从 +1 到无穷大的数字。

扩展示例：BinLeaf / BL

还有一个不平凡的例子，我们可以考虑将所有信息存储在叶子中的二叉树，但在内部节点上也包含注释：data BinLeaf a x = Leaf x | Bin a (BinLeaf a x) (BinLeaf a x)。按照 Church 编码的方法，我们这样做：

newtype BL a x = BL { runBL :: forall z. (x -> z) -> (a -> z -> z -> z) -> z}

现在我们用小写字母代替Bin "Hello" (Leaf 3) (Bin "What's up?" (Leaf 4) (Leaf 5)：

BL $ \leaf bin -> bin "Hello" (leaf 3) (bin "What's up?" (leaf 4) (leaf 5)

因此，同构是非常简单的一种方式：binleafFromBL f = runBL f Leaf Bin。对方有case dispatch，不过还不错。

递归数据上的递归算法呢？这就是它变得神奇的地方：Church 编码的foldr 和runBL 在我们到达树本身之前都运行了我们在子树上的任何函数。例如，假设我们要模拟这个函数：

sumAnnotate :: (Num n) => BinLeaf a n -> BinLeaf (n, a) n
sumAnnotate (Leaf n) = Leaf n
sumAnnotate (Bin a x y) = Bin (getn x' + getn y', a) x' y' 
    where x' = sumAnnotate x
          y' = sumAnnotate y
          getn (Leaf n) = n
          getn (Bin (n, _) _ _) = n

我们要做什么？

-- pseudo-constructors for BL a x.
makeLeaf :: x -> BL a x
makeLeaf x = BL $ \leaf _ -> leaf x

makeBin :: a -> BL a x -> BL a x -> BL a x
makeBin a l r = BL $ \leaf bin -> bin a (runBL l leaf bin) (runBL r leaf bin)

-- actual function
sumAnnotate' :: (Num n) => BL a n -> BL n n
sumAnnotate' f = runBL f makeLeaf (\a x y -> makeBin (getn x + getn y, a) x y) where
    getn t = runBL t id (\n _ _ -> n)

我们传入一个函数\a x y -> ... :: (Num n) => a -> BL (n, a) n -> BL (n, a) n -> BL (n, a) n。请注意，这两个“参数”与此处的“输出”类型相同。使用 Church 编码，我们必须像已经成功一样进行编程——这是一种称为“一厢情愿”的学科。

Free monad 的 Church 编码

Free monad 有范式

data Free f x = Pure x | Roll f (Free f x)

我们的 Church 编码程序说这变成了：

newtype Fr f x = Fr {runFr :: forall z. (x -> z) -> (f z -> z) -> z}

你的功能

matchFree p _ (Pure x) = p x
matchFree _ f (Free x) = f x

变得简单

matchFree' p f fr = runFr fr p f

Answer 2

让我描述一个更简单的场景的区别 - 列表。让我们关注如何使用列表：

• catamorphism，本质上意味着我们可以使用来表达它

  foldr :: (a -> r -> r) -> r -> [a] -> r
  

  正如我们所见，折叠函数永远不会得到列表尾部，只会得到处理后的值。

• 通过模式匹配我们可以做更多的事情，特别是我们可以构造一个类型的泛化折叠

  foldrGen :: (a -> [a] -> r) -> r -> [a] -> r
  

  很容易看出，可以使用foldrGen 来表达foldr。但是，由于foldrGen 不是递归的，因此该表达式涉及递归。

• 为了概括这两个概念，我们可以引入

  foldrPara :: (a -> ([a], r) -> r) -> r -> [a] -> r
  

  这给了消费函数更多的权力：尾巴的减少值，以及尾巴本身。显然，这比以前的两个都更通用。这对应于paramorphism，它“吃掉它的论点并保留它”。

但也可以反过来做。尽管超态更普遍，但可以通过在途中重新创建原始结构来使用变态（以一定的开销成本）来表达它们：

foldrPara :: (a -> ([a], r) -> r) -> r -> [a] -> r
foldrPara f z = snd . foldr f' ([], z)
  where
    f' x t@(xs, r) = (x : xs, f x t)

现在 Church-encoded 数据结构对 catamorphism 模式进行编码，对于列表，它是可以使用 foldr 构造的所有内容：

newtype List a = L (forall r . r -> (a -> r -> r) -> r)

nil :: List a
nil = L $ \n _ -> n

cons :: a -> List a -> List a
cons x (L xs) = L $ \n c -> c x (xs n c)

fromL :: List a -> [a]
fromL (L f) = f [] (:)

toL :: [a] -> List a
toL xs = L (\n c -> foldr c n xs)

为了查看子列表，我们采取了相同的方法：在途中重新创建它们：

foldrParaL :: (a -> (List a, r) -> r) -> r -> List a -> r
foldrParaL f z (L l) = snd $ l (nil, z) f'
  where
    f' x t@(xs, r) = (x `cons` xs, f x t)

---

这通常适用于 Church 编码的数据结构，例如编码的 free monad。它们表达变质，即折叠而不看到结构的各个部分，只有递归结果。为了在这个过程中掌握子结构，我们需要在途中重新创建它们。

Answer 3

这有点令人讨厌。这个问题是每个人第一次遇到它时都会遇到的难题的更一般版本：定义编码为 Church 数字的自然数的前身（想想：Nat ~ Free Id ()）。

我已将我的模块拆分为许多中间定义，以突出解决方案的结构。为了方便使用，我还上传了a self-contained gist。

我从没有什么令人兴奋的事情开始：重新定义F，因为我目前没有安装这个包。

{-# LANGUAGE Rank2Types #-}
module MatchFree where

newtype F f a = F { runF :: forall r. (a -> r) -> (f r -> r) -> r }

现在，甚至在考虑模式匹配之前，我们可以从定义通常数据类型的构造函数的对应物开始：

pureF :: a -> F f a
pureF a = F $ const . ($ a)

freeF :: Functor f => f (F f a) -> F f a
freeF f = F $ \ pr fr -> fr $ fmap (\ inner -> runF inner pr fr) f

接下来，我介绍两种类型：Open 和Close。 Close 只是 F 类型，但 Open 对应于观察到 F f a 元素的内容：它是 Either 纯 a 或 f (F f a)。

type Open  f a = Either a (f (F f a))
type Close f a = F f a

正如我的手波描述所暗示的，这两种类型实际上是等价的，我们确实可以编写在它们之间来回转换的函数：

close :: Functor f => Open f a -> Close f a
close = either pureF freeF

open :: Functor f => Close f a -> Open f a
open f = runF f Left (Right . fmap close)

现在，我们可以回到您的问题，操作过程应该非常明确：open F f a，然后根据我们得到的应用 kp 或 kf。它确实有效：

matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r
matchF kp kf = either kp kf . open

回到关于自然数的原始评论：使用 Church 数字实现的前身在自然数的大小上是线性，而我们可以合理地期望简单的案例分析是常数时间。好吧，就像自然数一样，这种案例分析非常昂贵，因为正如在 open 的定义中使用 runF 所示，遍历了整个结构。

Answer 4

你的

matchF
  :: Functor f
  => (a -> r)
  -> (f (F f a) -> r)
  -> F f a
  -> r

看起来像 Scott 编码的 Free monad。 Church 编码的版本只是

matchF
  :: Functor f
  => (a -> r)
  -> (f r -> r)
  -> F f a
  -> r
matchF kp kf f = runF f kp kf

以下是 Church 和 Scott 编码的列表以供比较：

newtype Church a = Church { runChurch :: forall r. (a -> r       -> r) -> r -> r }
newtype Scott  a = Scott  { runScott  :: forall r. (a -> Scott a -> r) -> r -> r }