Function Type

type-theory

Definition

Function Type

A function type is a type whose terms are functions from inputs of one type to outputs of another type.

Formally, if ${\tau }_1$ and ${\tau }_2$ are types, then

$${\tau }_1\to {\tau }_2$$

is the type of functions that take an argument of type ${\tau }_1$ and return a result of type ${\tau }_2$.