From 043bf8b4764dbf0a3b0325e32d20fc6409a5f3aa Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Tue, 10 Jul 2018 16:10:07 -0400
Subject: [PATCH] sec 7

---
 paper/gtt.tex | 150 ++++++++++++++++++++++++++++----------------------
 paper/max.bib |  30 ++++++++++
 2 files changed, 115 insertions(+), 65 deletions(-)

diff --git a/paper/gtt.tex b/paper/gtt.tex
index 109d25a..b0ce0e6 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -7757,7 +7757,7 @@ The most famous application of this is to observational equivalence,
 which is the lifting of equality: $\ctxize=$, and we will show that
 $\equidyn$ proofs in GTT imply observational equivalences.
 %
-However, as shown in \cite{newahmed2018}, the graduality property is
+However, as shown in \cite{newahmed18}, the graduality property is
 defined in terms of an observational \emph{approximation} relation
 $\ltdyn$ that places $\err$ as the least element, and every other
 element as a maximal element.
@@ -7864,7 +7864,7 @@ approximation, i.e., $M \ctxize= N$ if and only if $M \ctxize\preceq
 N$ and $N \ctxize\preceq M$, and since $\preceq$ has $\diverge$ as
 a least element, we can use a step-indexed relation to prove it.
 %
-As shown in \cite{newahmed2018}, a similar trick works for error
+As shown in \cite{newahmed18}, a similar trick works for error
 approximation, but since $\ltdyn$ is \emph{not} an equivalence
 relation, we decompose it rather into two \emph{different} orderings:
 error approximation up to divergence on the left $\preceq\ltdyn$ and
@@ -8904,14 +8904,17 @@ contextual equivalence is a model of equi-dynamism.
   preorder, and commuting of conjection with contextual lifting.
 \end{longproof}
 
-\section{Discussion and Related Work}
+\section{Related Work and Discussion}
 \label{sec:related}
 
+\iflong
 \paragraph{Gradual Typing Frameworks}
+\fi
 
 Our approach to systematically producing a gradual type theory from a
 type theory is similar in spirit to ``frameworks'' for gradual typing,
-specifically AGT \cite{AGT} and the Gradualizer \cite{gradualizer}.
+specifically AGT \cite{AGT} and the Gradualizer
+\cite{gradualizer16,gradualizer17}.
 %
 Both approaches systematically produce a gradual language from a
 statically typed language, and the Gradualizer in particular has been
@@ -8930,12 +8933,11 @@ This means our approach accomplishes something quite different: their
 frameworks produce specific implementations, whereas our approach is
 about finding commonalities across different implementations.
 % AA: Perhaps the above point should also be made in the intro. 
-
-Furthermore, while both the AGT and Gradualizer approaches prove various gradual
-typing correctness theorems by construction (gradual type safety,
-conservativity, gradual guarantee), neither considers the program
-equivalences that we argued are the raison d'\^etre of gradual typing
-in the first place.
+Furthermore, while both the AGT and Gradualizer approaches prove various
+gradual typing correctness theorems by construction (gradual type
+safety, conservativity, gradual guarantee), neither considers the
+program equivalences that we argued are the raison d'\^etre of gradual
+typing in the first place.
 %
 In fact, the systems both \emph{fail} to preserve these equivalences.
 %
@@ -8951,10 +8953,9 @@ Both systems, however, fail to preserve the program
 equivalences of parametric polymorphism, and in addition fail to meet
 gradual typing criteria for stateful references.
 %
-While we have not considered these features, we have reason to believe
+While we have not yet considered these features, we have reason to believe
 that our approach will be more successful: specifically, the
-``reason'' that all of these occur 
-% AA: what occur? what is "all of these"?
+``reason'' that these violations occur
 is that they are not safety
 properties of the operational semantics, and the operational semantics
 is the only input to these frameworks.
@@ -8964,47 +8965,42 @@ polymorphism and state is to start with the rich \emph{relational
   logics} for program equivalence that have been developed for these
 features (TODO: citessss).
 
-\paragraph{Blame and Upcasts and Downcasts}
-
-We do not give a treatment of blame but our axiomatic language is
-sufficiently similar to cast calculi that it should be clear how to
-add it.
+\iflong \paragraph{Blame}
+\fi
+We do not give a treatment of blame, but our axiomatic language is
+sufficiently similar to cast calculi that it should be easy to add.
 %
 The division of casts into upcasts and downcasts naturally pairs with
