如何使用免费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

你问过"你缺少的一般模式".让我自己尝试解释它,虽然PetrPudlá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同构的currying观察是x -> y -> z一个持续传递冰山的一角,它允许我们用纯函数表示数据结构,没有数据结构,因为显然类型Identity (x, y)是等价的forall z. (x -> y -> z) -> z.因此,将两个项目"粘合"在一起与创建此类型的值相同,后者仅使用纯函数作为"粘合剂".

要看到这种等价,我们必须处理另外两个属性.

第一种是sum-type构造函数,形式为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("斯科特"编码),要么我们可以使用我们给出的函数预先减少它,在这种情况下它变成了z使用我们已经拥有的功能("教会"编码).现在由于递归已经在我们前面进行,所以Church编码只对有限数据结构完全相同; Scott编码可以处理无限列表等.也很难理解如何在教会形式中编码相互递归,而斯科特形式通常更简单一些.

无论如何,教会编码有点难以思考,但有点神奇,因为我们用一厢情愿的想法接近它:"假设这z已经是你想要完成的任何事情tail list,然后将它与head list适当的结合起来办法." 这种一厢情愿的想法正是人们难以理解的原因foldr,因为这种双射的一方正是foldr列表中的一方.

还有一些其他问题,例如"如果,喜欢Int或者Integer,构造函数的数量是大还是无限？".这个特定问题的答案是使用这些功能

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

这是什么,你问？好吧,一个聪明的人(教会)已经研究出这是一种将整数表示为重复组合的方法:

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和给定的++乘法给出>>.

为了提高效率,你可以教会编码data PosNeg x = Neg x | Zero | Pos x并使用教会编码(保持它有限!)[Bool]来形成教会编码,PosNeg [Bool]其中每个[Bool]隐含地以True最末端的最高位未声明结束,因此[Bool]代表来自的数字+1到无穷大.

一个扩展的例子:BinLeaf/BL

还有一个非常重要的例子,我们可能会考虑二进制树,它将所有信息存储在叶子中,但也包含内部节点上的注释:data BinLeaf a x = Leaf x | Bin a (BinLeaf a x) (BinLeaf a x).按照教会编码的方法,我们做:

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教会编码兼得运行无论我们的功能是在子树之前,我们得到的树木本身.假设我们想要模拟这个函数:

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.请注意,这两个"参数"与"输出"的类型相同.使用教会编码,我们必须编程好像我们已经成功 - 一个称为"一厢情愿"的学科.

教会编码免费monad

自由单子有正常形式

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

我们的教会编码程序说这变为:

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

你的

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

看起来像斯科特编码的自由单子。教会编码的版本只是

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 }

Answer 3

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

• 通过catamorphism,这基本上意味着我们可以使用它来表达它

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

  正如我们所看到的,折叠函数永远不会得到列表尾部,只有它的处理值.

• 通过模式匹配,我们可以做得更多,特别是我们可以构造一个广义的类型折叠

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

  很容易看出一个人可以表达foldr使用foldrGen.但是,由于foldrGen不是递归的,这个表达式涉及递归.

• 为了概括这两个概念,我们可以介绍一下

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

  这使得消耗功能更强大:尾部的减少值以及尾部本身.显然,这比以前的更通用.这对应于一种"吃掉它的论点并保持它" 的同质性.

但也可以反过来做到这一点.尽管paramorphisms更为通用,但它们可以通过重新创建原始结构的方式使用catamorphisms(以一些开销成本)表达:

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)

现在,教会编码的数据结构对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编码的数据结构,类似于编码的自由monad.它们表达了catamorphisms,即折叠而不看结构的部分,只有递归结果.为了在过程中掌握子结构,我们需要在路上重新创建它们.