摘要
This chapter considers two ways of typing the λ-calculus. Simple types are easy to understand, but are not very expressive. Greater power is obtained by introducing type symbols and their quantification, in System F. Now the Church encodings of data structures can be typed. Also, reduction is strongly normalising.
摘要译文
本章考虑了两种键入λ演算的方法。简单类型易于理解，但不是很有表现力。通过在系统F中引入类型符号及其量化来获得更大的功率。现在可以键入数据结构的教会编码。此外，减少是强烈正常化。
Barry Jay1. Parametric Polymorphism. Pattern Calculus[M].DE: Springer;ComputingReviews, 2009: 67-79