Definition. Typed partial combinatory algebra (TPCA) [math-Y5YD]

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.