[Git][monnier/typer][report/hmdup] - - Typer

1 Jul 2020


      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.





    