Stefan pushed to branch report/hmdup at Stefan / Typer

Commits: b9d015b4 by Stefan Monnier at 2020-06-28T17:57:48-04:00 -

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -310,6 +310,7 @@ minimizing the amount of type annotations was secondary to the design. \newcommand \Arw [2] {#1 \to #2} \newcommand \Lam [2] {\lambda #1 . #2} \newcommand \TLam [2] {\Lambda #1 . #2} +\newcommand \TApp [2] {#1[#2]} \newcommand \Meta [1] {#1} \newcommand \DArw [3] {\forall #1 : #2 . #3} \newcommand \Let [3] {\kw{let}~#1=#2~\kw{in}~#3} @@ -577,24 +578,17 @@ a $\Lam{x}{e}$. }

\Infer{ - %% \Jmono{\tau} \ - \Jsynth e \tau' \ - \Jcoerce {\tau'} \tau + \Jcheck[\Gamma,\overrightarrow{t:*}] e {\tau} }{ - \JcheckCoerce{e}{\tau} + \JcheckCoerce{e}{\MDArw{t:*}{\tau}} }

- %% \Infer{ - %% \Jsynth{e}{\tau'} \ - %% \Jcoerce {\tau'} \tau - %% }{ - %% \JsynthCoerce{e}{\tau} - %% } - %% \Infer{ - \Jcheck[\Gamma,\overrightarrow{t:*}] e {\tau} + %% \Jmono{\tau} \ + \Jsynth e \tau' \ + \Jcoerce {\tau'} \tau }{ - \JcheckCoerce{e}{\MDArw{t:*}{\tau}} + \JcheckCoerce{e}{\tau} } \end{mathpar} \caption{Bidirectional type inference for System F} @@ -803,86 +797,11 @@ incompatible with things like value polymorphism.

\section{Elaboration}

-\FIXME{Adapt the rules to the new algorithm} - -\begin{figure} - \begin{mathpar} - \Infer{ - \Gamma(x) = \tau - }{ - \Jsynth{x}{\tau} - } - - \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{ - %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ - \Jfresh{u_1,u_2} \ - \JcheckCoerce{e_1}{\Arw{u_1}{u_2}} \ - \JcheckCoerce{e_2}{u_1} - }{ - \Jsynth{e_1~e_2}{u_2} - } - - \Infer{ - \Jfresh{u_1, u_2} \ - %% FIXME: Introduce polymorphism?! - \Junify{\tau}{\Arw{u_1}{u_2}} \ - \JcheckCoerce[\Gamma,x:u_1] e {u_2} - }{ - \Jcheck{\Lam x e}{\tau} - } - %% - - %% - \Infer{ - \JcheckCoerce e \tau - }{ - \Jsynth{\HasType{e}{\tau}}{\tau} - } - - \Infer{ - \Jfresh{\Meta{u}} \ \Jcheck e {\Meta{u}} - }{ - %% FIXME: Make it \JsynthCoerce? - \Jsynth e {\Meta{u}} - } - - \Infer{ - %% \Jmono{\tau} \ - \Jsynth e \tau' \ - \Jcoerce {\tau'} \tau - }{ - \JcheckCoerce{e}{\tau} - } - - %% \Infer{ - %% \Jsynth{e}{\tau'} \ - %% \Jcoerce {\tau'} \tau - %% }{ - %% \JsynthCoerce{e}{\tau} - %% } - %% - \Infer{ - \Jcheck[\Gamma,\overrightarrow{t:*}] e {\tau} - }{ - \JcheckCoerce{e}{\MDArw{t:*}{\tau}} - } - \end{mathpar} - \caption{Bidirectional type inference for System F} - \label{fig:system-f} -\end{figure} - \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} \newcommand \JEpoly [4][\Gamma] {#1 \vdash #2 \Leftrightarrow #4 : #3} +\newcommand \JEcoerce [4] {#1 : #2 \stackrel{\kw{coerce}}{\Longrightarrow} #3 : #4}

\begin{figure} \begin{mathpar} @@ -931,18 +850,39 @@ incompatible with things like value polymorphism. \JEsynth{e}{\Meta{u}}{E} }

+ \Infer{ + \JEcheck[\Gamma,\overrightarrow{t:*}] e {\tau}{E} + }{ + \JEcheckCoerce{e}{\MDArw{t:*}{\tau}}{\TLam{\overrightarrow{t:*}}{E}} + } + \Infer{ %% \Jmono{\tau} \ - \JEsynth{e}{\tau'}{E} \ - \FIXMEs{E' = \Jcoerce {\tau'} \tau} + \JEsynth{e}{\tau}{E} \ + \JEcoerce {E}{\tau}{E'}{\tau'} + }{ + \JEcheckCoerce{e}{\tau'}{E'} + } + + %% FIXME: The rules below don't make much sense yet, I think! + %% + \Infer{ + \Jfresh {\vec {\Meta{u}}} \ + \Junify{\tau[\vec {\Meta{u}}/\vec t]}{\tau'} }{ - \JEcheckCoerce{e}{\tau}{E'} + \JEcoerce {E} {\MDArw{t:*}{\tau}} + {\TApp{E}{\vec {\Meta{u}}}} {\tau'} }

\Infer{ - \JEcheck[\Gamma,\overrightarrow{t:*}] e {\tau}{E} + \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]) }{ - \JEcheckCoerce{e}{\MDArw{t:*}{\tau}}{\TLam{\overrightarrow{t:*}}{E}} + \JEcoerce {E} {\tau} {\TLam{\overrightarrow{t:*}}{E'}} {\MDArw{t:*}{\tau'}} } \end{mathpar} \caption{Elaboration for System F}

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b9d015b4842ea6de505a6735d5913dc018...