[Git][monnier/typer][report/hmdup] Simplify the rules a bit; not bidi any more :-(
Stefan pushed to branch report/hmdup at Stefan / Typer
Commits: 20732788 by Stefan Monnier at 2020-07-14T22:14:30-04:00 Simplify the rules a bit; not bidi any more :-(
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -50,8 +50,8 @@ \usepackage[utf8]{inputenc} \usepackage{amsmath,mathtools,stmaryrd} \usepackage{mathpartir} -\usepackage{mdframed,empheq} -\usepackage{parskip} +%% \usepackage{mdframed,empheq} +%% \usepackage{parskip} \usepackage{fancybox} %For \ovalbox \usepackage{extarrows} %For \overrightarrow
@@ -333,6 +333,14 @@ minimizing the amount of type annotations was secondary to the design. \Jsynth{x}{\tau[\vec \tau/\vec t]} }
+ \Infer[(HM-Let)]{ + \Jsynth{e_1}{\tau_1} \ + \overrightarrow{t:*} = \kw{gen}(\Gamma,\tau_1) \ + \Jsynth[\Gamma,x:\MDArw{t:*}{\tau_1}]{e_2}{\tau} + }{ + \Jsynth{\Let x {e_1}{e_2}}{\tau} + } + \Infer[(HM-Lam)]{ \Jsynth[\Gamma,x:\tau_1] e {\tau_2} }{ @@ -347,14 +355,6 @@ minimizing the amount of type annotations was secondary to the design. \Jsynth{e_1~e_2}{\tau_2} }
- \Infer[(HM-Let)]{ - \Jsynth{e_1}{\tau_1} \ - \tau_1' = \kw{gen}(\Gamma,\tau_1) \ - \Jsynth[\Gamma,x:\tau_1']{e_2}{\tau} - }{ - \Jsynth{\Let x {e_1}{e_2}}{\tau} - } - %% \Infer{ %% \Jsynth e \tau' \ \Junify \tau {\tau'} %% }{ @@ -412,49 +412,49 @@ $u_2$ was instantiated to.
-\begin{figure} - \begin{mathpar} - \Infer[(BC-Var)]{ - \Gamma(x) = \tau - }{ - \Jsynth{x}{\tau} - } - - \Infer[(BC-Let)]{ - \Jsynth{e_1}{\tau_1} \ - \Jpoly[\Gamma,x:\tau_1]{e_2}{\tau_2} - }{ - \Jpoly{\Let x {e_1}{e_2}}{\tau_2} - } - - \Infer[(BC-App)]{ - %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ - \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ - \Jcheck{e_2}{\tau_1} - }{ - \Jsynth{e_1~e_2}{\tau_2} - } - - %% \Infer{ - %% \Jsynth e \tau' \ \Junify \tau {\tau'} - %% }{ - %% \Jcheck{e}{\tau} - %% } - - \Infer[(BC-Lam)]{ - \Jcheck[\Gamma,x:\tau_1] e {\tau_2} - }{ - \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} - } - - \Infer[(BC-HT)]{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}} - - \Infer[(BC-Check)]{\Jsynth e \tau' \ \tau = \tau'}{\Jcheck{e}{\tau}} - %% - \end{mathpar} - \caption{Basic bidirectional type checking rules} - \label{fig:bidi-check} -\end{figure} +%% \begin{figure} +%% \begin{mathpar} +%% \Infer[(BC-Var)]{ +%% \Gamma(x) = \tau +%% }{ +%% \Jsynth{x}{\tau} +%% } + +%% \Infer[(BC-Let)]{ +%% \Jsynth{e_1}{\tau_1} \ +%% \Jpoly[\Gamma,x:\tau_1]{e_2}{\tau_2} +%% }{ +%% \Jpoly{\Let x {e_1}{e_2}}{\tau_2} +%% } + +%% \Infer[(BC-App)]{ +%% %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ +%% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ +%% \Jcheck{e_2}{\tau_1} +%% }{ +%% \Jsynth{e_1~e_2}{\tau_2} +%% } + +%% %% \Infer{ +%% %% \Jsynth e \tau' \ \Junify \tau {\tau'} +%% %% }{ +%% %% \Jcheck{e}{\tau} +%% %% } + +%% \Infer[(BC-Lam)]{ +%% \Jcheck[\Gamma,x:\tau_1] e {\tau_2} +%% }{ +%% \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} +%% } + +%% \Infer[(BC-Ann)]{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}} + +%% \Infer[(BC-Check)]{\Jsynth e \tau' \ \tau = \tau'}{\Jcheck{e}{\tau}} +%% %% +%% \end{mathpar} +%% \caption{Basic bidirectional type checking rules} +%% \label{fig:bidi-check} +%% \end{figure}
Figure~\cite{fig:bidi-check} shows the traditional bidirectional rules to type check the $\lambda$-calculus. @@ -494,7 +494,7 @@ type check the $\lambda$-calculus. \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} } \\ - \Infer[(BI-HT)]{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}} + \Infer[(BI-Ann)]{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}}
\Infer[(BI-Check)]{\Jsynth e \tau}{\Jcheck{e}{\tau}}
@@ -520,10 +520,87 @@ a $\Lam{x}{e}$.
\section{System F}
-%% \newcommand \JsynthCoerce [3][\Gamma] {#1 \vdash #2 \Longrightarrow #3} +\newcommand \JsynthCoerce [3][\Gamma] {#1 \vdash #2 \Longrightarrow #3} \newcommand \JcheckCoerce [3][\Gamma] {#1 \vdash #2 \Longleftarrow #3} %% \newcommand \Jmono [1] {\kw{monotype}(#1)}
+%% \begin{figure} +%% \begin{mathpar} +%% \Infer[(SF-Var)]{ +%% \Gamma(x) = \tau +%% }{ +%% \Jsynth{x}{\tau} +%% } + +%% \Infer[(SF-Let)]{ +%% \Jsynth{e_1}{\tau_1} \ +%% \overrightarrow{t:*} = \kw{gen}(\Gamma,\tau_1) \ +%% \Jpoly[\Gamma,x:\MDArw{t:*}{\tau_1}]{e_2}{\tau} +%% }{ +%% \Jpoly{\Let x {e_1}{e_2}}{\tau} +%% } + +%% \Infer[(SF-App)]{ +%% %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ +%% \JcheckCoerce{e_1}{\Arw{\tau_1}{\tau_2}} \ +%% \JcheckCoerce{e_2}{\tau_1} +%% }{ +%% \Jsynth{e_1~e_2}{\tau_2} +%% } + +%% %% +%% \Infer[(SF-Ann)]{ +%% \JcheckCoerce e \tau +%% }{ +%% \Jsynth{\HasType{e}{\tau}}{\tau} +%% } + +%% \Infer[(SF-Lam)]{ +%% \JcheckCoerce[\Gamma,x:\tau_1] e {\tau_2} +%% }{ +%% \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} +%% } +%% %% + +%% %% FIXME: Not needed? +%% %% \Infer[(SF-Check)]{\Jsynth e \tau}{\Jcheck{e}{\tau}} + +%% \Infer[(SF-Guess)]{ +%% \Jcheck e {\tau} +%% }{ +%% %% FIXME: Make it \JsynthCoerce? +%% \Jsynth e {\tau} +%% } +%% \\ +%% \Infer[(SF-Poly)]{ +%% \JcheckCoerce[\Gamma,\overrightarrow{t:*}] e {\tau} +%% }{ +%% \JcheckCoerce{e}{\MDArw{t:*}{\tau}} +%% } + +%% \Infer[(SF-Inst)]{ +%% \Jsynth e {\MDArw{t:*}{\tau}} \ +%% }{ +%% \JcheckCoerce{e}{\tau[\vec \tau/\vec t]} +%% } +%% %% +%% %% \Infer[(SF-Poly)]{ +%% %% \Jcheck[\Gamma,\overrightarrow{t:*}] e {\tau} +%% %% }{ +%% %% \JcheckCoerce{e}{\MDArw{t:*}{\tau}} +%% %% } +%% %% +%% %% \Infer[(SF-Coerce)]{ +%% %% %% \Jmono{\tau} \ +%% %% \Jsynth e \tau' \ +%% %% \Jcoerce {\tau'} \tau +%% %% }{ +%% %% \JcheckCoerce{e}{\tau} +%% %% } +%% \end{mathpar} +%% \caption{Bidirectional type inference for System F} +%% \label{fig:system-f} +%% \end{figure} \begin{figure} \begin{mathpar} \Infer[(SF-Var)]{ @@ -534,62 +611,53 @@ a $\Lam{x}{e}$.
\Infer[(SF-Let)]{ \Jsynth{e_1}{\tau_1} \ - \tau_1' = \kw{gen}(\Gamma,\tau_1) \ - \Jpoly[\Gamma,x:\tau_1']{e_2}{\tau} + \overrightarrow{t:*} = \kw{gen}(\Gamma,\tau_1) \ + \Jsynth[\Gamma,x:\MDArw{t:*}{\tau_1}]{e_2}{\tau} }{ - \Jpoly{\Let x {e_1}{e_2}}{\tau} + \Jsynth{\Let x {e_1}{e_2}}{\tau} }
\Infer[(SF-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ - \JcheckCoerce{e_1}{\Arw{\tau_1}{\tau_2}} \ - \JcheckCoerce{e_2}{\tau_1} + \JsynthCoerce{e_1}{\Arw{\tau_1}{\tau_2}} \ + \JsynthCoerce{e_2}{\tau_1} }{ \Jsynth{e_1~e_2}{\tau_2} }
%% - \Infer[(SF-HT)]{ - \JcheckCoerce e \tau + \Infer[(SF-Ann)]{ + \JsynthCoerce e \tau }{ \Jsynth{\HasType{e}{\tau}}{\tau} }
\Infer[(SF-Lam)]{ - \JcheckCoerce[\Gamma,x:\tau_1] e {\tau_2} + \JsynthCoerce[\Gamma,x:\tau_1] e {\tau_2} }{ - \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} + \Jsynth{\Lam x e}{\Arw{\tau_1}{\tau_2}} } %%
- %% FIXME: Not needed? - %% \Infer[(SF-Check)]{\Jsynth e \tau}{\Jcheck{e}{\tau}} - - \Infer[(SF-Guess)]{ - \Jcheck e {\tau} - }{ - %% FIXME: Make it \JsynthCoerce? - \Jsynth e {\tau} - } \\ \Infer[(SF-Poly)]{ - \JcheckCoerce[\Gamma,\overrightarrow{t:*}] e {\tau} + \JsynthCoerce[\Gamma,\overrightarrow{t:*}] e {\tau} }{ - \JcheckCoerce{e}{\MDArw{t:*}{\tau}} + \JsynthCoerce{e}{\MDArw{t:*}{\tau}} }
\Infer[(SF-Inst)]{ \Jsynth e {\MDArw{t:*}{\tau}} \ }{ - \JcheckCoerce{e}{\tau[\vec \tau/\vec t]} + \JsynthCoerce{e}{\tau[\vec \tau/\vec t]} } - + %% %% \Infer[(SF-Poly)]{ %% \Jcheck[\Gamma,\overrightarrow{t:*}] e {\tau} %% }{ %% \JcheckCoerce{e}{\MDArw{t:*}{\tau}} %% } - + %% %% \Infer[(SF-Coerce)]{ %% %% \Jmono{\tau} \ %% \Jsynth e \tau' \ @@ -597,8 +665,8 @@ a $\Lam{x}{e}$. %% }{ %% \JcheckCoerce{e}{\tau} %% } -\ \end{mathpar} - \caption{Bidirectional type inference for System F} + \end{mathpar} + \caption{Type inference for System F} \label{fig:system-f} \end{figure}
@@ -607,26 +675,40 @@ a $\Lam{x}{e}$. It is usually accepted wisdom that extending HM-inference to a more sophisticated type system requires the addition of explicit annotations. While we do not intend to require as few annotations as systems like -\MLF{}~\cite{Botlan03}, we do consider it important to make good use of existing -type annotations to try and reduce the amount of annotations needed. -To this end, we need to pay attention to the places where redundant type -information can be better used. In the original Hindley-Milner algorithm, -we can see that the only place where we might ``burn off'' excess -information is in the call to \kw{unify} in the application rule, where the -type $\tau_1$ of the argument might be inferred both from $e_2$ and from $e_1$. +\MLF{}~\cite{Botlan03}, we do consider it important to make good use of +existing type information to try and reduce the amount of annotations +needed. To this end, we need to pay attention to the places where redundant +type information can be better used. In the original Hindley-Milner +algorithm, we can see that the only place where we might ``burn off'' excess +information is in the \textsc{HM-App} rule, where the type $\tau_1$ of the +argument might be inferred both from $e_2$ and from $e_1$. + Our inference algorithm takes inspiration from bidirectional type systems to -try and make better use of that information. +try and make better use of that information. In such systems, the +application rule usually looks something like: +\begin{displaymath} + \Infer[(BI-App)]{ + \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ + \Jcheck{e_2}{\tau_1} + }{ + \Jsynth{e_1~e_2}{\tau_2} + } +\end{displaymath} +Which means that to \emph{synthesize} the type of ``${e_1~e_2}$'' we first +synthesize the type of $e_1$, which gives us both $\tau_1$ and $\tau_2$ after +which we can just \emph{check} the type of $e_2$ against $\tau_1$. +This is because in the vast majority of cases we already know the type of +the function we're calling.
The only change to the syntax of the language is the addition of the form $\HasType{e}{\tau}$. While the specific form of the type annotations is not -a primary -concern for us, we did want to avoid ``non-standard'' annotations such as -the freeze annotation of FreezeML~\cite{Emrich20} or the constrained +a primary concern for us, we did want to avoid ``non-standard'' annotations +such as the freeze annotation of FreezeML~\cite{Emrich20} or the constrained quantifiers of \MLF: %% \begin{displaymath} \begin{array}{cc@{;;::=;;}l} - \textit{(types)} & \tau & t ~|~ \Meta{u} ~|~ \Arw{\tau_1}{\tau_2} ~|~ \DArw t * \tau \ + \textit{(types)} & \tau & t ~|~ \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} ~|~ \HasType{e}{\tau} \ \textit{(context)} & \Gamma & \bullet ~|~ \Gamma,x:\tau ~|~ \Gamma,t:* \ @@ -634,11 +716,14 @@ quantifiers of \MLF: \end{array} \end{displaymath} %% -Figure~\ref{fig:system-f} shows how we extend the previous rules to handle -System-F. There are now three judgments: $\Jsynth e \tau$ which synthesizes -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. +Figure~\ref{fig:system-f} shows an idealized form of how we extend +Hindley-Milner to handle System-F. There are now three judgments: $\Jsynth +e \tau$ which synthesizes 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 checks that $e$ is well-typed and that it can be +coerced to type $\tau$ by judicious addition of type abstractions and type +applications. 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 @@ -763,7 +848,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{gen}(\Gamma, \tau_1) \ \JEpoly[\Gamma,x:\MDArw{t:*}{\tau_1}]{e_2}{\tau}{E_2} }{ \JEpoly{\Let x {e_1}{e_2}}{\tau}{ @@ -772,32 +857,29 @@ incompatible with things like value polymorphism.
\Infer[(EF-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ - \Jfresh{u_1,u_2} \ - \JEcheckCoerce{e_1}{\Arw{u_1}{u_2}}{E_1} \ - \JEcheck{e_2}{u_1}{E_2} + \JEcheckCoerce{e_1}{\Arw{\tau_1}{\tau_2}}{E_1} \ + \JEcheck{e_2}{\tau_1}{E_2} }{ - \JEsynth{e_1~e_2}{u_2}{E_1~E_2} + \JEsynth{e_1~e_2}{\tau_2}{E_1~E_2} }
- \Infer[(EF-Lam)]{ - \Jfresh {\Meta{u_1},\Meta{u_2}} \ - \Junify {\tau}{\Arw{\Meta{u_1}}{\Meta{u_2}}} \ - \JEcheckCoerce[\Gamma,x:\Meta{u_1}]{e}{\Meta{u_2}}{E} + \Infer[(EF-Ann)]{ + \JEcheckCoerce e \tau E }{ - \JEcheck{\Lam x e}{\tau}{\Lam{x:\Meta{u_1}}{E}} + \JEsynth{(\HasType{e}{\tau})}{\tau}{E} }
- \Infer[(EF-HT)]{ - \JEcheckCoerce e \tau E + \Infer[(EF-Lam)]{ + \JEcheckCoerce[\Gamma,x:\tau_1]{e}{\tau_2}{E} }{ - \JEsynth{\HasType{e}{\tau}}{\tau}{E} + \JEcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}}{\Lam{x:\tau_1}{E}} }
- \Infer[(EF-Infer)]{ - \Jfresh{\Meta{u}} \ \JEcheck{e}{\Meta{u}}{E} + \Infer[(EF-Guess)]{ + \JEcheck{e}{\tau}{E} }{ %% FIXME: Make it \JsynthCoerce? - \JEsynth{e}{\Meta{u}}{E} + \JEsynth{e}{\tau}{E} }
\Infer[(EF-Poly)]{ @@ -806,43 +888,42 @@ incompatible with things like value polymorphism. \JEcheckCoerce{e}{\MDArw{t:*}{\tau}}{\TLam{\overrightarrow{t:*}}{E}} }
- \Infer[(EF-Coerce)]{ + \Infer[(EF-Inst)]{ %% \Jmono{\tau} \ - \JEsynth{e}{\tau}{E} \ - \JEcoerce {E}{\tau}{E'}{\tau'} + \JEsynth e {\MDArw{t:*}{\tau}}{E} \ }{ - \JEcheckCoerce{e}{\tau'}{E'} + \JEcheckCoerce{e}{\tau[\vec \tau/\vec t]}{\TApp{e}{\vec \tau}} }
%% FIXME: The rules below don't make much sense yet, I think! %% - \Infer[(CO-Inst)]{ - \Jfresh {\vec {\Meta{u}}} \ - \Junify{\tau[\vec {\Meta{u}}/\vec t]}{\tau'} - }{ - \JEcoerce {E} {\MDArw{t:*}{\tau}} - {\TApp{E}{\vec {\Meta{u}}}} {\tau'} - } + %% \Infer[(CO-Inst)]{ + %% \Jfresh {\vec {\Meta{u}}} \ + %% \Junify{\tau[\vec {\Meta{u}}/\vec t]}{\tau'} + %% }{ + %% \JEcoerce {E} {\MDArw{t:*}{\tau}} + %% {\TApp{E}{\vec {\Meta{u}}}} {\tau'} + %% }
- \Infer[(CO-Gen)]{ - \Jfresh {\vec {\Meta{u}}} \ - \JEcoerce {E} {\tau} {E'} {\tau'[\vec {\Meta{u}}/\vec t]} \ - \vec {\Meta{u}} \subset \kw{fmv}(\Gamma,\tau'[\vec {\Meta{u}}/\vec t]) - }{ - \JEcoerce {E} {\tau} {\TLam{\overrightarrow{t:*}}{E'}} {\MDArw{t:*}{\tau'}} - } + %% \Infer[(CO-Gen)]{ + %% \Jfresh {\vec {\Meta{u}}} \ + %% \JEcoerce {E} {\tau} {E'} {\tau'[\vec {\Meta{u}}/\vec t]} \ + %% \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} - } + %% \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}
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/20732788c43cab1470c19eddf7b0a9a980...
Afficher les réponses par date
-
Stefan