We often omit $AB$ from $\cdot_{AB}$ and treat $\cdot$ as left-associative.

A partial applicative substructure $A^\#$ of $A^\circ$ consists of $A^\# \subset A$ for each datatype $A \in |A^\circ|$ such that

• if $f \in (A \Rightarrow B)^\#$ and $a \in A^\#$, then $f \cdot a \in B^\#$.

Above $(A^\circ; A^\#)$ is a relative partial applicative structure.

• If $A^\# = A^\circ$, then $(A^\circ; A^\#)$ is full.

A typed partial combinatory algebra is a partial applicative structure satisfying the following conditions

1. For all $A, B \in |A|$, there is a $k_{AB} : A \Rightarrow B \Rightarrow A$ such that $$\forall a.\ k \cdot a \downarrow, \quad \forall a,b.\ k \cdot a \cdot b = a$$
2. For all $A, B, C \in |A|$, there is a $s_{ABC} : (A \Rightarrow B \Rightarrow C) \Rightarrow (A \Rightarrow B) \Rightarrow (A \Rightarrow C)$ such that $$\forall f, g.\ s \cdot f \cdot g \downarrow, \quad \forall f,g,a.\ s \cdot f \cdot g \cdot a \simeq (f \cdot a) \cdot (g \cdot a)$$

Any higher-order model yields an underlying TPCA.