时间戳

首页 > 解决方案 > 编程语言中参数化多态函数（不是临时多态）操作的全部空间是多少？

haskell - 编程语言中参数化多态函数（不是临时多态）操作的全部空间是多少？

问题描述

在A Theory of Type Polymorphism in Programming 的第 349 页第 5 段中，米尔纳说，

对我们来说，程序中存在的多态性是原始多态运算符的自然产物，这些运算符似乎存在于每种编程语言中。此类运算符是赋值、函数应用、配对和元组以及列表处理运算符。

此描述是否定义了完整的参数多态函数集（当我们将列表处理运算符扩展为所有递归数据类型的运算符时）？（+, *, ... 需要以一种特殊的风格定义，它们处理的每种类型都有不同的底层实现）。此外，是否有某种形式模式可以将参数多态函数与必须通过重载（即席）定义的函数分开？

标签： haskellpolymorphismparametric-polymorphismtype-theoryadhoc-polymorphism

解决方案

这个描述是否定义了完整的参数多态函数集？

当然不是。Church 告诉我们，参数多态函数的集合是无限丰富的。例如：

type Nat = forall a. (a -> a) -> a -> a

zero :: Nat
zero s z = z

succ :: Nat -> Nat
succ n s z = s (n s z)

one, two, three :: Nat
one = succ zero
two = succ one
three = succ two

所有zero, one, two, 和three都是参数多态函数；它们都是不同的，因为我们可以将它们应用到一些论点上，从而为每个论点提供不同的结果。这只是最简单的递归数据类型之一的Church 编码。其他数据类型的编码也产生了令人难以置信的复杂的其他类型的参数多态函数族......并且存在不对应于任何数据类型的 Church 编码的参数多态函数。

试图写下所有参数多态函数的列表确实是一项无望的任务，类似于（通过Curry-Howard 同构）写下所有数学真理的列表！

此外，是否有某种形式模式可以将参数多态函数与必须通过重载（即席）定义的函数分开？

并不真地。GHC 中类型类的字典传递实现证明，任何依赖临时多态性的定义都可以以系统的、机械的方式转换为使用参数多态性。

推荐阅读