polymorphic lambda-calculus

You are here: irt.org | FOLDOC | 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 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.

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

(2005-03-07)

Nearby terms: polylithism « Poly/ML « polymorphic « polymorphic lambda-calculus » polymorphism » polynomial » polynomial-time

FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL