Polymorphic lambda-calculus

Computing Dictionary

polymorphic lambda-calculus definition

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)

The Free On-line Dictionary of Computing, © Denis Howe 2010 http://foldoc.org
Cite This Source
Explore Dictionary.com
Previous Definition: polymorphic function
Next Definition: polymorphic reticulosis
More from Thesaurus.com
Synonyms and Antonyms for polymorphic lambda-calculus
More from Reference.com
Search for articles containing polymorphic lambda-calculus
Dictionary.com Word FAQs

Dictionary.com presents 366 FAQs, incorporating some of the frequently asked questions from the past with newer queries.

Copyright © 2014 Dictionary.com, LLC. All rights reserved.
  • Please Login or Sign Up to use the Recent Searches feature