λ. The “Curry view” and the “Church view” of polymorphic λ-calculus
- the “Curry view” of polymorphic λ-calculus
- Pure terms of the λ-calculus are assigned type expressions involving universal quantifiers.
- the “Church view” of polymorphic λ-calculus
- Terms and types are defined simultaneously to produce typed term.
という二つの見方があるんだそうな。 Type reconstruction in finite-rank fragments of the polymorphic λ-calculus. より。