Home > Electronics Tutorials > Online Computer Terms Dictionary > P

# Online Computer Terms Dictionary - P

## 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

 Discover
 Home Electronic Circuits Electronic Tutorials Engineering Hobby Projects Resources Links Sitemap Disclaimer/T&C