Source : Free On-Line Dictionary of Computing

polymorphic lambda-calculus
     
        (Or "second order typed lambda-calculus").  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.
     
        (1994-12-16)