回顾
上文我们介绍了let多态，
将let表达式，看做了的简写，
即，把中出现的所有，都用替换掉，因此这些副本可以具有不同的类型。
本文将介绍另外一种多态形式，称为参数化多态（parametric polymorphism），例如，
1 | data Maybe a = Nothing | Just a |
以上Haskell代码，定义了一个Maybe a类型，
其中Maybe称为类型构造器（type constructor），a是它的参数。
Maybe不是一个合法的类型，它只有和某个具体的a放在一起，才是一个合法的类型，
例如，Maybe Int，Maybe Char。
System F
为了实现参数化多态，我们需要对简单类型化演算（系统）进行扩展，
在中，我们用来表示抽象（lambda abstraction），
而使用来表示应用（lambda application）。
现在我们引入一种新的抽象形式，，它的参数是一个类型，称为类型抽象，
再引入一种新的应用形式，，称为类型实例化，其中是一个类型表达式。
求值规则如下，
例如，我们可以这样定义一个多态函数，
当把它应用于类型时，
，它为类型上的恒等函数。
而把它应用于类型时，
，它为类型上的恒等函数，
可见，的具体类型，依赖于它的类型参数。
它应用于任意一个类型，都会得到一个类型为的函数，
因此，人们通常将的类型记为。
类型规则如下，
（1）
（2）
其中，类型，叫做全称类型（universal type），
称为全称量词（universal quantifier），
引入了全称类型之后得到的系统，称为System F。
Rank-N Types
有了全称类型之后，函数的参数类型和返回值类型，都有可能具有全称类型。
不难看出，函数返回值类型的全称量词，总是可以提取出来，放到最外面，
但是参数类型的全称量词，不能提取出来。
例如，，相当于，
而，与则不同。
不包含全称量词的类型表达式，具有rank-0类型，也称为单态类型（monotype），
全称量词都可以提取出来类型表达式，具有rank-1类型（rank-1 type），
一个函数类型，它的入参具有rank-n类型，那么该函数就具有rank-(n+1)类型。
例如，
，具有rank-3类型，
，具有rank-1类型。
System F的功能是很强大的，但是不幸的是，
人们发现，该系统中的类型推导算法是不可判定的。
例如，一般而言，一个rank-3及其以上rank-N类型的表达式，其类型是不可确定的，
为了确定它的类型，人们不得不手工加上必要的类型信息。
Haskell采用了Hindley–Milner类型系统，
它是System F的一个子集，其中包含了可判定的类型推导算法。
在Haskell中，类型参量（type variable）默认具有全称类型（universally quantified），
例如，a -> a，实际上表示类型，
a -> a可看做(->) a a类型，其中->为函数类型构造器。
非直谓性
在数学和逻辑学中，一个定义称为非直谓的（impredicative），
指的是它包含了自引用（self-reference）。
例如，在定义一个集合的时候，用到了正在定义的这个集合。
罗素悖论就是用非直谓的方式构造出来的，
如果我们定义，那么。
非直谓定义并不一定导致矛盾，有些情况下还是有用的，
例如，我们可以非直谓的定义，集合中的最小元素为，，。
具有参数化多态的类型表达式，
也有直谓（predicative）和非直谓（impredicative）之分。
如果它可以用一个多态类型实例化，例如用它自己来实例化，
就称为非直谓多态类型（impredicative polymorphism）。
反之，如果一个多态类型表达式，只能用单态类型实例化，
就称它具有直谓多态类型（predicative_polymorphism）。
单态限制
1 | f x = let g y z = ([x,y], z) |
假设x的类型为a，那么g的类型只能为a -> b -> ([a], b)，
其中，由于列表类型的限制，x和y必须具有相同的类型。
此时，只有b可以具有全称量词，即，
因为a在类型上下文中，已经出现了，不能再被实例化为其他的类型了。
我们称，g的第一个参数a具有单态性（monomorphism）。
例如，(g True, g 'c')不是良类型的，
而(g True, g False)是良类型的。
值得一提的是，显式的给g注明类型，也不能阻止a的单态行为，
1 | f x = let |
此时，a仍然是单态的。
如果一个类型变量，不在类型上下文中出现，它就可以被全称化（generalize）。
但是Haskell考虑到性能和模块间的类型推导，
还增加了特殊的单态限制（monomorphism restriction）避免全称化。
Rule 1
在一组相互依赖的声明中，满足以下两个条件，其中的类型变量才会被全称化，
（1）每一个变量，都被函数或模式匹配所绑定，
（2）被模式匹配绑定的变量，都有显式的类型签名。
Rule 2
导入到其他模块（module）的单态类型变量，被认为是有歧义的（ambiguous），
类型通过其来源模块内的default声明来决定。
1 | module M1(len1) where |
当模块M1的类型推导结束后，根据Rule 1，len1具有单态类型，len1 :: Num a => a，
Rule 2表明，类型变量a具有歧义性，必须使用default声明来解决歧义。
因此，根据default( Int, Double )，len1得到了类型Int，
不过，M2中对len1 :: Int的使用导致了类型错误。
参考
Types and programming languages
Glasgow Haskell Compiler User's Guide