haskell - 使用 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

这看起来可能是某种变态（我使用的是 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：

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.

即，花式对类型。让我们用实际的 pair 类型替换它以使事情更清楚：

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