Stefan pushed to branch report/hmdup at Stefan / Typer
Commits: 70a63f79 by Stefan Monnier at 2020-07-01T17:56:57-04:00 -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -637,6 +637,7 @@ a type, as before, $\Jcheck e \tau$ which only \emph{checks}, taking all three arguments $\Gamma$, $e$, and $\tau$ as input, and $\JcheckCoerce e \tau$ which \FIXME{explain}. The rules also use $\Jpoly e \tau$ which is just a shorthand for a pair of rules, one that checks and one that synthesizes.
+\FIXME{The text below is out of date} The first three lines are equivalent to the base Hindley-Milner system presented earlier. The two differences are: (1) the instantiation of polymorphic terms has now been moved from the variable rule to its own @@ -682,6 +683,12 @@ so there is no backtracking involved. \FIXME{Write (sketch of) the proof} \end{proof}
+\subsection{Implicit type variables} + +\FIXME{Expand} +The \textsc{SF-Poly} rule has the side effect of making the $t$ variable +visible in the code. + \subsection{Metavariables}
A more subtle aspect of these rules is that the side-effects of unifications @@ -710,6 +717,18 @@ resort to such a mitigation strategy.
\FIXME{This was true in the previous version of the rules, but not any more}
+There can be different choices of how to combine the \textsc{CO-Gen} and +\textsc{CO-Inst} rules. For example, when coercing +a $\DArw{t}{*}{\Arw{t}{\Meta{u}}}$ to +$\DArw{t'}{*}\DArw{t}{*}{\Arw{t}{t'}}$, one choice is to just generalize +$\Meta{u}$ to a $t'$ type parameter and be done with it, but another choice +is for \textsc{CO-Inst} to first instantiate $t$ to $\Meta{u'}$ and then +have \textsc{CO-Gen} generalize both $\Meta{u}$ and $\Meta{u'}$ to two +type parameters. The second choice leads to extra $\eta$-redexes but has the +advantage of being a bit more permissive w.r.t ordering of type arguments. + + + This presentation has the downside that it introduces many eta-redexes because the $\forall$ rule eagerly introduces $\Lambda$. It does have the advantage of making the inference less sensitive to the order of quantifiers, but it @@ -722,6 +741,9 @@ incompatible with things like value polymorphism.
\section{Elaboration}
+\FIXME{We should probably directly present the elaborating version of the + algorithm without going through Figure~\ref{fig:system-f} first} + \newcommand \JEcheck [4][\Gamma] {#1 \vdash #2 : #3 \Rightarrow #4} \newcommand \JEsynth [4][\Gamma] {#1 \vdash #2 \Rightarrow #4 : #3} \newcommand \JEcheckCoerce [4][\Gamma] {#1 \vdash #2 : #3 \Longrightarrow #4} @@ -738,7 +760,7 @@ incompatible with things like value polymorphism.
\Infer[(EF-Let)]{ \JEsynth{e_1}{\tau_1}{E_1} \ - \overrightarrow{t:*} = \kw{fmv}(\Gamma,\tau_1) \ + \overrightarrow{t:*} = \kw{fmv!}(\Gamma,\tau_1) \ \JEpoly[\Gamma,x:\MDArw{t:*}{\tau_1}]{e_2}{\tau}{E_2} }{ \JEpoly{\Let x {e_1}{e_2}}{\tau}{ @@ -802,18 +824,41 @@ incompatible with things like value polymorphism. \Infer[(CO-Gen)]{ \Jfresh {\vec {\Meta{u}}} \ \JEcoerce {E} {\tau} {E'} {\tau'[\vec {\Meta{u}}/\vec t]} \ - %% FIXME: Maybe "u" was instantiated to some other - %% (uninstantiated) metavar. If so, should it still be in `fmv`? - %% FIXME: Define `fmv`!! \vec {\Meta{u}} \subset \kw{fmv}(\Gamma,\tau'[\vec {\Meta{u}}/\vec t]) }{ \JEcoerce {E} {\tau} {\TLam{\overrightarrow{t:*}}{E'}} {\MDArw{t:*}{\tau'}} } \end{mathpar} + \FIXME{ + Rule \textsc{CO-Gen} has many problems: + \begin{itemize} + \item Maybe "u" was instantiated to some other + (uninstantiated) metavar. \ + If so, should it still be in `fmv`? + \item We're using $\Gamma$ even though we don't actually have it! + \item Define `fmv`!! + \item `fmv` is not quite the same as the previous `fmv!`!! + \end{itemize} + } \caption{Elaboration for System F} \label{fig:elab-system-f} \end{figure}
+Figure~\ref{fig:elab-system-f} shows the type inference algorithm for +System~F, which also returns an elaborated form of the source code. + +The target language is a fairly standard version of Church style System F: +\begin{displaymath} + \begin{array}{cc@{;;::=;;}l} + \textit{(types)} & \tau & t ~|~ \Meta{u} ~|~ \Arw{\tau_1}{\tau_2} ~|~ \DArw t * \tau \ + \textit{(terms)} & E & x ~|~ \Lam x e ~|~ e_1~e_2 ~|~ \Let + x {e_1} {e_2} ~|~ \TLam{t:*}{E} ~|~ \TApp{E}{\tau} \ + \textit{(context)} & \Gamma & \bullet ~|~ \Gamma,x:\tau ~|~ \Gamma,t:* \ + %% \textit{(substitutions)} & \sigma & \textsf{id} ~|~ \sigma,\Meta{u}\mapsto\tau + \end{array} +\end{displaymath} + + \section{Lazy elaboration}
To try and address the ordering issue, we can do the elaboration a bit more
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/70a63f794071e24e0bb4b67aa2ed591ff7...