$$
\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}}
$$
HMF
var
- trivial
- renvoie juste le type selon le contexte
let
- trivial
- infère le type de la variable
- infère le type du corps avec le type de la variable dans le contexte
- renvoie le type du corps avec le préfixe à jour
abs
- obtient une variable fraiche \(\alpha\) pour le type du paramètre
- infère le type du corps avec le contexte mis à jour avec le paramètre
- instancie le type du corps \(\sigma\) en \(\rho\)
generalize \(\alpha \to \rho\) et retourne
- (remonte les quantificateurs en position positive dans les fonctions)
abs-ann
- idem sauf qu’on passe directement \(x: \sigma\) lors de l’inférence du
corps de l’abstraction
app
- toute la viande est là
- infère le type de la fonction, instancie en \(\rho\)
- matche \(\rho = \sigma_e \to \sigma\)
- normalement on a déjà \(\sigma = \rho_2\) car les quantificateurs
sont remontés (par contre attention aux annotations utilisateur
qui ne respectent pas forcément cela)
- infère le type de l’argument \(\sigma_o\)
subsume \(\sigma_e\) (expected) en \(\sigma_o\) (offered)
- i.e. trouve une substitution la plus générale possible telle
que \(\theta \sigma_o \leq \theta \sigma_e\)
split la substitution résultat en mono/polymorphe et vérifie que
la substitution polymorphe ne concerne aucune variable du contexte
- alternativement, on peut vérifier que le type de l’argument dans
abs est monomorphe, sans splitter la substitution
generalize le type de retour et retourne
subsume
- instancie le type \(\sigma_o\) pour matcher \(\sigma_e\)
- suppose que les deux arguments sont en forme normale
(quantificateurs dans l’ordre d’apparition des variables)
- skolemize \(\sigma_e\) en \(\rho_e\)
- instancie \(\sigma_o\) en \(\rho_o\)
unify \(\rho_e\) et \(\rho_o\)- erreur si la substitution résultat (sauf les variables instanciées
pour \(\rho_o\)) continent des skolems
- on doit pouvoir améliorer en ayant des variables qui peuvent ou
non unifier avec des skolems
unify
e-mail comments/suggestions