polymorphic lambdacalculus
<language, types> (Or "second order typed lambdacalculus", "System F",
"Lambda2"). An extension of typed lambdacalculus 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 lambdacalculus was invented by JeanYves Girard in 1971 and
independently by John C. Reynolds in 1974.
["Proofs and Types", JY. Girard, Cambridge U Press 1989].
(20050307)
Nearby terms:
polylithism « Poly/ML « polymorphic « polymorphic
lambdacalculus » polymorphism » polynomial »
polynomialtime
