日々の流転

λ. 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. より。