6

各种递归方案归结为特定的实例化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) aandnewtype Mu f = Mu {unMu :: forall b. (f b -> b) -> b}可以看作是余代数和代数中忘记函子的 colimit 和 limit，并且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))
4

2 回答 2

1

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

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

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

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

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

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

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

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

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

在实践中，refold它不仅用作通用数据类型之间的态射，而且如果您有与函子关联的余数据类型的最终s-coalgebra ：Cs

eatC :: C -> ListF Integer C

以及与仿函数相关的数据类型的初始s 代数：Ds

makeD :: ListF Integer D -> D

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

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

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

于 2022-02-06T20:07:53.323 回答
0

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

  • 正如@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

  • 初始代数，如monads和其他概念，发生在两个层面，一个在语言的语义中，另一个在我们编写的程序中显式地发生。例如，的语义是data ListInt = [] | Int * ListInt一个初始代数。并且，在 haskell 中，语义上也是一个最终的余代数。这是你可能听到的“Mu = Nu”，而这个自相矛盾的等式恰好在 haskell 的语义中。Mu这里无关data Mu f = ..。当我们在程序中模拟type ListInt = Fix ListIntF该语义的地方编写时data Fix f = Fix (f (Fix f))也会发生同样的情况，但这本身受制于 Haskell 的语义（实际上，这个（初始代数）与语义相同，并且MuNu并等于两者，因为 haskell 将它们等同）。在某种程度上，通过写作data Mu f = ...，data Nu f = ..我们正在“窃取”（并且必须这样做）haskell 语义的一部分，并将其与我们自己的（正确表达通用 co-coneNu 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 sTwisted(Hask)Haskrefold'sCHasks'Twisted(C)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），而有些态射实际上是函数，即使我们选择了另一个类别。

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

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

于 2022-02-09T19:21:54.053 回答