-the blame soundness properties given in \cite{wadler-findler}: upcasts
+the blame soundness properties given in \cite{wadler-findler09}: upcasts
 never raise positive blame, so only need to be parameterized by a
 negative label and downcasts never raise negative blame so only need
 to be parameterized by a positive label.
-
+%
 We argue that the observation that upcasts are thunkable and downcasts
 are linear is directly related to blame in that if an upcast were
 \emph{not} thunkable, it should raise positive blame and if a downcast
 were \emph{not} linear, it should raise negative blame.
 %
-First, if an upcast of value types were \emph{not} a priori thunkable,
-it would be of the form $\upcast{\u F A}{\u F A'}$, and if it truly
-were not thunkable, then in our logical relation this would mean there
-was a value $V : A$ such that $\upcast{\u F A}{\u F A'}\ret V$
-performs some effect.
+First, consider a potentially effectful stack upcast of the form
+$\upcast{\u F A}{\u F A'}$. If it is not thunkable, then in our logical
+relation this would mean there is a value $V : A$ such that $\upcast{\u
+  F A}{\u F A'}(\ret V)$ performs some effect.
 %
-Since casts must be minimal in the refinement ordering, the only
-observable effects for casts should be dynamic type errors, this means
-that $\upcast{\u F A}{\u F A'}\ret V \mapsto \err$, and we must decide
+Since the only observable effects for casts are dynamic type errors, 
+$\upcast{\u F A}{\u F A'}(\ret V) \mapsto \err$, and we must decide
 whether the positive party or negative party is at fault.
-% AA: above sentence is hard to follow.  Too long and a bit jargon-y.
 %
 However, since this is call-by-value evaluation, this error happens
 unconditionally on the continuation, so the continuation never had a
-chance to behave in such a way as to prevent blame, so we must blame the
+chance to behave in such a way as to prevent blame, and so we must blame the
 positive party.
-
-Dually, if a downcast of computation types were not a priori linear,
-it would be of the form $\dncast{U \u B}{U \u B'}$ and if it were
-truly not linear, that would mean it forces its $U \u B'$ input either
-never or more than once.
+%
+Dually, consider a value downcast of the form $\dncast{U \u B}{U \u B'}$.
+If it is not linear, that would mean it forces its $U \u B'$
+input either never or more than once.
 %
 Since downcasts should refine their inputs, it is not possible for
-the downcast to use the argument twice, since printing twice does not
+the downcast to use the argument twice, since e.g. printing twice does not
 refine printing once.
 %
 So if the cast is not linear, that means it fails without ever forcing
@@ -9027,6 +9023,7 @@ so must blame the negative party.
 %% The association we propose of upcasts to (positive) value types and
 %% downcasts to (negative) computation types
 
+\begin{longonly}
 \paragraph{Denotational and Category-theoretic Models}
 
 We have presented certain concrete models of GTT using ordered CBPV
@@ -9035,53 +9032,54 @@ interpretation.
 %
 It may be of interest to develop a more general notion of model of GTT
 for which we can prove soundness and completeness theorems, as in
-\cite{cbn-gtt}.
+\cite{newlicata2018-fscd}.
 %
 A model would be a strong adjunction between double categories where
 one of the double categories has all ``companions'' and the other has
-all ``conjoints'' corresponding to our upcasts and downcasts.
+all ``conjoints'', corresponding to our upcasts and downcasts.
 %
 Then the contract translation should be a construction that takes a
-strong adjunction and makes a strong adjunction between double
-categories where the ep pairs are ``Kleisli'' ep pairs: the upcast is
-has a right adjoint, but only in the Kleisli category and vice-versa
-the downcast has a left adjoint in the Co-Kleisli category.
+strong adjunction between 2-categories and makes a strong adjunction
+between double categories where the ep pairs are ``Kleisli'' ep pairs:
+the upcast is has a right adjoint, but only in the Kleisli category and
+vice-versa the downcast has a left adjoint in the co-Kleisli category.
 
 Furthermore, the ordered CBPV with errors should also have a sound and
 complete notion of model, and so our contract translation should have
 a semantic analogue as well.
+\end{longonly}
+
+\begin{longonly}
+  \paragraph{Gradual Session Types} ~
+\end{longonly}
 
-\paragraph{Modal Gradual Typing}
+Gradual session types~\cite{igarashi+17gradualsession} share some
+similarities to GTT, in that there are two sorts of types (values and
+sessions) with a dynamic value type and a dynamic session type.
+However, their language is not \emph{polarized} in the same way as CBPV,
+so there is not likely an analogue between our upcasts always being
+between value types and downcasts always being between computation
+types.  Instead, we could reconstruct this in a \emph{polarized} session
+type language like ~\cite{pfenninggriffith15session}.
+\begin{longonly}
+The two dynamic types would then be the ``universal sender'' and
+``universal receiver'' session types.
+\end{longonly}
 
-The most similar gradually typed language to our full GTT is the
-language of gradual session types given in (TODO: cite Gradual Session
-Types).
-%
-It has several similarities: there are two sorts of types (values and
-sessions) and correspondingly two dynamic types: a dynamic value type
-and dynamic session type.
-%
-However, their formulation is quite different in that sessions are
-considered to be a \emph{subset} of value types whereas in ours there
-are explicit coercions between value and computation types.
-%
-Furthermore, their language is not \emph{polarized} in the same way as
-CBPV, so there is not likely an analogue between our upcasts being
-always between value types and downcasts being always between
-computation types in their system.
-%
-Instead, we could reconstruct this in a \emph{polarized} session type
-language where there are two types of sessions: sending and receiving
-and there would be ``universal sender'' and ``universal receiver''
-session types.
+%% if this is making one of F, U silent that doesn't seem that different to me
+%% 
+%% However, their formulation is quite different in that sessions are
+%% considered to be a \emph{subset} of value types whereas in ours there
+%% are explicit coercions between value and computation types.
 
+\begin{longonly}
 \paragraph{Dynamically Typed Call-by-push-value}
 
 Our interpretation of the dynamic types in CBPV suggests a design for
 a Scheme-like language with a value and computation distinction.
 %
 This may be of interest for designing an extension of Typed Racket that
-efficiently supports CBN or a scheme-like language with codata types.
+efficiently supports CBN or a Scheme-like language with codata types.
 %
 While the definition of the dynamic computation type by a lazy product
 may look strange, we argue that it is no stranger than the use of its
@@ -9104,6 +9102,28 @@ This says that a dynamically typed computation is one that can be
 invoked with any finite number of arguments on the stack, a fairly
 accurate model of implementations of Scheme that pass multiple
 arguments on the stack.
+\end{longonly}
+
+\smallskip
+
+In this paper, we have given an axiomatic logic for reasoning about
+gradual programs in a mixed call-by-value/call-by-name language, shown
+that the axioms imply almost all of a contract translation implementing
+the runtime casts of gradual typing, and shown that the axiomatics is
+sound for contextual equivalence/approximation in an operational model.
+We believe it is straightforward to add inductive value types and
+coinductive computation types, and obtain similar unique cast
+implementation theorems
+(e.g. $\upcast{\mathtt{list}(A)}{\mathtt{list}(A')} \equidyn
+\mathtt{map}(\upcast{A}{A'})$).  In future work, we plan to investigate
+extensions of GTT with unrestricted recursive types, polymorphism, and
+state, where both equational reasoning and gradualization are more
+difficult~\cite{...}.  We also plan to investigate models of GTT based
+on efficient contract implementation strategies such as~\cite{siekwadler10zigzag},
+to see if these satisfy the design criteria of $\beta,\eta$ and
+graduality.  
+
+\newpage
 
 \bibliography{max}
 
diff --git a/paper/max.bib b/paper/max.bib
index 6b861d9..00ef0b3 100644
--- a/paper/max.bib
+++ b/paper/max.bib
@@ -1060,3 +1060,33 @@ pages="396--410",
   volume =    {volume 9600},
 }
 
+@article{igarashi+17gradualsession,
+ author = {Igarashi, Atsushi and Thiemann, Peter and Vasconcelos, Vasco T. and Wadler, Philip},
+ title = {Gradual Session Types},
+ journal = {Proceedings of ACM Programning Languages},
+ issue_date = {September 2017},
+ volume = {1},
+ number = {ICFP},
+ month = aug,
+ year = {2017},
+ pages = {38:1--38:28},
+ articleno = {38},
+ numpages = {28},
+} 
+
+@InProceedings{pfenninggriffith15session,
+  author =       {Frank Pfenning and Dennis Griffith},
+  title =        {Polarized Substructural Session Types (invited talk)},
+  booktitle = {International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)},
+  year =      {2015}
+}
+
+@inproceedings{siekwadler10zigzag,
+ author = {Siek, Jeremy G. and Wadler, Philip},
+ title = {Threesomes, with and Without Blame},
+ booktitle = popl,
+ year = {2010},
+ location = {Madrid, Spain},
+ pages = {365--376},
+ publisher = {ACM}
+} 
\ No newline at end of file
-- 
GitLab