Page "System F" Paragraph 10

( 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 ; the universal quantifier binding the α corresponds to the Λ binding the alpha in the lambda expression itself.

Also, note that is a convenient shorthand for, but it is not a symbol of System F itself, but rather a " meta-symbol ".

Likewise, and 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.