haskell - 我如何为 Free Monads 使用 Church 编码？

Question

我一直在使用 Free Control.Monad.Free 中的数据类型来自 free包裹。现在我正在尝试将其转换为使用 F在 Control.Monad.Free.Church但无法弄清楚如何映射函数。

例如，一个简单的模式匹配函数使用 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

我可以轻松地将其转换为使用 F 的函数通过转换为/从 Free ——

-- 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以类似的方式。

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

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

第一个是和型构造函数，形式为 Either x y -> z .见， Either x y -> z同构于

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

从中我们可以得到模式的基本思想:

取一个新鲜类型变量z没有出现在表达式的主体中。

对于数据类型的每个构造函数，创建一个函数类型，它将所有类型参数作为参数，并返回 z .调用这些与构造函数相对应的“处理程序”。所以 (x, y) 的处理程序是 (x, y) -> z我们 curry 到 x -> y -> z ，以及 Left x | Right y 的处理程序是 x -> z和 y -> z .如果没有参数，你可以只取一个值 z作为你的函数而不是更麻烦的() -> z .

将所有这些处理程序作为参数传递给表达式 forall z. Handler1 -> Handler2 -> ... -> HandlerN -> z .

一半的同构基本上只是将构造函数作为所需的处理程序；其他模式匹配构造函数并应用相应的处理程序。

微妙的缺失

同样，将这些规则应用于各种事物很有趣；例如，正如我上面提到的，如果您将此应用于 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”编码)，或者我们可以用我们已经给出的函数抢先减少它，在这种情况下它变成 z使用我们已有的功能(“教堂”编码)。现在因为递归已经为我们预先执行了，Church 编码只对有限数据结构完全等效； Scott 编码可以处理无限列表等。也可能很难理解如何在 Church 形式中对相互递归进行编码，而 Scott 形式通常更简单一些。

无论如何，Church 编码有点难以思考，但更神奇，因为我们可以一厢情愿地接近它:“假设这个 z 已经是你试图用 tail list 完成的任何事情，那么以适当的方式将其与 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 给出和由 ++ 给出的加法和由 >> 给出的乘法.

为了提高效率，您可以使用 Church-encode data PosNeg x = Neg x | Zero | Pos x并使用 [Bool] 的 Church 编码(保持有限!)形成 PosNeg [Bool]的Church编码凡 [Bool]以未说明的 True 隐式结束在最后的最高有效位，所以 [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 .对方有案发，但也不算太差。

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

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 .请注意，这里的两个“参数”与“输出”的类型相同。使用教堂编码， 我们必须像已经成功一样进行编程 ——一门学科，叫做“一厢情愿”。

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