如何为免费Monad使用教堂编码? [英] How do I use the Church encoding for Free Monads?

问题描述

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

I've been using the Free datatype in Control.Monad.Free from the free package. Now I'm trying to convert it to use F in Control.Monad.Free.Church but can't figure out how to map the functions.

例如，使用Free的简单模式匹配功能将如下所示-

For example, a simple pattern matching function using Free would look like this -

-- 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-

-- 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的情况下完成它-

However I can't figure out how to get it done without using toF and 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

我必须缺少一个通用模式.你能帮我弄清楚吗?

There must be a general pattern I am missing. Can you help me figure it out?

推荐答案

您要求输入缺少的通用模式".尽管PetrPudlák的回答也很不错，但让我尝试自己解释一下.正如user3237465所说，我们可以使用两种编码，Church和Scott，而您使用的是Scott，而不是Church.所以这是一般的评论.

You asked for the "general pattern you are missing". Let me give my own attempt at explaining it, though Petr Pudlák's answer is also pretty good. As user3237465 says, there are two encodings that we can use, Church and Scott, and you're using Scott rather than Church. So here's the general review.

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

By continuation passing, we can describe any value of type x by some unique function of type

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.

The "forall" here is very important, it says that this type leaves z as an unspecified parameter. The bijection is that Id . ($ id) . runIdFn goes from IdentityFn to Identity while IdFn . flip ($) . runId goes the other way. The equivalence comes because there is essentially nothing one can do with the type forall z. z, no manipulations are sufficiently universal. We can equivalently state that newtype UnitFn = UnitFn { runUnitFn :: forall z. z -> z } has only one element, namely UnitFn id, which means that it corresponds to the unit type data Unit = Unit in a similar way.

现在，(x, y) -> z与x -> y -> z同构的不断出现的观察是连续传递冰山的一角，它使我们能够用纯函数表示数据结构，而没有数据结构，因为显然等同于forall z. (x -> y -> z) -> z.因此，将两个项目粘合"在一起与创建这种类型的值相同，后者只是将纯函数用作粘合".

Now the currying observation that (x, y) -> z is isomorphic to x -> y -> z is the tip of a continuation-passing iceberg which allows us to represent data structures in terms of pure functions, with no data structures, because clearly the type Identity (x, y) is equivalent therefore to forall z. (x -> y -> z) -> z. So "gluing" together two items is the same as creating a value of this type, which just uses pure functions as "glue".

要看到这种等效性，我们必须处理其他两个属性.

To see this equivalence, we have to just handle two other properties.

第一个是sum-type构造函数，形式为Either x y -> z.可见，Either x y -> z与

The first is sum-type constructors, in the form of Either x y -> z. See, Either x y -> z is isomorphic to

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

从中我们获得了模式的基本概念:

from which we get the basic idea of the pattern:

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. 同构的一半基本上只是将构造函数作为所需的处理程序提供；构造函数上的其他模式匹配并应用相应的处理程序.

1. Take a fresh type variable z that does not appear in the body of the expression.
2. For each constructor of the data type, create a function-type which takes all of its type-arguments as parameters, and returns a z. Call these "handlers" corresponding to the constructors. So the handler for (x, y) is (x, y) -> z which we curry to x -> y -> z, and the handlers for Left x | Right y are x -> z and y -> z. If there are no parameters, you can just take a value z as your function rather than the more cumbersome () -> z.
3. Take all of those handlers as parameters to an expression forall z. Handler1 -> Handler2 -> ... -> HandlerN -> z.
4. One half of the isomorphism is basically just to hand the constructors in as the desired handlers; the other pattern-matches on the constructors and applies the correponding handlers.

微妙的失物

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

Subtle missing things

Again, it's fun to apply these rules to various things; for example as I noted above, if you apply this to data Unit = Unit you find that any unit type is the identity function forall z. z -> z, and if you apply this to data Bool = False | True you find the logic functions forall z. z -> z -> z where false = const while true = const id. But if you do play with it you will notice that something's missing still. Hint: if we look at

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

我们看到该模式应类似于:

we see that the pattern should look like:

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

一些???.上面的规则并没有限制那里发生的事情.

for some ???. The above rules don't pin down what goes there.

