formalism: Add synthetic unmarked polymorphic expression typing rules

hazelgrove · Jun 1, 2023 · d0b4ddc · d0b4ddc
1 parent ab27750
commit d0b4ddc
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 0 deletions.
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -273,3 +273,32 @@ \subsubsection{Unmarked expressions}
     \subsumable{\ETypeAp{\EMV}{\TMV}}
   }
 \end{mathpar}
+
+\subsubsection{Marked expressions}
+\judgbox{\ensuremath{\bothCtxSynTypeM{\tvarCtx}{\ctx}{\EMV}{\TMV}}} $\EMV$ synthesizes type $\TMV$
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[MSTypeLam]{
+    \bothCtxSynTypeM{\extendTvarCtx{\tvarCtx}{\MTVarMV}}{\ctx}{\ECMV}{\MTMV}
+  }{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeLam{\MTVarMV}{\ECMV}}{\MTForall{\MTVarMV}{\MTMV}}
+  }
+
+  \inferrule[MSTypeAp1]{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECMV}{\MTMV} \\
+    \tvarCtxWFM{\tvarCtx}{\MTMV_2} \\
+    \matchedForall{\MTMV}{\MTVarMV}{\MTMV_1}
+  }{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeAp{\ECMV}{\MTMV_2}}{\subst{\MTMV_1}{\MTMV_2}{\MTVarMV}}
+  }
+
+  \inferrule[MSTypeAp2]{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECMV}{\MTMV} \\
+    \tvarCtxWFM{\tvarCtx}{\MTMV'} \\
+    \notMatchedForall{\MTMV}
+  }{
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeAp{\ECMV}{\MTMV'}}{\MTUnknown}
+  }
+\end{mathpar}
diff --git a/formalism/symbols/polymorphism.tex b/formalism/symbols/polymorphism.tex
@@ -47,8 +47,11 @@
 \newcommand{\inTvarCtx}[2]{\ensuremath{#2 \in #1}}
 \newcommand{\notInTvarCtx}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#2 \not\in #1}}}
 \newcommand{\withTvarCtx}[2]{\ensuremath{#1 \vdash #2}}
+\newcommand{\withTvarCtxNot}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#1 \centernot\vdash #2}}}
 \newcommand{\withTvarCtxU}[2]{\ensuremath{#1 \goodcolor{\colorUText}{\vdash_{\hspace{-4.25pt}\scaleto{U}{3.5pt}}} #2}}
+\newcommand{\withTvarCtxUNot}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#1 \centernot\vdash_{\hspace{-4.25pt}\scaleto{U}{3.5pt}} #2}}}
 \newcommand{\withTvarCtxM}[2]{\ensuremath{#1 \goodcolor{\colorMText}{\vdash_{\hspace{-4.25pt}\scaleto{M}{3.5pt}}} #2}}
+\newcommand{\withTvarCtxMNot}[2]{\ensuremath{\goodcolor{\colorFailSideJudge}{#1 \centernot\vdash_{\hspace{-4.25pt}\scaleto{M}{3.5pt}} #2}}}
 \newcommand{\withTvarCtxMK}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\vdash} #2}}
 
 \newcommand{\withBothCtx}[3]{\ensuremath{#1; #2 \vdash #3}}