Stefan pushed to branch report/hmdup at Stefan / Typer
Commits: 9260df91 by Stefan Monnier at 2020-07-01T13:05:31-04:00 -
- - - - -
1 changed file:
- paper.tex
Changes:
===================================== paper.tex ===================================== @@ -320,21 +320,28 @@ minimizing the amount of type annotations was secondary to the design. \newcommand \Jcheck [3][\Gamma] {#1 \vdash #2 \Leftarrow #3} \newcommand \Jsynth [3][\Gamma] {#1 \vdash #2 \Rightarrow #3} \newcommand \Jpoly [3][\Gamma] {#1 \vdash #2 \Leftrightarrow #3} -\newcommand \Junify [2] {\kw{unify}(#1,#2)} +\newcommand \Junify [2] {\kw{unify!}(#1,#2)} \newcommand \Jfresh [1] {#1~\kw{fresh}} \newcommand \Jinst [1] {\kw{inst}(#1)} \newcommand \Jcoerce [2] {\kw{coerce}(#1,#2)}
\begin{figure} \begin{mathpar} - \Infer{ - \Gamma(x) = \tau \ - \tau' = \Jinst{\tau} + \Infer[(HM-Var)]{ + \Gamma(x) = \MDArw{t:*}\tau \ + \Jfresh {\vec u} }{ - \Jsynth{x}{\tau'} + \Jsynth{x}{\tau[\vec u/\vec t]} }
- \Infer{ + \Infer[(HM-Lam)]{ + \Jfresh u \ + \Jsynth[\Gamma,x:u] e {\tau} + }{ + \Jsynth{\Lam x e}{\Arw{u}{\tau}} + } + + \Infer[(HM-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ \Jsynth{e_1}{\tau} \ \Jfresh{u_2} \ @@ -344,7 +351,7 @@ minimizing the amount of type annotations was secondary to the design. \Jsynth{e_1~e_2}{u_2} }
- \Infer{ + \Infer[(HM-Let)]{ \Jsynth{e_1}{\tau_1} \ \tau_1' = \kw{gen}(\Gamma,\tau_1) \ \Jsynth[\Gamma,x:\tau_1']{e_2}{\tau} @@ -358,12 +365,6 @@ minimizing the amount of type annotations was secondary to the design. %% \Jcheck{e}{\tau} %% }
- \Infer{ - \Jfresh u \ - \Jsynth[\Gamma,x:u] e {\tau} - }{ - \Jsynth{\Lam x e}{\Arw{u}{\tau}} - } %% \end{mathpar} \caption{Hindley-Milner type inference in the style of algorithm J} @@ -408,7 +409,7 @@ metavariable will usually have been instantiated by the preceding $\Junify{\tau}{\Arw{\tau_1}{u_2}}$, so the type returned is really whichever type $u_2$ was instantiated to.
-\FIXME{Walk through the rules, describe/define \kw{inst} and \kw{gen}, ...}. +\FIXME{Walk through the rules, describe/define \kw{gen}, ...}.
%% \newpage \subsection{Bidirectional Type Checking} @@ -417,20 +418,20 @@ $u_2$ was instantiated to.
\begin{figure} \begin{mathpar} - \Infer{ + \Infer[(BC-Var)]{ \Gamma(x) = \tau }{ \Jsynth{x}{\tau} }
- \Infer{ + \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{ + \Infer[(BC-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ \Jcheck{e_2}{\tau_1} @@ -444,15 +445,15 @@ $u_2$ was instantiated to. %% \Jcheck{e}{\tau} %% }
- \Infer{ + \Infer[(BC-Lam)]{ \Jcheck[\Gamma,x:\tau_1] e {\tau_2} }{ \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} }
- \Infer{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}} + \Infer[(BC-HT)]{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}}
- \Infer{\Jsynth e \tau' \ \tau = \tau'}{\Jcheck{e}{\tau}} + \Infer[(BC-Check)]{\Jsynth e \tau' \ \tau = \tau'}{\Jcheck{e}{\tau}} %% \end{mathpar} \caption{Basic bidirectional type checking rules} @@ -464,20 +465,20 @@ type check the $\lambda$-calculus.
\begin{figure} \begin{mathpar} - \Infer{ + \Infer[(BI-Var)]{ \Gamma(x) = \tau }{ \Jsynth{x}{\tau} }
- \Infer{ + \Infer[(BI-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{ + \Infer[(BI-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ \Jsynth{e_1}{\tau_1} \ \Jfresh{u_1, u_2} \ @@ -493,7 +494,7 @@ type check the $\lambda$-calculus. %% \Jcheck{e}{\tau} %% }
- \Infer{ + \Infer[(BI-Lam)]{ \Jfresh{\Meta{u_1}, \Meta{u_2}} \ \Junify{\tau}{\Arw{u_1}{u_2}} \ \Jcheck[\Gamma,x:\Meta{u_1}] e {\Meta{u_2}} @@ -501,12 +502,15 @@ type check the $\lambda$-calculus. \Jcheck{\Lam x e}{\tau} } \\ - \Infer{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}} + \Infer[(BI-HT)]{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}}
- \Infer{\Jfresh{\Meta{u}} \ \Jcheck e {\Meta{u}}}{\Jsynth e {\Meta{u}}} + \Infer[(BI-Check)]{\Jsynth e \tau' \ \Junify{\tau}{\tau'}}{\Jcheck{e}{\tau}}
- \Infer{\Jsynth e \tau' \ \Junify{\tau}{\tau'}}{\Jcheck{e}{\tau}} - %% + \Infer[(BI-Infer)]{ + \Jfresh{\Meta{u}} \ \Jcheck e {\Meta{u}} + }{ + \Jsynth e {\Meta{u}} + } \end{mathpar} \caption{Basic bidirectional type inference rules} \label{fig:bidi-infer} @@ -530,13 +534,13 @@ a $\Lam{x}{e}$.
\begin{figure} \begin{mathpar} - \Infer{ + \Infer[(SF-Var)]{ \Gamma(x) = \tau }{ \Jsynth{x}{\tau} }
- \Infer{ + \Infer[(SF-Let)]{ \Jsynth{e_1}{\tau_1} \ \tau_1' = \kw{gen}(\Gamma,\tau_1) \ \Jpoly[\Gamma,x:\tau_1']{e_2}{\tau} @@ -544,7 +548,7 @@ a $\Lam{x}{e}$. \Jpoly{\Let x {e_1}{e_2}}{\tau} }
- \Infer{ + \Infer[(SF-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ \Jfresh{u_1,u_2} \ \JcheckCoerce{e_1}{\Arw{u_1}{u_2}} \ @@ -553,7 +557,7 @@ a $\Lam{x}{e}$. \Jsynth{e_1~e_2}{u_2} }
- \Infer{ + \Infer[(SF-Lam)]{ \Jfresh{u_1, u_2} \ %% FIXME: Introduce polymorphism?! \Junify{\tau}{\Arw{u_1}{u_2}} \ @@ -564,26 +568,26 @@ a $\Lam{x}{e}$. %%
%% - \Infer{ + \Infer[(SF-HT)]{ \JcheckCoerce e \tau }{ \Jsynth{\HasType{e}{\tau}}{\tau} }
- \Infer{ + \Infer[(SF-Infer)]{ \Jfresh{\Meta{u}} \ \Jcheck e {\Meta{u}} }{ %% FIXME: Make it \JsynthCoerce? \Jsynth e {\Meta{u}} }
- \Infer{ + \Infer[(SF-Poly)]{ \Jcheck[\Gamma,\overrightarrow{t:*}] e {\tau} }{ \JcheckCoerce{e}{\MDArw{t:*}{\tau}} }
- \Infer{ + \Infer[(SF-Coerce)]{ %% \Jmono{\tau} \ \Jsynth e \tau' \ \Jcoerce {\tau'} \tau @@ -595,85 +599,6 @@ a $\Lam{x}{e}$. \label{fig:system-f} \end{figure}
-%% \begin{figure} -%% \begin{mathpar} -%% \Infer{ -%% \Gamma(x) = \tau -%% }{ -%% \Jsynth{x}{\tau} -%% } - -%% \Infer{ -%% \Jsynth{x}{\tau} \ -%% \tau' = \Jinst{\tau} -%% }{ -%% \JsynthCoerce{x}{\tau'} -%% } - -%% \Infer{ -%% %% \Jmono{\tau} \ -%% \JsynthCoerce e \tau' \ -%% \Junify \tau {\tau'} -%% }{ -%% \Jcheck{e}{\tau} -%% } - -%% \Infer{ -%% %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ -%% \JsynthCoerce{e_1}{\tau} \ -%% \Jfresh{u_1,u_2} \ -%% \Junify{\tau}{\Arw{u_1}{u_2}} \ -%% \Jcheck{e_2}{u_1} -%% }{ -%% \Jsynth{e_1~e_2}{u_2} -%% } - -%% \Infer{ -%% \Jsynth{e_1}{\tau_1} \ -%% \tau_1' = \kw{gen}(\Gamma,\tau_1) \ -%% \Jpoly[\Gamma,x:\tau_1']{e_2}{\tau} -%% }{ -%% \Jpoly{\Let x {e_1}{e_2}}{\tau} -%% } - -%% \Infer{ -%% \Jfresh u \ -%% \JsynthCoerce[\Gamma,x:u] e {\tau} -%% }{ -%% \Jsynth{\Lam x e}{\Arw{u}{\tau}} -%% } -%% %% -%% \\ -%% %% -%% \Infer{ -%% \Jcheck e \tau -%% }{ -%% \Jsynth{\HasType{e}{\tau}}{\tau} -%% } - -%% \Infer{ -%% \Jcheck[\Gamma,x:\tau_1] e {\tau_2} -%% }{ -%% \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} -%% } - -%% %% \Infer{ -%% %% \Gamma(x) = \tau' \ \Junify{\tau'}{\DArw{t}{*}{\tau}} -%% %% }{ -%% %% \Jcheck{x}{\DArw{t}{*}{\tau}} -%% %% } -%% %% -%% \Infer{ -%% \Jcheck[\Gamma,t:*] e {\tau} -%% }{ -%% \Jcheck{e}{\DArw{t}{*}{\tau}} -%% } - -%% \end{mathpar} -%% \caption{Bidirectional type inference with extra eta for System F} -%% \label{fig:system-f} -%% \end{figure} - \newcommand \MLF {ML\textsuperscript{F}}
It is usually accepted wisdom that extending HM-inference to a more
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9260df919402604ceb9a87a0fa1c53b13e...