e, 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. theef="module.php?name=Lexikon&file=search&eid=1&query=polymorphic">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)
