这个描述是否定义了完整的参数多态函数集?
当然不是。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 中类型类的字典传递实现证明,任何依赖临时多态性的定义都可以以系统的、机械的方式转换为使用参数多态性。