From 81114e58136c9cb793cc018bb0e61f3307c8cb76 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Fri, 6 Jul 2018 21:55:34 -0400
Subject: [PATCH] edits
---
paper/gtt.tex | 24 ++++++++++++++----------
1 file changed, 14 insertions(+), 10 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index ab62b39..4278eba 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1576,15 +1576,18 @@ relevant definitions and facts:
$A$ and $A'$}, which consists of two complex values $x : A \vdash V'
: A'$ and $x' : A' \vdash V : A$ such that $x : A \vdash V[V'/x']
\equidyn x : A$ and $x' : A' \vdash V'[V/x] \equidyn x' : A'$.
- \item We write $\u B \cong_v \u B'$ for a \emph{computation
+ \item We write $\u B \cong_c \u B'$ for a \emph{computation
isomorphism between $\u B$ and $\u B'$}, which consists of two
- complex stacls $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
+ complex stacks $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
B' \vdash S : \u B$ such that $\bullet : \u B \vdash S[S'/x']
\equidyn \bullet : \u B$ and $\bullet' : \u B' \vdash S'[S/\bullet]
\equidyn \bullet' : \u B'$.
\end{enumerate}
\end{definition}
+FIXME: Note that an effectful isomorphism is a computation isomorphism
+between $\u F$ types and dually~\cite{levy16popl}.
+
\smallskip
\begin{lemma}[Intitial objects] ~ \label{lem:initial}
@@ -2281,8 +2284,8 @@ Dually, we have
\end{proof}
-\begin{theorem}{Functorial Casts} \label{thm:functorial-casts}
- \begin{small}
+\begin{theorem}{Cast Unique Implementation Theorem for $+,\times,\to,\with$} \label{thm:functorial-casts}
+\begin{small}
\[
\begin{array}{l}
\upcast{A_1 + A_2}{A_1' + A_2'}{s} \equidyn \caseofXthenYelseZ{s}{x_1.\inl{(\upcast{A_1}{A_1'}{x_1})}}{x_2.\inr{(\upcast{A_2}{A_2'}{x_2})}}\\
@@ -2917,7 +2920,7 @@ it seems that we cannot prove that $x : \leastdynv \vdash
\begin{theorem}[Least Dynamic Computation Type]
If $\leastdync$ is a type such that $\leastdync \ltdyn \u B$ for all $\u
-B$, and we have a terminal computation type $\top$, then $U \leastdynv
+B$, and we have a terminal computation type $\top$, then $U \leastdync
\cong_{v} U \top$.
\end{theorem}
\begin{proof}
@@ -2925,7 +2928,7 @@ We have stacks $\bullet : \top \dncast{\leastdync}{\top}{\bullet} :
\leastdync$ and $\bullet : \leastdync \vdash \{\} : \top$. The
composite at $\top$ is the identity by Lemma~\ref{lem:terminal}. However,
because $\top$ is not a strict terminal object, the dual of the above
-argument does not give a stack isomorphism $\leastdynv \cong_c \top$.
+argument does not give a stack isomorphism $\leastdync \cong_c \top$.
However, using the retract axiom, we have
\[
@@ -3038,7 +3041,7 @@ define their universal property:
\[
{x : A' \vdash \defdncast{A}{A'}{x} \ltdyn x : A \ltdyn A'}
\qquad
- {x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \dncast{A}{A'} x' : A}
+ {x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \defdncast{A}{A'} x' : A}
\]
\end{definition}
@@ -3049,8 +3052,9 @@ upcasts/downcasts, the analogues of these theorems hold for computation
upcasts and value downcasts as well.
Some value downcasts and computation upcasts do exist, leading to a
-characterization of the casts for the monad/comonad of $F \dashv U$:
-\begin{theorem}[Monadic/Comonadic Casts] \label{thm:monadic-comonadic-casts}
+characterization of the casts for the monad $U \u F A$ and comonad $\u F
+U \u B$ of $F \dashv U$:
+\begin{theorem}[Cast Unique Implementation Theorem for $U \u F, \u F U$] \label{thm:monadic-comonadic-casts}
Suppose $A \ltdyn A'$ and $\u B \ltdyn \u B'$.
\begin{enumerate}
\item $\bullet : \u F A \vdash
@@ -3372,7 +3376,7 @@ universal property already existing).
\subsection{Equidynamic Types are Isomorphic}
-\begin{theorem}
+\begin{theorem}[Equidynamism implies Isomorphism]
\begin{enumerate}
\item
If $A \ltdyn A'$ and $A' \ltdyn A$ then $A \cong_v A'$.
--
GitLab