多态递归的应用

问题描述 投票：8回答：4

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

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

  1. 在“命名问题”中我们希望同时具有（a）快速捕获避免替换和（b）快速alpha等效性检查，还有bound库（更详细的解释here）。在为函数式编程语言编写编译器时，这两个属性都是可取的。

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

我不想要的事情的例子：

  1. 回答显示如何使用多态递归从类别理论中编码X，除非它们演示了编码X如何有利于解决Y符合上述标准的问题。
  2. 小玩具示例，表明你可以用多态递归做X，但你不能没有它。
haskell recursion polymorphism
4个回答
2
投票

这是一个接近我的工作的例子，我认为相当好用：在一种连接语言中，即一种构建在组合函数上的语言，这些函数在一个共享程序状态（如堆栈）上运行，所有函数都是多态的，相对于他们不接触的堆栈，所有递归都是多态递归，而且所有高阶函数也都是更高级别的。例如，这种语言中的map类型可能是：

∀avs。 σ×列表α×（∀tτ×α→τ×β）→σ×列表b

其中×是左边的关联产品类型，左边是堆叠式，右边是价值型，σ和τ是堆叠型变量，α和β是价值型变量。 map可以在任何程序状态σ上调用，只要它有一个αs列表和一个从顶部的αs到βs的函数，如：

"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相同。

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

3
投票

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

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

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

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

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

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

如果一个人想要在这样的树上操作，则需要多态递归。编写计算树高的函数，对CTree Int中的所有数字或通用映射或折叠求和需要多态递归。

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

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

1
投票

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

长话短说，我有一个数据结构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)递归调用自身，因此每个步骤都会增加类型。

0
投票

Haskell Sequence容器使用内部非常规递归数据类型，只能通过多态递归处理

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.