Tap

paper.tex

@@ -4919,19 +4919,33 @@ \subsubsection{Substructural Types and Effects}
 consider how we could support substructural, and in particular linear, \emph{types}. Categorically,
 this corresponds to weakening the requirement that our base category be cartesian, instead requiring
 only a symmetric monoidal category; the resulting generalization of a Freyd category is called an
-\emph{effectful category} by \citet{promonad}. We have made siginificant progress towards
-generalizing both our effect system and our type system to support substructruality.
-
-\subsubsection{Enriched Categories}
-
-\TODO{this}
-
-\begin{enumerate}
-  \item ...
-\end{enumerate}
+\emph{effectful category} by \citet{promonad}. Generalizing both our effect system and our type
+system to support substructruality is ongoing work.
+
+\subsubsection{Refinement and Enrichment}
+
+Throughout this work, we have focused on the notion of program \emph{equivalence}
+$\lbeq{\Gamma}{r}{r'}{\ms{L}}$. In many settings, especially when considering the nondeterminism and
+concurrency, we would also like to study program \emph{refinement} $\haslb{\Gamma}{r \sqsubseteq
+r'}{\ms{L}}$. Semantically, this corresponds to an enrichment of our model in the category of
+partial orders; it would not take too many changes to support this in our language as-is. We may
+also consider how our syntax could be extended to support explicit parallelism and how we could
+reflect the corresponding algebraic laws (as given in, e.g., \citet{hoare-parallel-14}), such as
+\begin{equation}
+  (P \parallel Q) ; (R \parallel S) \sqsubseteq (P ; R) \parallel (Q ; S)
+\end{equation}
+in our equational theory. More generally, we can consider enrichment with further structures, such
+as distributive lattices and dcpos, and the language features these correspond to, such as
+nondeterministic choice between programs $P \lor C$. These features are particularly interesting
+from the perspective of programs as \emph{specifications}, since there is the potential of
+representing complex specifications as SSA.
 
 \subsubsection{Guarded Iteration}
 
+Elgot categories and monads were introduced in \citet{elgot-elgot-75}, and subsequently formalized
+in \citet{adamek-elgot-11}. \citet{coinductive-resumption-levy-goncharov-19} generalize Elgot
+categories to \emph{guarded Elgot categories}, to support partial non-unique iteration.
+
 \TODO{this}
 
 \begin{enumerate}