Stefan pushed to branch report/hmdup at Stefan / Typer

Commits: 9322269d by Stefan Monnier at 2020-07-07T22:39:46-04:00 Rewrite rules to keep unification implicit

- - - - -

1 changed file:

- paper.tex

Changes:

===================================== paper.tex ===================================== @@ -329,26 +329,22 @@ minimizing the amount of type annotations was secondary to the design. \begin{mathpar} \Infer[(HM-Var)]{ \Gamma(x) = \MDArw{t:*}\tau \ - \Jfresh {\vec u} }{ - \Jsynth{x}{\tau[\vec u/\vec t]} + \Jsynth{x}{\tau[\vec \tau/\vec t]} }

\Infer[(HM-Lam)]{ - \Jfresh u \ - \Jsynth[\Gamma,x:u] e {\tau} + \Jsynth[\Gamma,x:\tau_1] e {\tau_2} }{ - \Jsynth{\Lam x e}{\Arw{u}{\tau}} + \Jsynth{\Lam x e}{\Arw{\tau_1}{\tau_2}} }

\Infer[(HM-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ - \Jsynth{e_1}{\tau} \ - \Jfresh{u_2} \ - \Junify{\tau}{\Arw{\tau_1}{u_2}} \ + \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ \Jsynth{e_2}{\tau_1} }{ - \Jsynth{e_1~e_2}{u_2} + \Jsynth{e_1~e_2}{\tau_2} }

\Infer[(HM-Let)]{ @@ -367,8 +363,8 @@ minimizing the amount of type annotations was secondary to the design.

%% \end{mathpar} - \caption{Hindley-Milner type inference in the style of algorithm J} - \label{fig:algo-j} + \caption{Hindley-Milner type inference} + \label{fig:hm} \end{figure}

As a warm up and to clarify the notation used in the rest of the article, we @@ -377,7 +373,7 @@ the $\lambda$-calculus we will use for that is the following: %% \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} \ \textit{(context)} & \Gamma & \bullet ~|~ \Gamma,x:\tau ~|~ \Gamma,t:* \ %% \textit{(substitutions)} & \sigma & \textsf{id} ~|~ \sigma,\Meta{u}\mapsto\tau @@ -480,12 +476,10 @@ type check the $\lambda$-calculus.

\Infer[(BI-App)]{ %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ - \Jsynth{e_1}{\tau_1} \ - \Jfresh{u_1, u_2} \ - \Junify{\tau_1}{\Arw{u_1}{u_2}} \ - \Jcheck{e_2}{u_1} + \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \ + \Jcheck{e_2}{\tau_1} }{ - \Jsynth{e_1~e_2}{u_2} + \Jsynth{e_1~e_2}{\tau_2} }

%% \Infer{ @@ -495,21 +489,19 @@ type check the $\lambda$-calculus. %% }

\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}} + \Jcheck[\Gamma,x:\tau_1] e {\tau_2} }{ - \Jcheck{\Lam x e}{\tau} + \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} } \\ \Infer[(BI-HT)]{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}}

- \Infer[(BI-Check)]{\Jsynth e \tau' \ \Junify{\tau}{\tau'}}{\Jcheck{e}{\tau}} + \Infer[(BI-Check)]{\Jsynth e \tau}{\Jcheck{e}{\tau}}

- \Infer[(BI-Infer)]{ - \Jfresh{\Meta{u}} \ \Jcheck e {\Meta{u}} + \Infer[(BI-Guess)]{ + \Jcheck e {\tau} }{ - \Jsynth e {\Meta{u}} + \Jsynth e {\tau} } \end{mathpar} \caption{Basic bidirectional type inference rules} @@ -550,22 +542,11 @@ a $\Lam{x}{e}$.

\Infer[(SF-App)]{ %% \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[(SF-Lam)]{ - \Jfresh{u_1, u_2} \ - %% FIXME: Introduce polymorphism?! - \Junify{\tau}{\Arw{u_1}{u_2}} \ - \JcheckCoerce[\Gamma,x:u_1] e {u_2} + \JcheckCoerce{e_1}{\Arw{\tau_1}{\tau_2}} \ + \JcheckCoerce{e_2}{\tau_1} }{ - \Jcheck{\Lam x e}{\tau} + \Jsynth{e_1~e_2}{\tau_2} } - %%

%% \Infer[(SF-HT)]{ @@ -574,27 +555,49 @@ a $\Lam{x}{e}$. \Jsynth{\HasType{e}{\tau}}{\tau} }

- \Infer[(SF-Infer)]{ - \Jfresh{\Meta{u}} \ \Jcheck e {\Meta{u}} + \Infer[(SF-Lam)]{ + \JcheckCoerce[\Gamma,x:\tau_1] e {\tau_2} }{ - %% FIXME: Make it \JsynthCoerce? - \Jsynth e {\Meta{u}} + \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)]{ - \Jcheck[\Gamma,\overrightarrow{t:*}] e {\tau} + \JcheckCoerce[\Gamma,\overrightarrow{t:*}] e {\tau} }{ \JcheckCoerce{e}{\MDArw{t:*}{\tau}} }

- \Infer[(SF-Coerce)]{ - %% \Jmono{\tau} \ - \Jsynth e \tau' \ - \Jcoerce {\tau'} \tau + \Infer[(SF-Inst)]{ + \Jsynth e {\MDArw{t:*}{\tau}} \ }{ - \JcheckCoerce{e}{\tau} + \JcheckCoerce{e}{\tau[\vec \tau/\vec t]} } - \end{mathpar} + + %% \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}

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