(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.

< Previous Terms |
Terms Containing polymorphic lambda-calculus |
Next Terms > |

polygon pusher POLYGOTH polylithism Poly/ML polymorphic |
polymorphic lambda-calculus PPLambda System F |
polymorphism polynomial polynomial-time polynomial-time algorithm polyvinyl chloride |

WeWork Office Space & Coworking

Address: 115 Broadway, New York, NY 10006

Hours: Opens 9AM - 6PM

Phone: +1 646-396-3519

shape

shape