note that the enriched effect calculus types don't seem to work

gcbpv.tex

@@ -737,9 +737,11 @@ and vice-versa the upcast for the product under a $U$.
   \caption{Binary Sum and Binary Computation Product Contract Uniqueness Theorems}
 \end{figure}
 
-\subsection{Multiplicatives: Value Products and Functions}
+\subsection{Nice Multiplicatives: Value Products and Functions}
 
-Next, we consider the multiplicative connectives.
+Next, we consider the two ``nice'' multiplicative connectives ($\u F$
+and $U$ are also multiplicatives but they are ``bad'' because they
+don't have a uniqueness principle for their casts).
 %
 L
 \begin{figure}[H]
@@ -951,6 +953,13 @@ U(p)$ and again the downcast retracts the upcast $U(p) \circ e = id_{U
 
 Next, we will use poset CBPV as a metalanguage and compile GCBPV into
 poset CBPV with recursive types.
+%
+As a domain equation we can write this as a pair of mutually recursive equations:
+
+\begin{mathpar}
+  \dynv = 1 + (\dynv \times \dynv) + (\dynv + \dynv) + U \dync\\
+  \dync = (\dync \wedge \dync) \wedge (\dynv \to \dync) \wedge \u F \dynv
+\end{mathpar}
 
 \begin{mathpar}
   \dynv(X, \u Y) = 1 + (X \times X) + (X + X) + U \u Y
@@ -996,6 +1005,121 @@ Note that these both satisfy adjunction and retraction.
   %% {{\lett y = \dncast{\u F T}{\u F \dynv}\ret x; \ret \roll\sigma_T y \ltdyn \ret x}}
 \end{mathpar}
 
+\section{Call by Value $\ltdyn$ Call by Name}
+
+Can we model the idea that ``call by value errors more than call by
+name'' using type dynamism/ep pairs? Some basic calculations work
+out...
+
+\section{Focusing on an implementation}
+
+Call-by-push-value with complex values and stacks is odd from an
+operational perspective.
+%
+Values, rather than being simple trees built out of their
+constructors, can perform pattern matching on free variables, which
+would mean that they seemingly need ot be reduced operationally, when
+they are expected to be inert.
+%
+Dually, stacks, rather than being simple composites of
+\emph{destructors}, can also consist of $\lambda$s and code tuples,
+which are expected to \emph{delay} evaluation of their bodies in an
+operational semantics, whereas they are expected to \emph{force} the
+evaluation of the term plugged into the hole.
+%
+Levy resolves these seeming oddities by showing that as long as the
+values and stacks occur inside a larger term, the ``complex'' portions
+can be \emph{compiled away}.
+%
+Today, many years later, with the benefit of much hindsight, we can
+see Levy's proof as an application of the method of \emph{focusing}.
+
+Here we adapt that proof to get an operational semantics for
+\emph{Gradual} CBPV.
+
+TODO
+
+\section{The Notes we Don't Play}
+
+From a ``completionist'' perspective, call-by-push-value is missing
+some interesting connectives that are easy to define.
+%
+When added to call-by-push-value, the language is called the enriched
+effect calculus (EEC) and has been studied extensively (cite).
+
+First, there are 3 missing multiplicative connectives: the pure
+function space $A \Rightarrow A'$, linear function space $\u B
+\multimap \u B'$ and tensor product of a value and computation type $A
+\otimes \u B$.
+%
+Since they are problematic I will only describe their sorts and their
+sequent calculus invertible rule:
+
+\begin{mathpar}
+  \inferrule
+  {A \vtype \and A' \vtype}
+  {A \Rightarrow A' \vtype}
+
+  \inferrule
+  {\Gamma, A \vdash^V A'}
+  {\Gamma \vdash^V A \Rightarrow A'}
+
+  \inferrule
+  {\u B \ctype \and \u B' \ctype}
+  {\u B \multimap \u B' \vtype}
+
+  \inferrule
+  {\Gamma \pipe \u B \vdash \u B'}
+  {\Gamma \vdash \u B \multimap \u B'}
+
+  \inferrule
+  {A \vtype \and \u B \ctype}
+  {A \otimes \u B \ctype}
+
+  \inferrule
+  {\Gamma, A \pipe \u B \vdash \u C}
+  {\Gamma \pipe A \otimes \u B \vdash \u C}
+\end{mathpar}
+
+First, they are ``boundary-crossing'' connectives in that they each
+have a \emph{covariant} argument whose sort is different from the sort
+of the constructor or a \emph{contravariant} argument whose sort is
+the same as the constructor.
+%
+The pure function space has a contravariant argument of the same sort,
+the linear function space has a covariant computation type argument
+while it is a value type and the value-computation tensor has a
+covariant value type argument while it is a computation type.
+
+Second, from the perspective of our focusing operational semantics,
+each of them violates the rule of our focusing system that the only
+negative value type is $U$ and the only positive computation type is
+$\u F$.
+%
+Note that this is similar to but not the same as the boundary crossing
+rule, and there are some \emph{additives} that we violate the focusing
+restriction but not the boundary-crossing restriction: the negative
+value product and the positive computation sum, which we show now.
+
+\begin{mathpar}
+  \inferrule
+  {A \vtype \and A' \vtype}
+  {A \& A' \vtype}
+
+  \inferrule
+  {\Gamma \vdash A \and \Gamma \vdash A'}
+  {\Gamma \vdash A \& A'}
+
+  \inferrule
+  {\u B \ctype \and \u B' \ctype}
+  {\u B \oplus \u B' \ctype}
+
+  \inferrule
+  {{\Gamma \pipe \u B \vdash \u C} \and
+  {\Gamma \pipe \u B' \vdash \u C}}
+  {\Gamma \pipe \u B \oplus \u B' \vdash \u C}
+\end{mathpar}
+
 \end{document}
 
 %% Local Variables: