formalism: Extend definition of join for polymorphism

hazelgrove · Jun 2, 2023 · 9772c03 · 9772c03
1 parent 7cfe82c
commit 9772c03
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -87,6 +87,14 @@ \subsubsection{Unmarked types}
   }
 \end{mathpar}
 
+\judgbox{\ensuremath{\TJoin{\TMV_1}{\TMV_2}}} is a \emph{partial} metafunction defined as follows:
+%
+\[\begin{array}{rcl}
+  & \vdots & \\
+  \joinsTo{(\TForall{\TVarMV}{\TMV})}{(\TForall{\TVarMV}{\TMV'})}{\TForall{\TVarMV}{(\TJoin{\TMV}{\TMV'})}} \\
+  \joinsTo{\TVarMV}{\TVarMV}{\TVarMV} \\
+\end{array}\]
+
 \subsubsection{Type marking}
 \judgbox{\ensuremath{\tvarCtxTypeMarkedInto{\tvarCtx}{\TMV}{\MTMV}}} $\TMV$ is marked into $\MTMV$
 %
@@ -231,6 +239,16 @@ \subsubsection{Marked types}
   }
 \end{mathpar}
 
+\judgbox{\ensuremath{\MTJoin{\MTMV_1}{\MTMV_2}}} is a \emph{partial} metafunction defined as follows:
+%
+\[\begin{array}{rcl}
+  & \vdots & \\
+  \joinsTo{(\MTForall{\MTVarMV}{\MTMV})}{(\MTForall{\MTVarMV}{\MTMV'})}{\MTForall{\MTVarMV}{(\MTJoin{\MTMV}{\MTMV'})}} \\
+  \joinsTo{\MTVarMV}{\MTVarMV}{\MTVarMV} \\
+  \joinsTo{\MTUnbound{\MTVarMV}}{\MTMV}{\MTUnbound{\MTVarMV}} \\
+  \joinsTo{\MTMV}{\MTUnbound{\MTVarMV}}{\MTUnbound{\MTVarMV}} \\
+\end{array}\]
+
 \judgbox{\ensuremath{\markless{\MTMV}}} $\MTMV$ has no marks
 %
 \begin{mathpar}

diff --git a/formalism/symbols/polymorphism.tex b/formalism/symbols/polymorphism.tex
@@ -15,6 +15,8 @@
 \newcommand{\MTMName}{{\normalfont\textsf{MType}}}
 \newcommand{\MTMV}{\ensuremath{\check{\TMV}}}
 
+\newcommand{\MTJoin}[2]{\ensuremath{\TJoin{#1}{#2}}}
+
 \newcommand{\MTUnknown}{\ensuremath{\TUnknown}}
 \newcommand{\MTNum}{\ensuremath{\TNum}}
 \newcommand{\MTBool}{\ensuremath{\TBool}}