`refold :: Functor s => (a -> s a, a) -> (s b -> b) -> b` 作为通用类型之间的态射答案

【问题标题】：`refold :: Functor s => (a -> s a, a) -> (s b -> b) -> b` as a morphism between universal types`refold :: Functor s => (a -> s a, a) -> (s b -> b) -> b` 作为通用类型之间的态射
【发布时间】：2022-02-10 16:55:17
【问题描述】：

各种递归方案归结为refold 的特定实例化

refold :: Functor s => (s b -> b) -> (a -> s a) -> a -> b
refold f g = go where go a = f (fmap go (g a))

refold 的有意义的解释是什么？

数据类型data Nu f = forall a. Nu (a -> f a) a 和newtype Mu f = Mu {unMu :: forall b. (f b -> b) -> b} 可以看作是余数和代数中遗忘函子的余限和极限，而refold 是它们之间的态射，但它是否阐明了refold？

refold\' :: forall s. Functor s => Nu s -> Mu s
refold\' (Nu g (a :: a)) = Mu mu where

  mu :: forall b. (s b -> b) -> b
  mu f = go a where

    go :: a -> b
    go a = f (fmap go (g a))

不终止可能在这里扮演一个棘手的角色。考虑f a = Either () a。现在Mu f 是（有限）自然数的类型，而Nu f 还为自然数添加了“无穷大”值。然而，我们有 iso isoNu :: f (Nu f) -> Nu f 和 isoMu :: Mu f -> f (Mu f)，它们给了我们 refold isoNu isoMu :: Nu f -> Mu f。我相信这必须在“无穷大”值上有所不同。
@chi 另一个论点：让我们采用 s = 身份。类型表明它必须发散

标签： haskell functional-programming fold category-theory recursion-schemes

【解决方案1】：

我想这取决于您所说的“有意义的解释”是什么意思。

如果s 是递归数据类型和核心递归余数据类型的基本函子，例如递归列表数据类型[e] 的以下函子s ~ ListF e（在Haskell 中，它也是核心递归流余数据类型）：

