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