10

我一直在使用包中的数据Free类型。现在我正在尝试将其转换为使用但不知道如何映射函数。Control.Monad.FreefreeFControl.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

一定有一个我缺少的一般模式。你能帮我弄清楚吗？

4

4 回答 4

10

您要求“您缺少的一般模式”。让我自己尝试解释一下，尽管 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。等价的出现是因为基本上没有人可以对 type 做任何事情forall z. z，没有任何操作是足够普遍的。我们可以等价地声明它newtype UnitFn = UnitFn { runUnitFn :: forall z. z -> z }只有一个元素，即UnitFn id，这意味着它以data Unit = Unit类似的方式对应于单元类型。

现在，(x, y) -> z与_ _ 所以将两个项目“粘合”在一起与创建这种类型的值相同，它只是使用纯函数作为“粘合剂”。x -> y -> zIdentity (x, y)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. 调用与构造函数对应的这些“处理程序”。所以我们curry to的处理程序(x, y)是，而处理程序是和。如果没有参数，你可以只取一个值作为你的函数，而不是更麻烦的.(x, y) -> zx -> y -> zLeft x | Right yx -> zy -> zz() -> z
  3. 将所有这些处理程序作为表达式的参数forall z. Handler1 -> Handler2 -> ... -> HandlerN -> z。
  4. 一半的同构基本上只是将构造函数作为所需的处理程序提交；构造函数上的其他模式匹配并应用相应的处理程序。

微妙的缺失的东西

同样，将这些规则应用于各种事物很有趣；例如，如上所述，如果您将其应用于data Unit = Unit您会发现任何单位类型都是恒等函数forall z. z -> z，并且如果您将其应用于data Bool = False | True您会发现逻辑函数forall z. z -> z -> zwhere false = constwhile 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”编码）。现在，由于已经预先为我们执行了递归，因此 Church 编码仅对有限数据结构完全等效；Scott 编码可以处理无限列表等。也很难理解如何以 Church 形式对相互递归进行编码，而 Scott 形式通常更简单一些。

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

还有一些其他问题，例如“如果，喜欢Intor 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上是两者的产物。()但我之所以提到这一点，是因为插入 a并翻转参数以发现这实际上forall z. z -> (() -> z -> z) -> z是 list 类型并不难[()]，其值由给出，加法length由 给出++，乘法由 给出>>。

为了提高效率，您可以进行 Church 编码data PosNeg x = Neg x | Zero | Pos x并使用 Church 编码（保持它是有限的！）[Bool]来形成 Church 编码，PosNeg [Bool]其中每个[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. 对方有一个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 有范式

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
于 2015-07-14T21:50:38.860 回答
5

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

  • 通过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

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

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

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 编码的数据结构，例如编码的自由单子。它们表达变质，即折叠而不看到结构的各个部分，只有递归结果。为了在这个过程中掌握子结构，我们需要在途中重新创建它们。

于 2015-07-14T21:00:47.140 回答
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 }
于 2015-07-14T20:18:36.947 回答
3

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

我已将模块拆分为许多中间定义以突出解决方案的结构。为了便于使用，我还上传了一个独立的要点。

我从没有什么令人兴奋的事情开始：重新定义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 akpkf

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

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

于 2015-07-14T20:22:02.550 回答