多态递归的应用

Question

通过单态化(仅单态化)在语言中实现多态性的一个限制是你失去了支持多态递归的能力(例如参见rust-lang #4287).

有哪些引人注目的用例支持编程语言中的多态递归？我一直在努力寻找使用它的库/概念,到目前为止我遇到过一个例子:

1. 在"命名问题"中,我们希望同时具有(a)快速捕获避免替换和(b)快速alpha等价检查,还有绑定库(此处有更详细的解释).在为函数式编程语言编写编译器时,这两个属性都是可取的.

为了防止这个问题过于宽泛,我正在寻找其他程序/图书馆/研究论文,它们将多态递归的应用呈现给传统的计算机科学问题,例如那些编写编译器的问题.

我不想要的事情的例子:

1. 回答显示如何使用多态递归从类别理论中编码X,除非它们演示了编码X如何有利于解决Y符合上述标准的问题.

2. 小玩具示例,表明你可以用多态递归做X,但你不能没有它.

Answer 1

有时您希望在类型中编码一些约束，以便在编译时强制执行它们。

例如，一个完整的二叉树可以定义为

data CTree a = Tree a | Dup (CTree (a,a))

example :: CTree Int
example = Dup . Dup . Tree $ ((1,2),(3,4))

该类型将防止将不完整的树((1,2),3)存储在内部，从而强制执行不变量。

Okasaki 的书展示了许多这样的例子。

如果然后想要对这样的树进行操作，则需要多态递归。编写一个计算树的高度、对 a 中的所有数字求和的函数CTree Int，或者一个通用的 map 或 fold 需要多态递归。

现在，需要/想要这种多态递归类型并不是非常频繁。不过，他们很高兴。

在我个人看来，单态化有点不令人满意，不仅因为它阻止了多态递归，还因为它需要为使用它的每种类型编译一次多态代码。在 Haskell 或 Java 中， usingMaybe Int, Maybe String, Maybe Bool不会导致Maybe-related 函数被编译三次并在最终目标代码中出现三次。在 C++ 中，会发生这种情况，使目标代码膨胀。但是，确实，在 C++ 中，这允许使用更有效的特化（例如，std::vector<bool>可以用位向量实现）。这进一步启用了 C++ 的 SFINAE 等。不过，我认为我更喜欢多态代码编译一次并进行一次类型检查 - 之后保证所有类型都是类型安全的。

Answer 2

Here\xe2\x80\x99s 是一个与我的工作接近的示例，我认为它概括得相当好：在连接语言中，即一种基于组合函数构建的语言，这些函数在共享程序状态（例如堆栈）上运行，所有函数都是多态的对于它们不接触的堆栈部分，所有递归都是多态递归，而且所有高阶函数也是更高阶的。例如，类型map例如，这种语言中

\n\n

\n

\xe2\x88\x80\xce\xb1\xce\xb2\xcf\x83。\xcf\x83 \xc3\x97 列表 \xce\xb1 \xc3\x97 (\xe2\x88\x80\xcf\x84.\xcf\x84 \xc3\x97 \xce\xb1 \xe2\x86\x92 \xcf\ x84 \xc3\x97 \xce\xb2) \xe2\x86\x92 \xcf\x83 \xc3\x97 列表 \xce\xb2

\n

\n\n

其中 \xc3\x97 是左关联乘积类型，左侧是堆栈类型，右侧是值类型，\xcf\x83 和 \xcf\x84 是堆栈类型变量，\xce \xb1 和 \xce\xb2 是值类型变量。map可以在任何程序状态 \xcf\x83 上调用，只要它有一个 \xce\xb1s 列表和顶部从 \xce\xb1s 到 \xce\xb2s 的函数，例如：

\n\n

"ignored" [ 1 2 3 ] { succ show } map\n=\n"ignored" [ "2" "3" "4" ]\n

\n\n

这里存在\xe2\x80\x99s多态递归，因为map在\xcf\x83的不同实例上递归地调用自身（即堆栈\xe2\x80\x9d的\xe2\x80\x9crest的不同类型）：

\n\n

-- \xcf\x83 = Bottom \xc3\x97 String\n"ignored"           [ 1 2 3 ] { succ show } map\n"ignored" 1 succ show [ 2 3 ] { succ show } map cons\n\n-- \xcf\x83 = Bottom \xc3\x97 String \xc3\x97 String\n"ignored" "2"           [ 2 3 ] { succ show } map cons\n"ignored" "2" 2 succ show [ 3 ] { succ show } map cons cons\n\n-- \xcf\x83 = Bottom \xc3\x97 String \xc3\x97 String \xc3\x97 String\n"ignored" "2" "3"           [ 3 ] { succ show } map cons cons\n"ignored" "2" "3" 3 succ show [ ] { succ show } map cons cons cons\n\n-- \xcf\x83 = Bottom \xc3\x97 String \xc3\x97 String \xc3\x97 String \xc3\x97 String\n"ignored" "2" "3" "4" [ ] { succ show } map cons cons cons\n"ignored" "2" "3" "4" [ ] cons cons cons\n"ignored" "2" "3" [ "4" ] cons cons\n"ignored" "2" [ "3" "4" ] cons\n"ignored" [ "2" "3" "4" ]\n

\n\n

以及函数论证map需要更高的等级，因为它\xe2\x80\x99 也调用不同的堆栈类型（\xcf\x84 的不同实例）。

\n\n

为了在没有多态递归的情况下做到这一点，您需要一个额外的堆栈或局部变量来放置中间结果map获取 \xe2\x80\x9cout 的方式 \xe2\x80\x9d ，以便所有递归调用都进行放置在相同类型的堆栈上。这对于如何将函数式语言编译为类型化组合器机器具有影响：通过多态递归，您可以在保持虚拟机简单的同时保持安全性。

\n\n

其一般形式是，您有一个递归函数，该函数在数据结构的一部分上是多态的，例如一个数据结构的初始元素HList或多态记录的子集。

\n\n

正如 @chi 已经提到的，在 Haskell 中，您在函数级别需要多态递归的主要实例是当您在类型上具有多态递归时具有多态递归，例如：

\n\n

data Nest a = Nest a (Nest [a]) | Nil\n\nexample = Nest 1 $ Nest [1, 2] $ Nest [[1, 2], [3, 4]] Nil\n

\n\n

这种类型的递归函数始终是多态递归的，因为类型参数随着每次递归调用而变化。

\n\n

Haskell 需要此类函数的类型签名，但除了类型之外，机械上\xe2\x80\x99s 递归和多态递归之间没有区别。如果您有辅助定点运算符，则可以编写多态定点运算符newtype定点运算符：

\n\n

newtype Forall f = Abstract { instantiate :: forall a. f a }\n\nfix\' :: forall f. ((forall a. f a) -> (forall a. f a)) -> (forall a. f a)\nfix\' f = instantiate (fix (\\x -> Abstract (f (instantiate x))))\n

\n\n

没有所有的包装和拆包仪式，这与fix\' f = fix f。

\n\n

这也是多态递归不需要导致函数实例化爆炸的原因\xe2\x80\x94即使该函数专用于其值类型参数，它\xe2\x80 \x99s \xe2\x80\x9c 递归参数中的 \xe2\x80\x9d 完全多态，因此它根本不\xe2\x80\x99t 操作它，因此只需要单个编译表示。

\n