function type (Rev #1, changes)

Showing changes from revision #0 to #1:
Added | ~~Removed~~ | ~~Chan~~ged

Let $A,B$ be two types. We introduce a type $A \to B$ called the **function type**. The constructors for this type are written as

$(\lambda x . y) : A \to B$

where $x:A$ and $y:B$.

These can be computed (on application) using $\beta$-reduction:

$(\lambda x. y)z \equiv y[x/z]$

which says take $y$ and replace all occurrences of $x$ with $z$.

category: type theory

Revision on October 11, 2018 at 08:50:29 by Ali Caglayan. See the history of this page for a list of all contributions to it.