{-# LANGUAGE DeriveFunctor #-}
data ListF e b = Nil | Cons e b deriving (Show, Functor)

那么s-coalgebra 类型为a -> s a 和一个起始种子a 可以通过从该种子展开生成一个余数据类型[e] 的值，而s-algebra 类型为s b -> b 可以消耗数据类型为[e] 的值通过折叠成b 类型的值。 refold 函数只是结合了从 a 展开和折叠到 b 的操作，而没有实际创建中间 codata/data 类型。

例如，您可以通过使用起始值/余代数对 (a,g) 从 Integer 种子展开来生成（有限）余数据流 [10,9..1]，如下所示：

a :: Integer
a = 10

g :: Integer -> (ListF Integer) Integer
g 0 = Nil
g n = Cons n (n-1)

并折叠列表以使用代数计算其Int 长度：

f :: (ListF Integer) Int -> Int
f Nil = 0
f (Cons _ b) = 1 + b

refold 函数只是结合了这些操作：

main = print $ refold f g a

在这种特殊情况下，它计算流/列表[1..10] 的长度10，而不实际创建任何中间流/列表。

我猜直觉是，如果可以将操作想象为应用于同一仿函数 F 的 F-corecursion 的 F-recursion，那么它就是 refold。或者，也许更实际地，如果一个算法有一个与函子 F 匹配的内部递归结构，它可以表示为refold。 recursion-schemes 中的 refold 的 documentation 给出了快速排序的示例，该示例具有与二叉树匹配的递归结构，尽管您可能已经看过该示例。

注意：下面的内容是错误的或充其量是不精确的，但我会尝试多考虑一下。

~~在实践中，refold 不仅用作通用数据类型之间的态射，而且如果你有一个最后与函子 s 关联的余数据类型 C 的 s-coalgebra：~~

eatC :: C -> ListF Integer C

和最初的数据类型 D 的 s 代数也与函子 s 相关联：

makeD :: ListF Integer D -> D

那么refold makeD eatC 应该是从余数据类型C 到数据类型D 的自然态射。也就是说，它应该是满足的唯一态射：

fmap h . refold makeD eatC = refold makeD eatC . fmap h

我不确定这方面是否非常有趣......

【讨论】：

【解决方案2】：

一些评论（我认为这是有效的 - 不要犹豫纠正 - 我不是语义专家）：

不终止允许写任何东西，正如@chi 建议的那样。以s 为恒等函子，refold 读取为refold :: (b -> b) -> (a -> a) -> a -> b，这显然是一个悖论。因此，对于要“逻辑地”阅读的任何 haskell 类型，我们可能需要隐藏的附带条件。

我们甚至不需要递归来遇到悖论/非终止

-- N. P. Mendler. Recursive types and type constraints in second-order lambda calculus. In LICS, pages 30–36. IEEE Computer Society, 1987
data T a = C (T a -> ())

p :: T a -> (T a ->() )
p (C f) = f

w :: T a -> ()
w x = (p x) x

初始代数，喜欢单子和其他概念，发生在两个层面，一个在语言的语义中，另一个在我们编写的程序中显式地发生。例如语义data ListInt = [] | Int * ListInt 是一个初始代数。并且，在 haskell 中，语义上也是一个最终的余代数。这是你可能听到的“Mu = Nu”，而这个自相矛盾的等式恰好在 haskell 的语义中。 Mu 这里与data Mu f = .. 无关。同样的情况发生在我们写type ListInt = Fix ListIntFdata Fix f = Fix (f (Fix f)) 时模仿我们程序中的那个语义，但这本身受 Haskell 语义的约束（实际上，这个（初始代数）与语义 Mu 和 Nu 相同，并且等于两者，因为 Haskell 等同于它们）。在某种程度上，通过编写data Mu f = ... 和data Nu f = ..，我们正在“窃取”（并且必须这样做）haskell 语义的一部分，并将其与我们自己的（正确表达通用 co-cone Nu f 和通用锥体Mu f），尝试为递归提供嵌入（就像我们使用 HOAS 所做的那样，我们从 Haskell 中窃取绑定）。但我们无法摆脱悖论，因为我们是有义务的偷那个“Mu = Nu”。

这导致了非常有用但非常“不合逻辑”的功能，例如refold
通过编写fold : Functor s => (f a -> a) -> Fix s -> a，我们假装f 的初始代数始终存在，这可能转化为不终止

明确地说，我们可以通过两种不同的方式查看refold。这有点拗口，但我们开始吧：

refold 可以看作是一个合适的函数 refold :: Functor s => (s b -> b) -> (a -> s a) -> a -> b 稍后详述
refold' 可以看作是载体refold' :: forall s. Functor s => Nu s -> Mu s 是Twisted(Hask) 中的代数，其对象是Hask 中的态射。所以refold' 是这个范畴的一个对象，而不是态射。现在，每个类别 C（此处为 Hask）上的函子 s 通过应用于箭头来诱导 Twisted(C) 上的函子 s'。最后是Twisted中的态射
```
             `s' refold' -(out,in)-> refold'`
```
是初始的s' 代数，其中out 是“最终”代数Nu s -> s (Nu s) 和in 是“初始”代数 Mu s -> s (Mu s)

现在的行动功能refold 是，给定一个余代数和一个代数（这里在 Hask 但可能在其他地方），从余数的载体返回唯一态射，然后是 refold'，然后是来自初始代数的唯一态射.这是一个适当的功能这来自在给定组件处选择通用（共）锥体的组件。

这解释了为什么当我们将最终的代数 out 和初始代数 in 输入到 refold 时，我们会返回 refold' 本身。用于组合 refold' 的唯一态射是身份。

有点难以看出是什么，因为我们在Hask 工作，一切都是函数。有些态射实际上是关于我们工作的类别（可能是 Hask 以外的其他东西），有些态射实际上是函数，即使我们选择了另一个类别。

由于不终止，知道什么的解决方案真的是refold 必须忠实于haskell 的语义，并使用完整的偏序（或以某种方式限制s）。

所以我想refold 的真正含义可以从refold' 的真正含义推导出来，这只是一个初始代数，所有标准警告都来自haskell 语义线程。

【讨论】：