资料来源 : 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)