[Git][monnier/typer][report/hmdup] 2 commits: - - Typer

28 Jui 2020


      Stefan pushed to branch report/hmdup at Stefan / Typer
Commits:
7a1a6d26 by Stefan Monnier at 2020-06-28T16:07:26-04:00
-
- - - - -
103c6743 by Stefan Monnier at 2020-06-28T16:07:52-04:00
-
- - - - -
1 changed file:
- paper.tex
Changes:
=====================================
paper.tex
=====================================
@@ -90,6 +90,7 @@
 \newcommand \Comment[1] {}
\newcommand \FIXME[1] {\fbox{\parbox{\columnwidth}{{\color{red}{¡FIXME!}} #1}}}
+\newcommand \FIXMEs[1] {\fbox{{\color{red}{\text{¡FIXME!}}} #1}}
 %% \newtheorem{theorem}{Theorem}[section]
 %% \newtheorem{lemma}[theorem]{Lemma}
 \theoremstyle{plain}
@@ -313,6 +314,7 @@ minimizing the amount of type annotations was secondary to the design.
 \newcommand \DArw [3] {\forall #1 : #2 . #3}
 \newcommand \Let [3] {\kw{let}~#1=#2~\kw{in}~#3}
 \newcommand \MDArw [2] {\forall \overrightarrow{#1} . #2}
+\newcommand \HasType [2] {#1 : #2}
\newcommand \Jcheck [3][\Gamma] {#1 \vdash #2 \Leftarrow #3}
 \newcommand \Jsynth [3][\Gamma] {#1 \vdash #2 \Rightarrow #3}
@@ -447,7 +449,7 @@ $u_2$ was instantiated to.
       \Jcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}}
     }
-    \Infer{\Jcheck e \tau}{\Jsynth{e : \tau}{\tau}}
+    \Infer{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}}
\Infer{\Jsynth e \tau' \ \tau = \tau'}{\Jcheck{e}{\tau}}
     %%
@@ -498,7 +500,7 @@ type check the $\lambda$-calculus.
       \Jcheck{\Lam x e}{\tau}
     }
     \\
-    \Infer{\Jcheck e \tau}{\Jsynth{e : \tau}{\tau}}
+    \Infer{\Jcheck e \tau}{\Jsynth{\HasType{e}{\tau}}{\tau}}
\Infer{\Jfresh{\Meta{u}} \ \Jcheck e {\Meta{u}}}{\Jsynth e {\Meta{u}}}
@@ -521,9 +523,9 @@ a $\Lam{x}{e}$.
\section{System F}
-\newcommand \JsynthCoerce [3][\Gamma] {#1 \vdash #2 \Longrightarrow #3}
+%% \newcommand \JsynthCoerce [3][\Gamma] {#1 \vdash #2 \Longrightarrow #3}
 \newcommand \JcheckCoerce [3][\Gamma] {#1 \vdash #2 \Longleftarrow #3}
-\newcommand \Jmono [1] {\kw{monotype}(#1)}
+%% \newcommand \Jmono [1] {\kw{monotype}(#1)}
\begin{figure}
   \begin{mathpar}
@@ -564,7 +566,7 @@ a $\Lam{x}{e}$.
     \Infer{
       \JcheckCoerce e \tau
     }{
-      \Jsynth{e : \tau}{\tau}
+      \Jsynth{\HasType{e}{\tau}}{\tau}
     }
\Infer{
@@ -652,7 +654,7 @@ a $\Lam{x}{e}$.
 %%     \Infer{
 %%       \Jcheck e \tau
 %%     }{
-%%       \Jsynth{e : \tau}{\tau}
+%%       \Jsynth{\HasType{e}{\tau}}{\tau}
 %%     }
%%     \Infer{
@@ -694,7 +696,8 @@ Our inference algorithm takes inspiration from bidirectional type systems to
 try and make better use of that information.
The only change to the syntax of the language is the addition of the form
-$e : \tau$.  While the specific form of the type annotations is not a primary
+$\HasType{e}{\tau}$.  While the specific form of the type annotations is not
+a primary
 concern for us, we did want to avoid ``non-standard'' annotations such as
 the freeze annotation of FreezeML~\cite{Emrich20} or the constrained
 quantifiers of \MLF:
@@ -703,7 +706,7 @@ quantifiers of \MLF:
   \begin{array}{cc@{;;::=;;}l}
     \textit{(types)} & \tau & t ~|~ \Meta{u} ~|~ \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}
-    ~|~ e : \tau \
+    ~|~ \HasType{e}{\tau} \
     \textit{(context)} & \Gamma & \bullet ~|~ \Gamma,x:\tau ~|~ \Gamma,t:* \
     %% \textit{(substitutions)} & \sigma & \textsf{id} ~|~ \sigma,\Meta{u}\mapsto\tau 
   \end{array}
@@ -718,7 +721,7 @@ just a shorthand for a pair of rules, one that checks and one that synthesizes.
 The first three lines are equivalent to the base Hindley-Milner system
 presented earlier.  The two differences are: (1) the instantiation of
 polymorphic terms has now been moved from the variable rule to its own
-$\JsynthCoerce{e}{\tau}$ judgment and it is now applied less eagerly; (2) the
+$\JcheckCoerce{e}{\tau}$ judgment and it is now applied less eagerly; (2) the
 application rule does not unify the synthesized type of the argument with
 the type expected by the function any more but instead it \emph{checks} the
 type of the argument against that expected by the function.
@@ -802,42 +805,91 @@ incompatible with things like value polymorphism.
\FIXME{Adapt the rules to the new algorithm}
-\newcommand \JEcheck [4][\Gamma] {#1 \vdash #2 : #3 \Rightarrow #4}
-\newcommand \JEsynth [4][\Gamma] {#1 \vdash #2 \Rightarrow #4 : #3}
-\newcommand \JEsynthMono [4][\Gamma] {#1 \vdash #2 \Longrightarrow #4 : #3}
-\newcommand \JEpoly [4][\Gamma] {#1 \vdash #2 \Leftrightarrow #4 : #3}
-
 \begin{figure}
   \begin{mathpar}
     \Infer{
       \Gamma(x) = \tau
     }{
-      \JEsynth{x}{\tau}{x}
+      \Jsynth{x}{\tau}
     }
\Infer{
-      \JEsynth{x}{\MDArw {t:*} \tau}{E} \
-      \Jfresh {\vec u}
+      \Jsynth{e_1}{\tau_1} \
+      \tau_1' = \kw{gen}(\Gamma,\tau_1) \
+      \Jpoly[\Gamma,x:\tau_1']{e_2}{\tau}
     }{
-      \JEsynthMono{x}{\tau[\vec u/\vec t]}{E[\vec u]}
+      \Jpoly{\Let x {e_1}{e_2}}{\tau}
     }
\Infer{
-      %% \Jmono{\tau} \
-      \JEsynthMono e {\tau'} {E}\
-      \Junify \tau {\tau'}
+      %% \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}
     }{
-      \JEcheck{e}{\tau} {E}
+      \Jsynth{e_1~e_2}{u_2}
     }
\Infer{
-      %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \
-      \JEsynthMono{e_1}{\tau}{E_1} \
-      \Jfresh{u_1,u_2} \
+      \Jfresh{u_1, u_2} \
+      %% FIXME: Introduce polymorphism?!
       \Junify{\tau}{\Arw{u_1}{u_2}} \
-      \JEcheck{e_2}{u_1}{E_2}
+      \JcheckCoerce[\Gamma,x:u_1] e {u_2}
     }{
-      \JEsynth{e_1~e_2}{u_2}{E_1~E_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}
+
+\begin{figure}
+  \begin{mathpar}
+    \Infer{
+      \Gamma(x) = \tau
+    }{
+      \JEsynth{x}{\tau}{x}
     }
\Infer{
@@ -845,42 +897,53 @@ incompatible with things like value polymorphism.
       \overrightarrow{t:*} = \kw{fmv}(\Gamma,\tau_1) \
       \JEpoly[\Gamma,x:\MDArw{t:*}{\tau_1}]{e_2}{\tau}{E_2}
     }{
-      \JEpoly{\Let x {e_1}{e_2}}{\tau}{\Let x {\TLam{t:*}{E_1}}{E_2}}
+      \JEpoly{\Let x {e_1}{e_2}}{\tau}{
+        \Let {x} {\TLam{\overrightarrow{t:*}}{E_1}}{E_2}}
     }
\Infer{
-      \Jfresh u \
-      \JEsynthMono[\Gamma,x:u] e {\tau}{E}
+      %% \Jsynth{e_1}{\Arw{\tau_1}{\tau_2}} \
+      \Jfresh{u_1,u_2} \
+      \JEcheckCoerce{e_1}{\Arw{u_1}{u_2}}{E_1} \
+      \JEcheck{e_2}{u_1}{E_2}
     }{
-      \JEsynth{\Lam x e}{\Arw{u}{\tau}}{\Lam{x:u}{E}}
+      \JEsynth{e_1~e_2}{u_2}{E_1~E_2}
     }
-    %%
-    \\
-    %%
+
     \Infer{
-      \JEcheck e \tau E
+      \Jfresh {\Meta{u_1},\Meta{u_2}} \
+      \Junify {\tau}{\Arw{\Meta{u_1}}{\Meta{u_2}}} \
+      \JEcheckCoerce[\Gamma,x:\Meta{u_1}]{e}{\Meta{u_2}}{E}
     }{
-      \JEsynth{e : \tau}{\tau}{E}
+      \JEcheck{\Lam x e}{\tau}{\Lam{x:\Meta{u_1}}{E}}
     }
\Infer{
-      \JEcheck[\Gamma,x:\tau_1] e {\tau_2} {E}
+      \JEcheckCoerce e \tau E
     }{
-      \JEcheck{\Lam x e}{\Arw{\tau_1}{\tau_2}} {\Lam{x:\tau_1}{E}}
+      \JEsynth{\HasType{e}{\tau}}{\tau}{E}
+    }
+
+    \Infer{
+      \Jfresh{\Meta{u}} \ \JEcheck{e}{\Meta{u}}{E}
+    }{
+      %% FIXME: Make it \JsynthCoerce?
+      \JEsynth{e}{\Meta{u}}{E}
     }
-    %% \Infer{
-    %%   \Gamma(x) = \tau' \ \Junify{\tau'}{\DArw{t}{*}{\tau}}
-    %% }{
-    %%   \Jcheck{x}{\DArw{t}{*}{\tau}}
-    %% }
-    %%
     \Infer{
-      \JEcheck[\Gamma,t:*] e {\tau} {E}
+      %% \Jmono{\tau} \
+      \JEsynth{e}{\tau'}{E} \
+      \FIXMEs{E' = \Jcoerce {\tau'} \tau}
     }{
-      \JEcheck{e}{\DArw{t}{*}{\tau}} {\TLam{t:*}E}
+      \JEcheckCoerce{e}{\tau}{E'}
     }
+    \Infer{
+      \JEcheck[\Gamma,\overrightarrow{t:*}] e {\tau}{E}
+    }{
+      \JEcheckCoerce{e}{\MDArw{t:*}{\tau}}{\TLam{\overrightarrow{t:*}}{E}}
+    }
   \end{mathpar}
   \caption{Elaboration for System F}
   \label{fig:elab-system-f}
@@ -902,8 +965,9 @@ our language is extended as follows:
 \begin{displaymath}
   \begin{array}{cc@{;;::=;;}l}
     \textit{(types)} & \tau & t ~|~ \Meta{u} ~|~ \Arw{\tau_1}{\tau_2} ~|~ \DArw t * \tau \
-    \textit{(terms)} & e & x ~|~ \Meta{u} ~|~ \Lam x e ~|~ e_1~e_2 ~|~ \Let x {e_1} {e_2}
-    ~|~ e : \tau \
+    \textit{(terms)} & e & x ~|~ \Meta{u} ~|~ \Lam x e ~|~ e_1~e_2 ~|~ \Let
+    x {e_1} {e_2}
+    ~|~ \HasType{e}{\tau} \
     \textit{(context)} & \Gamma & \bullet ~|~ \Gamma,x:\tau ~|~ \Gamma,t:* \
     %% \textit{(substitutions)} & \sigma & \textsf{id} ~|~ \sigma,\Meta{u}\mapsto\tau 
   \end{array}
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/44ef07b166dcff92504793feab10e6427...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/44ef07b166dcff92504793feab10e6427...
You're receiving this email because of your account on gitlab.com.





    