Let be two types. We introduce a type called the function type. The constructors for this type are written as
where and .
These can be computed (on application) using -reduction:
which says take and replace all occurrences of with for an .
Given any type , there is a function called the identity function of denoted and defined by
Given any types and two functions , the composition of and is the function
Revision on January 19, 2019 at 15:22:54 by Ali Caglayan. See the history of this page for a list of all contributions to it.