使用变形术忘记 Cofree 注释

Question

我有一个 AST，正在使用

Cofree

:

进行注释

data ExprF a
  = Const Int
  | Add a
        a
  | Mul a
        a
  deriving (Show, Eq, Functor)

我使用

type Expr = Fix ExprF

代表未标记的 AST，使用

type AnnExpr a = Cofree ExprF a

代表标记的 AST。我找到了一个函数，可以通过丢弃所有注释将标记的 AST 转换为未标记的 AST：

forget :: Functor f => Cofree f a -> Fix f
forget = Fix . fmap uncofree . unwrap

这看起来可能是某种变形（我使用的是 Kmett 的 recursion-schemes 包中的定义）。

cata :: (Base t a -> a) -> t -> a
cata f = c where c = f . fmap c . project

我认为使用变形术重写的上面看起来像这样，但我不知道要为

alg

放置什么来进行类型检查。

forget :: Functor f => Cofree f a -> Fix f
forget = cata alg where
  alg = ???

任何帮助弄清楚这是否真的是卡塔/变形，以及为什么它是/不是的一些直觉将不胜感激。

Answer 1

import Data.Functor.Foldable (cata)
import Control.Comonad.Cofree (Cofree)
import Control.Comonad.Trans.Cofree as CofreeT (CofreeF(..))
import Data.Fix (Fix(..))

forget :: Functor f => Cofree f a -> Fix f
forget = cata (\(_ CofreeT.:< z) -> Fix z)

注意：请小心

Cofree

和

:<

的导入位置。 一个来自

Control.Comonad.Cofree

，另一个来自

Control.Comonad.Trans.Cofree

（作为

CofreeF

数据类型的一部分）。

如果您从

Cofree

导入

....Trans.Cofree

，则

cata

看起来像这样：

import Data.Functor.Identity (Identity(..))
import Data.Functor.Compose (Compose(..))
import Data.Functor.Foldable (cata)
import Control.Comonad.Trans.Cofree as CofreeT (Cofree, CofreeF(..))
import Data.Fix (Fix(..))

forget :: Functor f => Cofree f a -> Fix f
forget = cata (\(Compose (Identity (_ CofreeT.:< z))) -> Fix z)

说明

仅查看类型，我们可以证明实际上只有一种方法来实现

forget

。我们先从

cata

的类型开始：

cata :: Recursive t => (Base t b -> b) -> t -> b

这里

t ~ Cofree f a

和 Base

 的 

type 实例为

Cofree

给出：

type instance Base (Cofree f a) = CofreeF f a

其中

CofreeF

是：

data CoFreeF f a b = a :< f b
-- N.B.: CoFree also defines a (:<) constructor so you have to be
-- careful with imports.

即，一种奇特的配对类型。让我们将其替换为实际的对类型以使事情更清楚：

cata :: Functor f => ((a, f b) -> b) -> Cofree f a -> b

现在我们真正专业化了

cata

，具有更具体的

b

，即

Fix f

：

-- expected type of `cata` in `forget`
cata :: Functor f => ((a, f (Fix f)) -> Fix f) -> Cofree f a -> Fix f

forget

在

a

和

f

中是参数化的，因此我们给出的函数

cata

不能对这对中的

a

做任何事情，而实现剩余

f (Fix f) -> Fix f

的唯一合理方法是

 Fix

包装纸。

在操作上，

Fix

是恒等式，因此

(\(_ :< z) -> Fix z)

实际上是

(\(_ :< z) -> z)

，这对应于删除注释的直觉，即

(_ :< z)

对的第一个组成部分。