Type Inference

$$ \newcommand{\RR}{\mathbb{R}} \newcommand{\GG}{\mathbb{G}} \newcommand{\PP}{\mathbb{P}} \newcommand{\PS}{\mathcal{P}} \newcommand{\SS}{\mathbb{S}} \newcommand{\NN}{\mathbb{N}} \newcommand{\ZZ}{\mathbb{Z}} \newcommand{\CC}{\mathbb{C}} \newcommand{\HH}{\mathbb{H}} \newcommand{\ones}{\mathbb{1\hspace{-0.4em}1}} \newcommand{\alg}[1]{\mathfrak{#1}} \newcommand{\mat}[1]{ \begin{pmatrix} #1 \end{pmatrix} } \renewcommand{\bar}{\overline} \renewcommand{\hat}{\widehat} \renewcommand{\tilde}{\widetilde} \newcommand{\inv}[1]{ {#1}^{-1} } \newcommand{\eqdef}{\overset{\text{def}}=} \newcommand{\block}[1]{\left(#1\right)} \newcommand{\set}[1]{\left\{#1\right\}} \newcommand{\abs}[1]{\left|#1\right|} \newcommand{\trace}[1]{\mathrm{tr}\block{#1}} \newcommand{\norm}[1]{ \left\| #1 \right\| } \newcommand{\argmin}[1]{ \underset{#1}{\mathrm{argmin}} } \newcommand{\argmax}[1]{ \underset{#1}{\mathrm{argmax}} } \newcommand{\st}{\ \mathrm{s.t.}\ } \newcommand{\sign}[1]{\mathrm{sign}\block{#1}} \newcommand{\half}{\frac{1}{2}} \newcommand{\inner}[1]{\langle #1 \rangle} \newcommand{\dd}{\mathrm{d}} \newcommand{\ddd}[2]{\frac{\partial #1}{\partial #2} } \newcommand{\db}{\dd^b} \newcommand{\ds}{\dd^s} \newcommand{\dL}{\dd_L} \newcommand{\dR}{\dd_R} \newcommand{\Ad}{\mathrm{Ad}} \newcommand{\ad}{\mathrm{ad}} \newcommand{\LL}{\mathcal{L}} \newcommand{\Krylov}{\mathcal{K}} \newcommand{\Span}[1]{\mathrm{Span}\block{#1}} \newcommand{\diag}{\mathrm{diag}} \newcommand{\tr}{\mathrm{tr}} \newcommand{\sinc}{\mathrm{sinc}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\Ob}[1]{\mathrm{Ob}\block{\cat{#1}}} \newcommand{\Hom}[1]{\mathrm{Hom}\block{\cat{#1}}} \newcommand{\op}[1]{\cat{#1}^{op}} \newcommand{\hom}[2]{\cat{#1}\block{#2}} \newcommand{\id}{\mathrm{id}} \newcommand{\Set}{\mathbb{Set}} \newcommand{\Cat}{\mathbb{Cat}} \newcommand{\Hask}{\mathbb{Hask}} \newcommand{\lim}{\mathrm{lim}\ } \newcommand{\funcat}[1]{\left[\cat{#1}\right]} \newcommand{\natsq}[6]{ \begin{matrix} & #2\block{#4} & \overset{#2\block{#6}}\longrightarrow & #2\block{#5} & \\ {#1}_{#4} \hspace{-1.5em} &\downarrow & & \downarrow & \hspace{-1.5em} {#1}_{#5}\\ & #3\block{#4} & \underset{#3\block{#6}}\longrightarrow & #3\block{#5} & \\ \end{matrix} } \newcommand{\comtri}[6]{ \begin{matrix} #1 & \overset{#4}\longrightarrow & #2 & \\ #6 \hspace{-1em} & \searrow & \downarrow & \hspace{-1em} #5 \\ & & #3 & \end{matrix} } \newcommand{\natism}[6]{ \begin{matrix} & #2\block{#4} & \overset{#2\block{#6}}\longrightarrow & #2\block{#5} & \\ {#1}_{#4} \hspace{-1.5em} &\downarrow \uparrow & & \downarrow \uparrow & \hspace{-1.5em} {#1}_{#5}\\ & #3\block{#4} & \underset{#3\block{#6}}\longrightarrow & #3\block{#5} & \\ \end{matrix} } \newcommand{\cone}[1]{\mathcal{#1}} $$

unification

normal form for $\sigma$ types: all quantifiers are bound (appear in the type), ordered by appearance

not entirely clear why this is needed/practical

type variables $\alpha$ unify with $\sigma$ types under standard occurs check

type applications unify as usual

unclear whether higher-kinded types can be easily added
using kind-preserving substitutions should do the trick

unification of $\sigma$ types:

instantiate outer-most quantifiers to the same fresh skolem
unify instantiated types
fail the skolem escape, i.e. if some free type variable $\alpha$ gets unified with it
basically, only $\sigma$ types that are equivalent modulo variable renaming and substitution will unify.

subsumption

$\sigma_1$ is the expected function argument type, $\sigma_2$ is the actual function argment type

$\sigma_2$ should be “at least as polymorphic” as $\sigma_1$, possibly more

roughly: “$\sigma_2$ should have at least all the quantifiers of $\sigma_1$”

expressed as $\sigma_2 \sqsubseteq \sigma_1$

$\sigma_1 = \forall \alpha. \alpha \to \alpha$ and $\sigma_2 = \forall \alpha\beta. \alpha \to \beta$
(forall s. St s a) and (forall s. St s (\forall a. a -> a)

in practice:

skolemize outermost quantifiers and instantiate $\sigma_1$ with them
instantiate $\sigma_2$ with fresh $\alpha$ variables
- these may unify with the skolems, which is fine (quantified in $\sigma_2$)
- actually, skolems in $\sigma_1$ must unify with these variables for unification to succeed
unify instantiated types
check that no skolem escape through other $\alpha$ variables

$\sigma_2$ will get $\sigma_1$ skolems occurring at the same places as in $\sigma_1$ possibly elsewhere too as long unification agrees.

example

$\sigma_1 = \forall s.\mathrm{St}\ s\ a$ and $\sigma_2 = \forall s.\mathrm{St}\ s\ (\forall a.a\to a)$

$\sigma_1$ instantiates $s$ to a skolem $c$, giving $\mathrm{St}\ s\ a$

$\sigma_2$ instantiates $s$ to a fresh type variable $\beta$, which unifies with the skolem

the free ($\alpha$-)type variable $a$ in $\sigma_1$ unifies with $(\forall a.a\to a)$

inference

var

lookup $\sigma$ type for variable in the typing context

abs

fresh $\alpha$ type variable for parameter

infer $\sigma$ type for function body with augmented typing context

instantiate body type with fresh outer quantifiers as $\rho$

generalize $\alpha \to \rho$

app

infer function type $\sigma_1$

instantiate $\sigma_1$ outermost quantifiers to fresh $\alpha$ type variables

infer argument type $\sigma_2$

subsume $\sigma_1$ to $\sigma_2$

check to prevent free $\alpha$-variables from unifying with a $\sigma$-type:

split substitution into a polymorphic part and monomorphic part
check that no free type variable appear in the domain of the polymorphic part

Type Inference

HMF

unification

subsumption

example

inference

var

abs

app