给定可遍历的 F 代数,能否在应用代数上使用 catamorphism?

5
我有一个 F 代数(在先前的问题中介绍),我想将一个效应代数施加到它上面。通过不懈的尝试,我设法组合出了一个可行的单子范畴。我想知道它是否可以推广为一个应用函子,如果不能,为什么。
这是我如何定义 Traversable:
instance Traversable Expr where
    traverse f (Branch xs) = fmap Branch $ traverse f xs
    traverse f (Leaf   i ) = pure $ Leaf i

这是单子范畴折叠:

type AlgebraM a f b = a b -> f b

cataM :: (Monad f, Traversable a) => AlgebraM a f b -> Fix a -> f b
cataM f x = f =<< (traverse (cataM f) . unFix $ x)

这是它的工作原理:

λ let printAndReturn x = print x >> pure x
λ cataM (printAndReturn . evalSum) $ branch [branch [leaf 1, leaf 2], leaf 3]
1
2
3
3
6
6

我现在的想法是,我可以像这样重写:

cataA :: (Applicative f, Traversable a) => AlgebraM a f b -> Fix a -> f b
cataA f x = do
    subtree <- traverse (cataA f) . unFix $ x
    value <- f subtree
    return value

不幸的是,这里的value取决于subtree,根据一篇关于应用do-notation的论文所述,在这种情况下,我们无法将其展开为Applicative。看起来没有绕过这个问题的方法;我们需要一个单子从嵌套的深处浮现出来。
这是真的吗?我可以安全地得出结论,只有扁平结构才能仅使用applicative效果进行折叠吗?
1个回答

5

我可以安全地得出这样的结论,只有扁平的结构才能仅使用应用效果进行折叠?

你说得没错!毕竟,“展平嵌套结构”正是将单子变为单子,而不是Applicative只能组合相邻结构的原因。比较两个抽象的(版本)签名:

class Functor f => Applicative f where
    pure :: a -> f a
    (<.>) :: f a -> f b -> f (a, b)

class Applicative m => Monad m where
    join :: m (m a) -> m a
Monad相较于Applicative,增加了将嵌套的m合并为一个m的能力。这就是为什么[]join等同于concat。而Applicative只允许你将之前无关联的f聚合在一起。
自由单子(free monad)的Free构造器包含了一个完整的f,其中装满了Free f;反之,自由应用(free applicative)的Ap构造器只包含一个Ap f,这不是巧合。
data Free f a = Return a | Free (f (Free f a))
data Ap f a where
    Pure :: a -> Ap f a
    Cons :: f a -> Ap f b -> Ap f (a, b)

希望这能让您对为什么您应该期望使用不能折叠树结构有一些直观的认识。
让我们来玩一下“类型网球”,看看它的结果如何。我们想要编写:
cataA :: (Traversable f, Applicative m) => (f a -> m a) -> Fix f -> m a
cataA f (Fix xs) = _

我们有 xs :: f (Fix f) 以及一个涵盖 fTraversable。我的第一反应是使用 traverse 函数遍历 f 来折叠其中的子树:

cataA f (Fix xs) = _ $ traverse (cataA f) xs

现在这个空洞的目标类型是m (f a) -> m a。由于有一个f:: f a -> m a,我们尝试去扩展m,将包含的f转换成相应的形式:
cataA f (Fix xs) = _ $ fmap f $ traverse (cataA f) xs

现在我们有一个目标类型m(m a) -> m a,它是join。因此,你确实需要一个Monad

这是一些非常出色的“类型网球”技能。你能推荐一本更全面、更严谨地处理这些问题的读物吗? - Ignat Insarov
1
@Kindaro 嗯,我不认为我知道哪里能找到一个完整的证明,抱歉。我的说法仅来自于对单子与应用范畴不同之处的广泛了解,而非基于严格的正式基础。你可以尝试写这样一个证明,这可能是通过反证法证明的(“假设 cataA 可以被实现...那么就会出现矛盾”)。 - Benjamin Hodgson

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接