有两个不错的选择:我们可以充分利用newtype的功能以将ListFn x放在此处("Scott"编码)，或者可以使用我们提供的功能抢先减少它，在这种情况下，它将使用我们已经拥有的功能(教会"编码)成为z.现在，由于递归已经在我们前面执行，因此Church编码仅完全等同于 finite 数据结构； Scott编码可以处理无限列表等.很难理解如何以Church形式对相互递归进行编码，而Scott形式通常更简单一些.

There are two good options: either we use the power of the newtype to its fullest to put ListFn x there (the "Scott" encoding), or we can preemptively reduce it with the functions we've been given, in which case it becomes a z using the functions that we already have (the "Church" encoding). Now since the recursion is already being performed for us up-front, the Church encoding is only perfectly equivalent for finite data structures; the Scott encoding can handle infinite lists and such. It can also be hard to understand how to encode mutual recursion in the Church form whereas the Scott form is usually a little more straightforward.

无论如何，Church编码有点难以思考，但是却更具魔力，因为我们可以一厢情愿地处理它:假定此z已经是您要使用，然后以适当的方式将其与head list组合."这种一厢情愿的想法正是为什么人们难以理解foldr的原因，因为这种双射的一面恰好是列表的foldr.

Anyway, the Church encoding is a little harder to think about, but a little more magical because we get to approach it with wishful thinking: "assume that this z is already whatever you're trying to accomplish with tail list, then combine it with head list in the appropriate way." And this wishful thinking is precisely why people have trouble understanding foldr, as the one side of this bijection is precisely the foldr of the list.

还有其他一些问题，例如如果像Int或Integer那样，构造函数的数量是大还是无限?该怎么办?".这个特定问题的答案是使用功能

There are some other problems like "what if, like Int or Integer, the number of constructors is big or infinite?". The answer to this particular question is to use the functions

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

这是什么，你问?好吧，一个聪明的人(教会)已经弄清楚，这是一种将整数表示为重复组成的方式:

What is this, you ask? Well, a smart person (Church) has worked out that this is a way to represent integers as the repetition of composition:

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给出，加法由<给出c65>和>>给出的乘法.

Actually on this account m . n is the product of the two. But I mention this because it is not too hard to insert a () and flip arguments around to find that this is actually forall z. z -> (() -> z -> z) -> z which is the list type [()], with values given by length and addition given by ++ and multiplication given by >>.

为了获得更高的效率，您可以使用Church编码data PosNeg x = Neg x | Zero | Pos x并使用[Bool]的Church编码(保持有限！)形成PosNeg [Bool]的Church编码，其中每个[Bool]隐式地以未声明的True末尾的最高有效位，因此[Bool]表示从+1到无穷大的数字.

For greater efficiency, you might Church-encode data PosNeg x = Neg x | Zero | Pos x and use the Church encoding (keeping it finite!) of [Bool] to form the Church encoding of PosNeg [Bool] where each [Bool] implicitly ends with an unstated True at its most-significant bit at the end, so that [Bool] represents the numbers from +1 to infinity.

另一个不平凡的例子，我们可能会考虑二叉树，该树将其所有信息存储在叶子中，但在内部节点上也包含注释:data BinLeaf a x = Leaf x | Bin a (BinLeaf a x) (BinLeaf a x).按照教堂编码的方法，我们要做:

One more nontrivial example, we might think about the binary tree which stores all of its information in leaves, but also contains annotations on the internal nodes: data BinLeaf a x = Leaf x | Bin a (BinLeaf a x) (BinLeaf a x). Following the recipe for Church encoding we do:

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):

Now instead of Bin "Hello" (Leaf 3) (Bin "What's up?" (Leaf 4) (Leaf 5) we construct instances in lowercase:

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

同构因此是一种非常简单的方法:binleafFromBL f = runBL f Leaf Bin.另一端有案件派遣，但还算不错.

The isomorphism is thus very easy one way: binleafFromBL f = runBL f Leaf Bin. The other side has a case dispatch, but is not too bad.

关于递归数据的递归算法呢?这就是神奇的地方:在到达树本身之前，Church编码的foldr和runBL都可以运行子树上的所有功能.例如，假设我们要模拟此功能:

What about recursive algorithms on the recursive data? This is where it gets magical: foldr and runBL of Church encoding have both run whatever our functions were on the subtrees before we get to the trees themselves. Suppose for example that we want to emulate this function:

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编码，我们必须像已经成功一样进行编程 –一种叫做如意算盘"的学科.

We pass in a function \a x y -> ... :: (Num n) => a -> BL (n, a) n -> BL (n, a) n -> BL (n, a) n. Notice that the two "arguments" are of the same type as the "output" here. With Church encoding, we have to program as if we've already succeeded -- a discipline called "wishful thinking".

免费monad具有正常形式

The Free monad has normal form

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

我们的教堂编码程序说，它变成:

and our Church encoding procedure says that this becomes:

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

这篇关于如何为免费Monad使用教堂编码?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！