标签: recursion-schemes

我在函数式编程和PLT圈子中多次听到过"enggebras"这个术语,特别是在讨论对象,comonads,镜头等时.谷歌搜索这个术语给出了对这些结构进行数学描述的页面,这对我来说几乎是不可理解的.任何人都可以解释一下代数在编程环境中的意义,它们的意义是什么,以及它们与对象和共同体的关系？

我正在寻找一些非常简单,易于掌握的递归方案和核心运动方案(catamorphisms,anorporphisms,hylomorphisms等)的解释,这些解释不需要跟随大量的链接,或者打开类别理论教科书.我确信我已经无意识地重新设计了许多这些方案,并在编码过程中将它们"应用"在我的头脑中(我相信我们很多人都有),但我不知道(共同)递归方案我是什么使用被称为.(好吧,我撒了谎.我刚刚读了一些这些,这引发了这个问题.但在今天之前,我一无所知.)

我认为这些概念在编程社区中的传播受到了令人生畏的解释和例子的阻碍 - 例如在维基百科上,而且在其他地方.

它们的名字也可能受到阻碍.我认为有一些替代的,较少的数学名称(关于香蕉和带刺铁丝网的东西？)但是我不知道我使用的递归方案的名称是什么.

我认为使用表示简单实际问题的数据类型的示例,而不是抽象数据类型(如二叉树)会有所帮助.

我最终搞清楚了.请参阅我给出的演讲的视频和幻灯片:

• 幻灯片/ PDF

• 视频

原始问题:

在我努力理解通用递归方案(即使用Fix)时,我发现编写各种方案的仅列表版本很有用.它使得理解实际方案变得更加容易(没有额外的开销Fix).

但是,我还没有想出如何定义只列出版本zygo和futu.

以下是我目前的专门定义:

cataL :: (a ->        b -> b) -> b -> [a] -> b
cataL f b (a : as) = f a    (cataL f b as)
cataL _ b []       = b

paraL :: (a -> [a] -> b -> b) -> b -> [a] -> b
paraL f b (a : as) = f a as (paraL f b as)
paraL _ b …

写完这篇文章之后,我决定将我的钱放在我的嘴边,并开始转换我以前使用的项目recursion-schemes.

有问题的数据结构是一个懒惰的kdtree.请查看具有显式和隐式递归的实现.

这主要是一种简单的转换:

data KDTree v a = Node a (Node v a) (Node v a) | Leaf v a

至

data KDTreeF v a f = NodeF a f f | Leaf v a

现在对整个shebang进行基准测试后,我发现该KDTreeF版本比普通版本慢了两倍(在这里找到整个版本).

这只是额外的Fix包装,让我放慢了速度吗？有什么我可以做的吗？

注意事项:

• 目前这是专门为(V3双).
• 这是在变形应用之后的cata-.Hylomorphism不适合kdtrees.
• 我用cata (fmap foo algebra)了好几次.这是好习惯吗？
• 我使用Edwards recursion-schemes包.

编辑1:

这有关系吗？https://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers 是newtype Fix f = Fix …

我正在尝试了解catamorphisms,我已经阅读了维基百科文章以及F#博客上F#主题系列中的第一篇文章.

我理解这是折叠的概括(即,将许多值的结构映射到一个值,包括值列表到另一个列表).我认为折叠列表和折叠树是一个典型的例子.

可以使用LINQ的Aggregate运算符或其他一些更高阶的方法在C#中显示它吗？

在Ed Kmett的recursion-scheme包中,有三个声明:

newtype Fix f = Fix (f (Fix f))

newtype Mu f = Mu (forall a. (f a -> a) -> a)

data Nu f where 
  Nu :: (a -> f a) -> a -> Nu f

这三种数据类型有什么区别？

许多catamorphisms似乎很简单,大多数用自定义函数替换每个数据构造函数,例如

data Bool = False | True
foldBool :: r              -- False constructor
         -> r              -- True constructor
         -> Bool -> r

data Maybe a = Nothing | Just a
foldMaybe :: b             -- Nothing constructor
          -> (a -> b)      -- Just constructor
          -> Maybe a -> b

data List a = Empty | Cons a (List a)
foldList :: b              -- Empty constructor
         -> (a -> b -> b)  -- Cons constructor
         -> List a -> b

但是,对我来说不清楚的是,如果使用相同类型的构造函数,但使用不同的类型参数会发生什么.例如,而不是传递List …

毋庸置疑,Haskell的标准结构

newtype Fix f = Fix { getFix :: f (Fix f) }

cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata f = f . fmap (cata f) . getFix 

太棒了,非常有用.

试图在Agda中定义类似的东西(我只是为了完整起见)

data Fix (f : Set -> Set) : Set where
    mkFix : f (Fix f) -> Fix f

失败,因为f不一定是严格积极的.这是有道理的 - 通过适当选择,我很容易从这种结构中得到一个矛盾.

我的问题是:在Agda编码递归方案有什么希望吗？它完成了吗？需要什么？

根据Bartosz Milewski的文章(一,二),我定义了一个F代数:

(这并不是说我的代码是Bartosz思想的一个确切体现,它仅仅是我对它们的有限理解,而且任何缺陷都是我自己的.)

module Algebra where

data Expr a = Branch [a] | Leaf Int

instance Functor Expr where
    fmap f (Branch xs) = Branch (fmap f xs)
    fmap _ (Leaf   i ) = Leaf    i

newtype Fix a = Fix { unFix :: a (Fix a) }

branch = Fix . Branch
leaf   = Fix . Leaf

-- | This is an example algebra.
evalSum (Branch xs) = sum xs
evalSum (Leaf   i …

我发明了一种递归方案,这种方法是对同态性的推广.折叠具有catamorphism的数据结构时,您无法访问子项,只能访问折叠的子结果:

{-# LANGUAGE DeriveFunctor #-}
import qualified Data.Map as M

newtype Fix f = Fix { unFix :: f (Fix f) }

cata :: Functor f => (f b -> b) -> Fix f -> b
cata phi = self where
    self = phi . fmap (\x -> self x) . unFix

折叠功能phi只能访问self x原始结果,但不能访问原始结果x.所以我添加了一个加入功能:

cataWithSubterm :: Functor f => (Fix f -> c -> b) -> (f b -> c) -> Fix f -> …