使用catamorphism忘记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

这看起来可能是某种类似的catamorphism(我正在使用Kmett的recursion-schemes包中的定义).

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

我认为上面使用catamorphism重写的内容看起来像这样,但我无法弄清楚要做什么alg来使它成为类型检查.

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

任何有助于弄清楚这是否真的是一个cata/anamorphism,以及为什么它是/不是的一些直觉将非常感激.

Answer 1

forget :: Functor f => Cofree f a -> Fix f
forget = cata (\(_ :< z) -> Fix z)
-- (Control.Comonad.Trans.Cofree.:<)
-- not to be confused with
-- (Control.Comonad.Cofree.:<)

说明

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

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

这里t ~ Cofree f a和for的类型实例BaseCofree给出:

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于更具体a,即Fix f:

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

forget是参数in a和f,所以我们给出的函数cata不能与对a中的任何东西做任何事情,实现剩下的唯一合理的方法f (Fix f) -> Fix f是Fix包装器.

在操作上,Fix是身份,因此(\(_ :< z) -> Fix z)实际上(\(_ :< z) -> z)对应于删除注释的直觉,即对的第一个组成部分(_ :< z).