formalism: Indicate domain/codomain for all metafunctions

hazelgrove · Oct 10, 2023 · 145f154 · 145f154
1 parent bdb4e6f
commit 145f154
Show file tree

Hide file tree

Showing 4 changed files with 14 additions and 12 deletions.
diff --git a/formalism/marked.tex b/formalism/marked.tex
@@ -95,7 +95,7 @@ \subsection{Types}
   }
 \end{mathpar} \\
 
-\judgbox{\ensuremath{\TMeet{\TMV_1}{\TMV_2}}} is a \emph{partial} metafunction defined as follows:
+\judgbox{\ensuremath{\TMeet{\TMV_1}{\TMV_2}}} is a \emph{partial} metafunction $\TMName \times \TMName \rightharpoonup \TMName$ defined as follows:
 %
 \newcommand{\meetsToRow}[3]{\ensuremath{\TMeet{#1}{#2} & = & #3}}
 \[\begin{array}{rcl}
@@ -822,7 +822,7 @@ \subsection{Marked expressions}
 
 \subsection{Mark erasure}
 \label{sec:marked-mark-erasure}
-$\judgbox{\erase{\ECMV}}$ is a metafunction defined as follows:
+$\judgbox{\erase{\ECMV}}$ is a metafunction $\ECMName \to \EMName$ defined as follows:
 %
 \newcommand{\erasesToRow}[2]{\erase{#1} & = & #2}
 \[\begin{array}{rcl}

diff --git a/formalism/patterned.tex b/formalism/patterned.tex
@@ -52,7 +52,7 @@ \subsection{Types}
   }
 \end{mathpar}
 
-\judgbox{\ensuremath{\TMeet{\TMV_1}{\TMV_2}}} is a \emph{partial} metafunction defined as follows:
+\judgbox{\ensuremath{\TMeet{\TMV_1}{\TMV_2}}} is a \emph{partial} metafunction $\TMName \times \TMName \rightharpoonup \TMName$ defined as follows:
 %
 \newcommand{\meetsToRow}[3]{\ensuremath{\TMeet{#1}{#2} & = & #3}}
 \[\begin{array}{rcl}
@@ -288,11 +288,10 @@ \subsection{Marked patterns}
 
 \subsection{Pattern mark erasure}
 \label{sec:patterned-pattern-mark-erasure}
-$\judgbox{\erase{\PCMV}}$ is a metafunction defined as follows:
+$\judgbox{\erase{\PCMV}}$ is a metafunction $\PCMName \to \PMName$ defined as follows:
 %
 \newcommand{\erasesToRow}[2]{\erase{#1} & = & #2}
 \[\begin{array}{rcl}
-  & \vdots & \\
   \erasesToRow{\PCWild}{\PWild} \\
   \erasesToRow{\PCVar{x}}{\PVar{x}} \\
   \erasesToRow{\PCPair{\PCMV_1}{\PCMV_2}}{\PPair{\erase{\PCMV_1}}{\erase{\PCMV_2}}} \\
@@ -423,7 +422,7 @@ \subsection{Marked expressions}
 
 \subsection{Mark erasure}
 \label{sec:patterned-mark-erasure}
-$\judgbox{\erase{\ECMV}}$ is a metafunction defined as follows:
+$\judgbox{\erase{\ECMV}}$ is a metafunction $\ECMName \to \EMName$ defined as follows:
 %
 \[\begin{array}{rcl}
   & \vdots & \\

diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -114,7 +114,7 @@ \subsection{Unmarked types}
   }
 \end{mathpar}
 
-\judgbox{\ensuremath{\TMeet{\TMV_1}{\TMV_2}}} is a \emph{partial} metafunction defined as follows:
+\judgbox{\ensuremath{\TMeet{\TMV_1}{\TMV_2}}} is a \emph{partial} metafunction $\TMName \times \TMName \rightharpoonup \TMName$ defined as follows:
 %
 \newcommand{\meetsToRow}[3]{\ensuremath{\TMeet{#1}{#2} & = & #3}}
 \[\begin{array}{rcl}
@@ -123,7 +123,7 @@ \subsection{Unmarked types}
   \meetsToRow{\TVarMV}{\TVarMV}{\TVarMV} \\
 \end{array}\]
 
-\judgbox{\ensuremath{\subst{\TMV_1}{\TMV_2}{\TVarMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\subst{\TMV_1}{\TMV_2}{\TVarMV}}} is a metafunction $\TMName \times \TMName \times \TVarMName \to \TMName$ defined as follows:
 %
 \newcommand{\substToRow}[4]{\ensuremath{\subst{#1}{#2}{#3} & = & #4}}
 \[\begin{array}{rcll}
@@ -284,7 +284,7 @@ \subsection{Marked types}
   }
 \end{mathpar}
 
-\judgbox{\ensuremath{\MTMeet{\MTMV_1}{\MTMV_2}}} is a \emph{partial} metafunction defined as follows:
+\judgbox{\ensuremath{\MTMeet{\MTMV_1}{\MTMV_2}}} is a \emph{partial} metafunction $\MTMName \times \MTMName \rightharpoonup \MTMName$ defined as follows:
 %
 \[\begin{array}{rcl}
   & \vdots & \\
@@ -294,7 +294,7 @@ \subsection{Marked types}
   \meetsToRow{\MTMV}{\MTFree{\MTVarMV}}{\MTMV} \\
 \end{array}\]
 
-\judgbox{\ensuremath{\subst{\MTMV_1}{\MTMV_2}{\MTVarMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\subst{\MTMV_1}{\MTMV_2}{\MTVarMV}}} is a metafunction $\MTMName \times \MTMName \times \MTVarMName \to \MTMName$ defined as follows:
 %
 \[\begin{array}{rcll}
   \substToRow{\MTUnknown}{\MTMV}{\MTVarMV}{\MTUnknown} \\
@@ -351,7 +351,7 @@ \subsection{Marked types}
 
 \subsection{Type mark erasure}
 \label{sec:polymorphism-type-mark-erasure}
-\judgbox{\ensuremath{\erase{\MTMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\erase{\MTMV}}} is a metafunction $\MTMName \to \TMName$ defined as follows:
 %
 \newcommand{\erasesToRow}[2]{\erase{#1} & = & #2}
 \[\begin{array}{rcl}
@@ -545,7 +545,7 @@ \subsection{Marked expressions}
 
 \subsection{Mark erasure}
 \label{sec:polymorphism-mark-erasure}
-\judgbox{\ensuremath{\erase{\ECMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\erase{\ECMV}}} is a metafunction $\ECMName \to \EMName$ defined as follows:
 %
 \[\begin{array}{rcl}
   & \vdots & \\

diff --git a/formalism/symbols/polymorphism.tex b/formalism/symbols/polymorphism.tex
@@ -5,14 +5,17 @@
 %
 
 % syntax
+\newcommand{\TVarMName}{{\normalfont\textsf{TypeVar}}}
 \newcommand{\TVarMV}{\ensuremath{\alpha}}
+
 \newcommand{\TForall}[2]{\ensuremath{\forall #1. ~#2}}
 
 % substitution
 \newcommand{\subst}[3]{\ensuremath{#1[#2 / #3]}}
 
 % marked
 \newcommand{\MTMName}{{\normalfont\textsf{MType}}}
+\newcommand{\MTVarMName}{{\normalfont\textsf{MTypeVar}}}
 \newcommand{\MTMV}{\ensuremath{\check{\TMV}}}
 
 \newcommand{\MTMeet}[2]{\ensuremath{\TMeet{#1}{#2}}}