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... -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9260df919402604ceb9a87a0fa1c53b13e... You're receiving this email because of your account on gitlab.com.