formalism: Add back polymorphism stuff

hazelgrove · Jun 1, 2023 · 99623b1 · 99623b1
1 parent 8bc9bfe
commit 99623b1
Show file tree

Hide file tree

Showing 2 changed files with 114 additions and 0 deletions.
diff --git a/formalism/marked.tex b/formalism/marked.tex
@@ -952,5 +952,6 @@ \subsubsection{Localize to first}
 \end{mathpar}
 
 \input{patterned}
+\input{polymorphism}
 
 \end{document}
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -0,0 +1,113 @@
+\subsection{Extension: polymorphism}
+
+\subsubsection{Syntax}
+\[\begin{array}{rrcl}
+  \TMName  & \TMV  & \Coloneqq & \cdots \mid \TVarMV \mid \TForall{\TVarMV}{\TMV} \\
+  \EMName  & \EMV  & \Coloneqq & \cdots \mid \ETypeLam{\TVarMV}{\EMV} \mid \ETypeAp{\EMV}{\TMV} \\
+  \ECMName & \ECMV & \Coloneqq & \cdots \mid \ECTypeLam{\TVarMV}{\ECMV} \mid \ECTypeAp{\ECMV}{\TMV}
+\end{array}\]
+
+\subsubsection{Types}
+\judgbox{\ensuremath{\tvarCtxWF{\tvarCtx}{\TMV}}} $\TMV$ is well-formed
+%
+\begin{mathpar}
+  \inferrule[TWFUnknown]{ }{
+    \tvarCtxWF{\tvarCtx}{\TUnknown}
+  }
+
+  \inferrule[TWFNum]{ }{
+    \tvarCtxWF{\tvarCtx}{\TNum}
+  }
+
+  \inferrule[TWFBool]{ }{
+    \tvarCtxWF{\tvarCtx}{\TBool}
+  }
+
+  \inferrule[TWFArr]{
+    \tvarCtxWF{\tvarCtx}{\TMV_1} \\
+    \tvarCtxWF{\tvarCtx}{\TMV_2}
+  }{
+    \tvarCtxWF{\tvarCtx}{\TArrow{\TMV_1}{\TMV_2}}
+  }
+
+  \inferrule[TWFProd]{
+    \tvarCtxWF{\tvarCtx}{\TMV_1} \\
+    \tvarCtxWF{\tvarCtx}{\TMV_2}
+  }{
+    \tvarCtxWF{\tvarCtx}{\TProd{\TMV_1}{\TMV_2}}
+  }
+
+  \inferrule[TWFVar]{
+    \inTvarCtx{\tvarCtx}{\TVarMV}
+  }{
+    \tvarCtxWF{\tvarCtx}{\TVarMV}
+  }
+
+  \inferrule[TWFForall]{
+    \tvarCtxWF{\extendTvarCtx{\tvarCtx}{\TVarMV}}{\TMV}
+  }{
+    \tvarCtxWF{\tvarCtx}{\TForall{\TVarMV}{\TMV}}
+  }
+\end{mathpar}
+
+\judgbox{\ensuremath{\tvarCtxConsistent{\tvarCtx}{\TMV_1}{\TMV_2}}} $\TMV_1$ and $\TMV_2$ are consistent
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[TCVar]{
+    \inTvarCtx{\tvarCtx}{\TVarMV}
+  }{
+    \tvarCtxConsistent{\tvarCtx}{\TVarMV}{\TVarMV}
+  }
+
+  \inferrule[TCForall]{
+    \tvarCtxConsistent{\extendTvarCtx{\tvarCtx}{\TVarMV}}{\TMV}{\TMV'}
+  }{
+    \tvarCtxConsistent{\tvarCtx}{\TForall{\TVarMV}{\TMV}}{\TForall{\TVarMV}{\TMV'}}
+  }
+\end{mathpar}
+
+\subsubsection{Unmarked expressions}
+\judgbox{\ensuremath{\bothCtxSynTypeU{\tvarCtx}{\ctx}{\EMV}{\TMV}}} $\EMV$ synthesizes type $\TMV$
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[USTypeLam]{
+    \bothCtxSynTypeU{\extendTvarCtx{\tvarCtx}{\TVarMV}}{\ctx}{\EMV}{\TMV}
+  }{
+    \bothCtxSynTypeU{\tvarCtx}{\ctx}{\ETypeLam{\TVarMV}{\EMV}}{\TForall{\TVarMV}{\TMV}}
+  }
+
+  \inferrule[USTypeAp]{
+    \bothCtxSynTypeU{\tvarCtx}{\ctx}{\EMV}{\TMV} \\
+    \tvarCtxWF{\tvarCtx}{\TMV_2} \\
+    \matchedForall{\TMV}{\TVarMV}{\TMV_1}
+  }{
+    \bothCtxSynTypeU{\tvarCtx}{\ctx}{\ETypeAp{\EMV}{\TMV_2}}{\subst{\TMV_1}{\TMV_2}{\TVarMV}}
+  }
+\end{mathpar}
+
+\judgbox{\ensuremath{\bothCtxAnaTypeU{\tvarCtx}{\ctx}{\EMV}{\TMV}}} $\EMV$ analyzes against type $\TMV$
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[UATypeLam]{
+    \matchedForall{\TMV}{\TVarMV}{\TMV'} \\
+    \bothCtxAnaTypeU{\extendTvarCtx{\tvarCtx}{\TVarMV}}{\ctx}{\EMV}{\TMV'}
+  }{
+    \bothCtxAnaTypeU{\tvarCtx}{\ctx}{\ETypeLam{\TVarMV}{\EMV}}{\TMV}
+  }
+\end{mathpar}
+
+\judgbox{\ensuremath{\subsumable{\EMV}}} $\EMV$ is subsumable
+%
+\begin{mathpar}
+  \cdots
+
+  \inferrule[USuTypeAp]{ }{
+    \subsumable{\ETypeAp{\EMV}{\TMV}}
+  }
+\end{mathpar}