参数化

在编程语言理论中，参数化是参数化多态函数所享有的一种抽象的统一性属性，它抓住了一个多态函数的所有实例都以同样的方式行事的直觉。

考虑这个例子，基于一个集合X和从X到自身的函数的类型T(X)=[X→X]。由twiceX(f)=f∘f所给出的高阶函数twiceX:T(X)→T(X)，从直觉上讲是独立于集合X的。所有这样的函数twiceX的家族，以集合X为参数，被称为参数多态函数。我们简单地把这些函数的整个家族写成两次，并把它的类型写成X.T(X)→T(X)。各个函数twiceX被称为多态函数的组件或实例。请注意，所有组件函数两次X的行为方式是相同的，因为它们是由同一规则给出的。从每个T(X)→T(X)中挑选一个任意的函数而得到的其他函数族不会有这样的统一性。它们被称为特设的多态函数。

参数性是两次这样的均匀作用的族所享有的抽象属性，它将它们与特设族区分开来。有了对参数性的充分形式化，就有可能证明类型为参数多态的函数fn，即n的多态教会数字。相比之下，所有特设家族的集合将大得无法成为一个集合。

参数性定理最初是由JohnC.Reynolds提出的，他称之为抽象性定理。在他的论文Theoremsforfree！中，PhilipWadler描述了参数化的一个应用，即根据类型推导出关于参数化多态函数的定理。

参数性是在Haskell编程语言的编译器中实现许多程序转换的基础。由于Haskell的非严格语义，这些转换传统上被认为在Haskell中是正确的。尽管是一种懒惰的编程语言，Haskell确实支持某些原始操作--比如操作符seq--能够实现所谓的选择性严格，允许程序员强制评估某些表达式。在他们的论文《seq存在下的自由定理》中，PatriciaJohann和JanisVoigtlaender表明，由于这些操作的存在，一般的参数化定理对Haskell程序不成立；因此，这些转换一般来说是不健全的。