如何在范畴论中构建f-代数的规则？

Question

如何在范畴论中构建f-代数的规则？

5

这里有一些针对列表的简单F-algebra。它们与recursion-schemes库中的cata函数一起使用。

import Data.Functor.Foldable

algFilterSmall :: ListF Int [Int] -> [Int]
algFilterSmall Nil = [] 
algFilterSmall (Cons x xs) = if x >= 10 then (x:xs) else xs

algFilterBig :: ListF Int [Int] -> [Int]
algFilterBig Nil = [] 
algFilterBig (Cons x xs) = if x < 100 then (x:xs) else xs

algDouble :: ListF Int [Int] -> [Int]
algDouble Nil = [] 
algDouble (Cons x xs) = 2*x : xs

algTripple :: ListF Int [Int] -> [Int]
algTripple Nil = [] 
algTripple (Cons x xs) = 3*x : xs

现在我正在组合它们：

doubleAndTripple :: [Int] -> [Int]
doubleAndTripple = cata $ algTripple . project . algDouble
-- >>> doubleAndTripple [200,300,20,30,2,3]
-- [1200,1800,120,180,12,18]

doubleAndTriple 的功能正常。这两种代数结构都是“保持结构不变”的，它们不会改变列表的长度，因此 cata 可以将这两种代数结构应用于列表中的每个项目。

下一个是筛选和加倍：

filterAndDouble :: [Int] -> [Int] 
filterAndDouble = cata $ algDouble . project . algFilterBig
-- >>> filterAndDouble [200,300,20,30,2,3]
-- [160,60,4,6]

它不能正常工作。我猜是因为algFilterBig没有保持结构。

现在来看最后一个例子：

filterBoth :: [Int] -> [Int] 
filterBoth = cata $ algFilterSmall . project . algFilterBig 
-- >>> filterBoth [200,300,20,30,2,3]
-- [20,30]

这里的两个代数结构都不是结构保持的，但是这个例子是有效的。

组合f-代数的确切规则是什么？

- Jogger

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Li-yao Xia · Accepted Answer

“结构保持代数”可以被形式化为自然变换（可以在不同的函子之间）。”

inList :: ListF a [a] -> [a]
inList Nil = []
inList (Cons a as) = a : as

ntDouble, ntTriple :: forall a. ListF Int a -> ListF Int a
algDouble = inList . ntDouble
algTriple = inList . ntTriple

那么，对于任何代数f和自然变换n，

cata (f . inList . n) = cata f . cata n

doubleAndTriple示例是f = algTriple和n = ntDouble的一个实例。

这并不容易推广到更大的代数类。

我认为，没有使用范畴论的情况下，可以更容易地看到过滤器的情况，因为filter是半群同态：filter p . filter q = filter (liftA2 (&&) p q)。

我搜索了一般但足够的条件，以便在类似过滤器的代数上有一个“分配律”。缩写一下：afs = algFilterSmall，afb = algFilterBig。我们倒推，找到一个充分的条件：

cata (afs . project . afb) = cata afs . cata afb  -- Equation (0)

按照范畴论的定义，z = cata (afs . project . afb)是这个方程式（一个伪装的可交换图）的唯一解：

z . inList = afs . project . afb . fmap z

用前一个方程的右侧替换z：

cata afs . cata afb . inList = afs . project . afb . fmap (cata afs . cata afb)
-- (1), equivalent to (0)

在左侧，我们将的定义应用为Haskell函数，并使用project . inList = id进行简化；
在右侧，我们应用了一个函子定律fmap (f . g) = fmap f . fmap g。

这样就得到了：

cata afs . afb . fmap (cata afb) = afs . project . afb . fmap (cata afs) . fmap (cata afb)
-- (2), equivalent to (1)

我们“简化”掉最后一个因子fmap（cata afb）（记住我们是倒推的）：

cata afs . afb = afs . project . afb . fmap (cata afs)  -- (3), implies (2)

这是我能想到的最简单的一个。