formalism: Add analytic marked polymorphic expression typing rules

hazelgrove · Jun 1, 2023 · 5281aa1 · 5281aa1
1 parent 13cebb6
commit 5281aa1
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 1 deletion.
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -299,6 +299,36 @@ \subsubsection{Marked expressions}
     \tvarCtxWFM{\tvarCtx}{\MTMV'} \\
     \notMatchedForall{\MTMV}
   }{
-    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeAp{\ECMV}{\MTMV'}}{\MTUnknown}
+    \bothCtxSynTypeM{\tvarCtx}{\ctx}{\ECTypeApSynNonMatchedForall{\ECMV}{\MTMV'}}{\MTUnknown}
+  }
+\end{mathpar}
+
+\judgbox{\ensuremath{\bothCtxAnaTypeM{\tvarCtx}{\ctx}{\ECMV}{\MTMV}}} $\ECMV$ analyzes against type $\MTMV$
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[MATypeLam1]{
+    \matchedForall{\MTMV}{\MTVarMV}{\MTMV'} \\
+    \bothCtxAnaTypeM{\extendTvarCtx{\tvarCtx}{\MTVarMV}}{\ctx}{\ECMV}{\MTMV'}
+  }{
+    \bothCtxAnaTypeM{\tvarCtx}{\ctx}{\ECTypeLam{\MTVarMV}{\ECMV}}{\MTMV}
+  }
+
+  \inferrule[MATypeLam2]{
+    \notMatchedForall{\MTMV} \\
+    \bothCtxAnaTypeM{\extendTvarCtx{\tvarCtx}{\MTVarMV}}{\ctx}{\ECMV}{\MTUnknown}
+  }{
+    \bothCtxAnaTypeM{\tvarCtx}{\ctx}{\ECTypeLamAnaNonMatchedForall{\MTVarMV}{\ECMV}}{\MTMV}
+  }
+\end{mathpar}
+
+\judgbox{\ensuremath{\subsumable{\ECMV}}} $\ECMV$ is subsumable
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[MSuTypeAp]{ }{
+    \subsumable{\ECTypeAp{\ECMV}{\MTMV}}
   }
 \end{mathpar}
diff --git a/formalism/symbols/polymorphism.tex b/formalism/symbols/polymorphism.tex
@@ -39,6 +39,18 @@
 \newcommand{\ECTypeLam}[2]{\ensuremath{\Lambda #1. ~#2}}
 \newcommand{\ECTypeAp}[2]{\ensuremath{#1 ~[#2]}}
 
+\newcommand{\MRSynNonMatchedForall}{\ensuremath{\mathsmaller{\notMatchedForallRel}}}
+\newcommand{\MRAnaNonMatchedForall}{\ensuremath{\mathsmaller{\notMatchedForallRel}}}
+
+\newcommand{\ECMarkedSynNonMatchedForall}[1]{\ensuremath{\ECMarked{#1}{\MRSynNonMatchedForall}{\MRSyn}}}
+\newcommand{\ECMarkedAnaNonMatchedForall}[1]{\ensuremath{\ECMarked{#1}{\MRAnaNonMatchedForall}{\MRAna}}}
+
+\newcommand{\ECSynNonMatchedForall}[1]{\ensuremath{\ECMarkedSynNonMatchedForall{#1}}}
+\newcommand{\ECAnaNonMatchedForall}[1]{\ensuremath{\ECMarkedAnaNonMatchedForall{#1}}}
+
+\newcommand{\ECTypeApSynNonMatchedForall}[2]{\ensuremath{\ECTypeAp{\ECSynNonMatchedForall{#1}}{#2}}}
+\newcommand{\ECTypeLamAnaNonMatchedForall}[2]{\ensuremath{\ECAnaNonMatchedForall{\ECTypeLam{#1}{#2}}}}
+
 %
 % contexts
 %