System F

polymorphic lambda-calculus
System F

   <language, types> (Or "second order typed lambda-calculus",
   "System F", "Lambda-2").  An extension of {typed
   lambda-calculus} allowing functions which take types as
   parameters.  E.g. the {polymorphic} function "twice" may be
   written:

    	twice = /\ t . \  (f :: t -> t) . \ (x :: t) . f (f x)

   (where "/\" is an upper case Greek lambda and "(v :: T)" is
   usually written as v with subscript T).  The parameter t will
   be bound to the type to which twice is applied, e.g.:

   	twice Int

   takes and returns a function of type Int -> Int.  (Actual type
   arguments are often written in square brackets [ ]).  Function
   twice itself has a higher type:

   	twice :: Delta t . (t -> t) -> (t -> t)

   (where Delta is an upper case Greek delta).  Thus /\
   introduces an object which is a function of a type and Delta
   introduces a type which is a function of a type.

   Polymorphic lambda-calculus was invented by Jean-Yves Girard
   in 1971 and independently by John C. Reynolds in 1974.

   ["Proofs and Types", J-Y. Girard, Cambridge U Press 1989].

   (2005-03-07)