Π-types (Dependent function types)

Definition - “for all”

A dependent function type is the type of functions whose result type depends on the input value. Given a type $A:\mathcal{U}$ and a type family $B:A\to \mathcal{U}$ we construct a type of dependent functions: ${\Pi }_{(x:A)}B(x):\mathcal{U}$

A term of this type is a function $f$, given its input $x:A$, returns a term of $B(x)$ Formally, if $f:{\Pi }_{(x:A)}B(x)$, then for any $a:A$ we will have $f(a):B(a)$

Type family and dependent function type.excalidraw

⚠ Switch to EXCALIDRAW VIEW in the MORE OPTIONS menu of this document. ⚠ You can decompress Drawing data with the command palette: ‘Decompress current Excalidraw file’. For more info check in plugin settings under ‘Saving’

Excalidraw Data

Text Elements

x

A

f

B

Type

Term

Input

Output

Input

Output

dependent function type

type family

dependent function

type of type family

Embedded Files

2ac32adecf2abd035aa737b4ec51d1c26392dca9: ${\Pi }_{(x:A)}B(x)$

a9cda798425d6d416ecaad0c4c7a8490e5c2f038: $A\to \mathcal{U}$

44a822b01e15432d8b149bd8ac88743e96e3aafd: $B(x)$

72c67de3b382f9c9894dc502dc2ae3a6a373f82e: $f(x)$

6e48c148490b97fa98607c2c4420eb8ba2e0f8f3: $\mathcal{U}$

Link to original

Example 1

Suppose we have type $\text{Bool}:\mathcal{U}$ and type family $B:\text{Bool}\to \mathcal{U}$ defined by $B\text{true}=\mathbb{N}$ and $B\text{false}=\text{String}$ a function $f:{\Pi }_{(x:\text{Bool})}B(x)$ will returns a $n:\mathbb{N}$ when given $\text{true}$ and a $s:\text{String}$ when given $\text{false}$.

Example: fmax

we can define a dependent function $fmax:{\Pi }_{(n:\mathbb{N})}Fin(n+1)$ that gives the “largest” element of the resulting type. We can let $fmax(n):\equiv n_{n+1}$. Note that $n_{n+1}:Fin(n+1)$ (see Definition of Fin(n))

Polymorphic

we can also use types as parameters, such constructed dependent functions are polymorphic over a give universe.

Example: id

Let $id:{\Pi }_{(A:\mathcal{U})}A\to A$ $id$ is now a function that accept a type $A$ as input and return type $A\to A$ as output.

we generally call $id(A):A\to A$ as $i{d}_A:A\to A$ using $\lambda$-calculus $i{d}_A:\equiv \lambda (x:A).x$ which gives $id\equiv \lambda (A:\mathcal{U}).\lambda (x:A).x$