System F

System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974). System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974). Whereas simply typed lambda calculus has variables ranging over functions, 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 judgment 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 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 the fragment of second-order intuitionistic logic that uses only universal quantification. 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. The B o o l e a n {displaystyle scriptstyle {mathsf {Boolean}}} type is defined as: ∀ α . α → α → α {displaystyle scriptstyle forall alpha .alpha o alpha o alpha } , where α {displaystyle scriptstyle alpha } is a type variable. This means: B o o l e a n {displaystyle scriptstyle {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 o } to be right-associative.) The following two definitions for the boolean values T {displaystyle scriptstyle mathbf {T} } and F {displaystyle scriptstyle mathbf {F} } are used, extending the definition of Church booleans: (Note that the above two functions require three — not two — parameters. The latter two should be lambda expressions, but the first one should be a type. This fact is reflected in the fact that the type of these expressions is ∀ α . α → α → α {displaystyle scriptstyle forall alpha .alpha o alpha o alpha } ; the universal quantifier binding the α corresponds to the Λ binding the alpha in the lambda expression itself. Also, note that B o o l e a n {displaystyle scriptstyle {mathsf {Boolean}}} is a convenient shorthand for ∀ α . α → α → α {displaystyle scriptstyle forall alpha .alpha o alpha o alpha } , but it is not a symbol of System F itself, but rather a 'meta-symbol'. Likewise, T {displaystyle scriptstyle mathbf {T} } and F {displaystyle scriptstyle mathbf {F} } are also 'meta-symbols', convenient shorthands, of System F 'assemblies' (in the Bourbaki sense); otherwise, if such functions could be named (within System F), then there would be no need for the lambda-expressive apparatus capable of defining functions anonymously.) Then, with these two λ {displaystyle scriptstyle lambda } -terms, we can define some logic operators (which are of type B o o l e a n → B o o l e a n → B o o l e a n {displaystyle scriptstyle {mathsf {Boolean}} ightarrow {mathsf {Boolean}} ightarrow {mathsf {Boolean}}} ):