System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds. Whereas simply typed lambda calculus has variables ranging over terms, and binders for them, System F additionally has variables ranging over types, and binders for them. As an example, the fact that the identity function can have any type of the form A → A would be formalized in System F as the statement
⊢ Λ α . λ x α . x : ∀ α . α → α {\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }
where α {\displaystyle \alpha } is a type variable. The upper-case Λ {\displaystyle \Lambda } is traditionally used to denote type-level functions, as opposed to the lower-case λ {\displaystyle \lambda } which is used for value-level functions. (The superscripted α {\displaystyle \alpha } means that the bound variable x is of type α {\displaystyle \alpha } ; the expression after the colon is the type of the lambda expression preceding it.) As a term rewriting system, System F is strongly normalizing. However, type inference in System F (without explicit type annotations) is undecidable. Under the Curry–Howard isomorphism, System F corresponds to second-order propositional intuitionistic logic. System F can be seen as part of the lambda cube, together with even more expressive typed lambda calculi, including those with dependent types. According to Girard, the "F" in System F was picked by chance.
Typing rules The typing rules of System F are those of simply typed lambda calculus with the addition of the following:
where σ , τ {\displaystyle \sigma ,\tau } are types, α {\displaystyle \alpha } is a type variable, and α type {\displaystyle \alpha ~{\text{type}}} in the context indicates that α {\displaystyle \alpha } is bound. The first rule is that of application, and the second is that of abstraction.
Logic and predicates The B o o l e a n {\displaystyle {\mathsf {Boolean}}} type is defined as:
∀ α . α → α → α {\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha } , where α {\displaystyle \alpha } is a type variable. This means: B o o l e a n {\displaystyle {\mathsf {Boolean}}} is the type of all functions which take as input a type α and two expressions of type α, and produce as output an expression of type α (note that we consider → {\displaystyle \to } to be right-associative.) The following two definitions for the Boolean values T {\displaystyle \mathbf {T} } and F {\displaystyle \mathbf {F} } are used, extending the definition of Church Booleans:
T = Λ α . λ x α λ y α . x {\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}
F = Λ α . λ x α λ y α . y {\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}
… excerpt ends here. Continue reading the full article.
