Higher-Order Computability

A computability model $C$ over a set $T$ of type names consists of

• an indexed family $\vert C \vert = \{ C(\tau) \mid \tau \in T \}$ of sets, called the datatypes of $C$,
• for each $\sigma,\tau\in T$, a set $C[\sigma,\tau]$ of partial functions $f : C(\sigma) \to C(\tau)$, called operations of $C$

such that

1. for each $\tau \in T$, the identity function $id : C(\tau) \to C(\tau)$ is in $C[\tau,\tau]$
2. for any $f \in C[\rho, \sigma]$ and $g \in C[\sigma, \tau]$, the composition $g \circ f \in C[\rho, \tau]$.