polymorphic lambda-calculus

polymorphic lambda-calculus

(language, types)(Or "second order typed lambda-calculus","System F", "Lambda-2"). An extension of typed lambda-calculus allowing functions which take types asparameters. E.g. the polymorphic function "twice" may bewritten:

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

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

twice Int

takes and returns a function of type Int -> Int. (Actual typearguments are often written in square brackets [ ]). Functiontwice 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 Deltaintroduces a type which is a function of a type.

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

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