多态递归的应用

Question

在语言中通过单形化实现多态性的一个限制(仅限于单形化)是，您失去了支持多态递归的能力(例如，请参阅锈蚀-lang #4287)。

在编程语言中支持多态递归的一些令人信服的用例是什么？我一直试图找到使用这种方法的库/概念，到目前为止，我遇到了一个例子：

1. 在“命名问题”中，我们希望(a)快速捕获避免替换，(b)快速α等价检查，有定界库(更详细的解释这里)。在为函数式编程语言编写编译器时，这两个属性都是可取的。

为了防止这个问题过于宽泛，我正在寻找其他程序/库/研究论文，这些程序/库/研究论文展示了多态递归在传统计算机科学问题中的应用，例如那些涉及编写编译器的问题。

我不想找的例子：

1. 答案展示了如何使用多态递归从范畴理论中编码X，除非它们演示了编码X如何有利于解决Y的问题，而Y是符合上述标准的。
2. 小玩具例子，表明你可以做X多态递归，但你不能没有它。

Answer 1

这里有一个与我的工作很接近的例子，我认为很好地概括了这一点:在一种级联语言中，一种构建在一个共享程序状态(如堆栈)上的函数的语言，所有函数对于它们不接触的部分来说都是多态的，所有递归都是多态递归，而且所有高阶函数也都是高级别的。例如，这种语言中的map类型可能是：

∀αβσ。σ×Listα×(∀τ.τ×α→τ×β)→σ×Listβ

其中×是左关联积类型，左边是堆栈类型，右边是值类型，σ和τ是堆栈类型变量，α和β是值类型变量。任何程序状态的map都可以在σ上调用，只要它上面有一个α的列表和一个从α到β的函数，比如：

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

这里存在多态递归，因为map在不同的σ实例化(即不同类型的“堆栈的其余部分”)上递归地调用自己：

-- σ = Bottom × String
"ignored"           [ 1 2 3 ] { succ show } map
"ignored" 1 succ show [ 2 3 ] { succ show } map cons

-- σ = Bottom × String × String
"ignored" "2"           [ 2 3 ] { succ show } map cons
"ignored" "2" 2 succ show [ 3 ] { succ show } map cons cons

-- σ = Bottom × String × String × String
"ignored" "2" "3"           [ 3 ] { succ show } map cons cons
"ignored" "2" "3" 3 succ show [ ] { succ show } map cons cons cons

-- σ = Bottom × String × String × String × String
"ignored" "2" "3" "4" [ ] { succ show } map cons cons cons
"ignored" "2" "3" "4" [ ] cons cons cons
"ignored" "2" "3" [ "4" ] cons cons
"ignored" "2" [ "3" "4" ] cons
"ignored" [ "2" "3" "4" ]

而且map的函数参数需要更高的级别，因为它也是针对不同的堆栈类型(τ的不同实例化)调用的。

为了做到这一点而不需要多态递归，您需要一个额外的堆栈或局部变量，将map的中间结果放置在其中，从而使所有递归调用都发生在同一类型的堆栈上。这对如何将函数语言编译成类型化的组合器机器有意义:使用多态递归，您可以在保持虚拟机简单的同时保持安全性。

它的一般形式是对数据结构的一部分具有多态的递归函数，例如HList的初始元素或多态记录的子集。

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

data Nest a = Nest a (Nest [a]) | Nil

example = Nest 1 $ Nest [1, 2] $ Nest [[1, 2], [3, 4]] Nil

这种类型上的递归函数总是多形性递归的，因为类型参数随每次递归调用而变化。

Haskell需要这类函数的类型签名，但是除了类型之外，递归和多态递归之间没有任何机械上的区别。如果有隐藏多态性的辅助newtype，则可以编写多态定点运算符：

newtype Forall f = Abstract { instantiate :: forall a. f a }

fix' :: forall f. ((forall a. f a) -> (forall a. f a)) -> (forall a. f a)
fix' f = instantiate (fix (\x -> Abstract (f (instantiate x))))

没有所有的包装和展开仪式，这是相同的fix' f = fix f。

这也是多态递归不需要导致函数实例化的原因--即使函数专门用于其值类型参数，它在递归参数中是“完全多态的”，因此它根本不需要操作它，因此只需要一个编译的表示。

Answer 2

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

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

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

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

该类型将防止像((1,2),3)这样的非完整树存储在其中，从而执行不变量。

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

如果想要对这样的树进行操作，则需要多态递归。编写一个函数来计算树的高度，对CTree Int中的所有数字进行求和，或者泛型映射或折叠，都需要多态递归。

现在，需要/需要这样的多形性递归类型并不是很频繁。尽管如此，他们还是很高兴有。

在我个人看来，单形化有一点不令人满意，这不仅是因为它防止了多态递归，还因为它需要为它所使用的每一个类型编译一次多态代码。在Haskell或Java中，使用Maybe Int, Maybe String, Maybe Bool不会导致Maybe-related函数编译三次，并在最终的对象代码中出现三次。在C++中，这会导致对象代码膨胀。但是，在C++中，这确实允许使用更有效的专门化(例如，可以用位向量实现std::vector<bool> )。这进一步使C++的SFINAE等功能。不过，我认为我更喜欢当多态代码编译一次，类型检查一次--之后，它保证类型安全a所有类型。

Answer 3

我可以分享我在我的项目中使用的一个真实的例子。

长话短说，我有一个数据结构TypeRepMap，其中我将类型存储为键，这种类型与相应值的类型相匹配。

为了对我的库进行基准测试，我需要列出1000种类型的列表，以检查lookup在这个数据结构中的工作速度。接下来是多态递归。

为此，我引入了以下数据类型作为类型级自然数：

data Z
data S a

使用这些数据类型，我能够实现构建所需大小的TypeRepMap的函数。

buildBigMap :: forall a . Typeable a 
            => Int 
            -> Proxy a 
            -> TypeRepMap 
            -> TypeRepMap
buildBigMap 1 x = insert x
buildBigMap n x = insert x . buildBigMap (n - 1) (Proxy @(S a))

因此，当我使用大小为buildBigMap的n和Proxy a运行时，它在每一步都用n - 1和Proxy (S a)递归地调用自己，所以类型在每一步上都在增长。