From 871666ac59c034345203afa66592a80e3093c33d Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 29 Oct 2018 15:17:11 -0400
Subject: [PATCH] revise the lazy section

---
 paper/gtt.tex | 106 +++++++++++++++++++++++++-------------------------
 paper/max.bib |  21 ++++++++++
 2 files changed, 75 insertions(+), 52 deletions(-)

diff --git a/paper/gtt.tex b/paper/gtt.tex
index 608974c..6f7ac05 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -218,6 +218,7 @@
 \newcommand{\inr}{\kw{inr}}
 \newcommand{\intag}[1]{\texttt{in}_{#1}}
 \newcommand{\els}{\kw {else}}
+\newcommand{\texttt{seq}}
 
 \newcommand{\dyn}{{?}}
 \newcommand{\dynv}{{?}}
@@ -9407,9 +9408,9 @@ It is a well-known issue that the lazy semantics of function casts is
 not compatible with the refinement property that graduality models in
 the presence of pointer equality, and our uniqueness theorem provides
 a different perspective on this phenomenon
-\cite{findlerflattfelleisen04, refined}.
+\cite{findlerflattfelleisen04,chaperonesimpersonators, refined}.
 %
-However, we note that the cases of the uniqueness theorem, for each
+However, we note that the cases of the uniqueness theorem for each
 type connective are completely \emph{modular}: they rely only on the
 specification of casts and the $\beta,\eta$ principles for the
 particular connective, and not on the presence of any other types,
@@ -9419,50 +9420,57 @@ So while a call-by-value language that has reference equality of
 functions might still have the $\eta$ principle for strict pairs, so
 that case of the theorem still applies.
 
-% TODO: the following is all subsumed by using Levy's account of
-% "the lazy paradigm"
-While call-by-value evaluation is a fairly consistent notion,
-non-eager evaluation comes in many flavors.
+Next, we consider the applicability to non-eager languages.
 %
-Not only is there the distinction between call-by-name and
-call-by-need, but in practice lazy languages like Haskell contain
-operators like \texttt{seq} in Haskell that force strict evaluation
-and invalidate the call-by-name $\eta$ principle.
+Analogous to call-by-value, our uniqueness principle should apply to
+simple \emph{call-by-name} gradual languages, where full $\eta$
+equality for functions is satisfied, but $\eta$ equality for booleans
+and strict pairs requires a ``stack restriction'' dual to the value
+restriction for call-by-value function $\eta$.
 %
-Call-by-push-value has been shown to embed call-by-name evaluation
-\emph{without} the presence of the \texttt{seq} operator or any
-analogous operation where the function type is modeled as $UB \to B'$.
+We are not aware of any call-by-name gradual languages, but there is
+considerable work on \emph{contracts} for non-eager languages,
+especially Haskell, \cite{hinzeJeuringLoh06,XuPJC09}.
 %
-To apply our framework to call-by-name languages that support
-\texttt{seq}, we would need to first provide an embedding into
-call-by-push-value that supports this operation.
+However, we note that Haskell is \emph{not} a call-by-name language in
+our sense for two reasons.
 %
-This seems feasible, for instance a function $\texttt{Number} \to
-\texttt{String}$ would be interpreted as $UFU(UF\texttt{Number}\to
-\texttt{String})$, where the extra $UF$ models the fact that we can
-force the function to a value without necessarily calling it by using
-\texttt{seq}.
+First, Haskell uses call-by-need evaluation where results of
+computations are memoized. However when only considering Haskell's
+effects (error and divergence), this difference is not observable so
+this is not the main obstacle.
 %
-In this sense, Haskell's behavior is similar to call-by-value in that
-it satisfies a modified $\eta$ principle for functions: $x =
-\texttt{seq} x (\lambda y. x y)$ where $x$ is a variable.
+The bigger difference between Haskell and call-by-name is that Haskell
+supports a \texttt{seq} operation that enables the programmer to force
+evaluation of a term to a value.
 %
-If this embedding is correct, then just as with call-by-value, GTT
-provides a semantics of casts that satisfies graduality and validates
-this $\eta$ principle.
+This means Haskell violates the function $\eta$ principle because
+$\Omega$ will cause divergence under $\seq$, whereas $\lambda
+x. \Omega$ will not.
 %
-In future work, we plan to do a more thorough analysis of the
-resulting semantics and compare to previous proposals for lazy
-contract semantics (TODO cite).
+This is a crucial feature of Haskell and is a major source of
+differences between implementations of lazy contracts, as noted in
+\cite{Degen2012TheIO}.
 %
-Finally note that once we have introduced the extra thunks to model
-\texttt{seq}, if the only effects used are idempotent then the
-difference between call-by-name and call-by-need is only relevant for
-performance reasons.
+We can understand this difference by using a different translation
+into call-by-push-value: what Levy calls the ``lazy paradigm'', as
+opposed to call-by-name \cite{levy03cbpvbook}.
 %
-Since divergence and uncatchable errors are idempotent, and these are
-usually the only effects in lazy languages, the resulting cast
-semantics GTT produces should also be valid for call-by-need.
+Simply put, connectives are interpreted as in call-by-value, but with
+the addition of extra thunks $UF$, so for instance the lazy function
+type $A \to B$ is interpreted as $UFU(UFA \to FB)$ and the extra $UFU$
+here is what causes the failure of the call-by-name $\eta$ principle.
+%
+With this embedding and the uniqueness theorem, GTT produces a
+definition for lazy casts, and the definition matches the work of
+\citet{XuPJC09} when restricting to non-dependent contracts.
+
+Some recent work \cite{greenmanfelleisen:2018} gives a spectrum of
+differing syntactic type soundness theorems for different semantics of
+gradual typing.
+%
+Our work here is complementary, showing that certain program
+equivalences can only be achieved by certain cast semantics.
 
 \citet{Degen2012TheIO} give an analysis of different cast semantics
 for contracts in lazy languages, specifically based on Haskell, so
@@ -9489,29 +9497,23 @@ The two properties are incompatible because for instance a pair of a
 diverging term and a value can't be deeply checked without causing the
 entire program to diverge.
 %
-Assuming we can extend the translation of call-by-name with
-\texttt{seq} to call-by-push-value, then their incompatibility theorem
-should be a consequence of our main theorem in the following sense.
+Using Levy's embedding of the lazy paradigm into call-by-push-value
+their incompatibility theorem should be a consequence of our main
+theorem in the following sense.
 %
-Our main theorem shows that any semantics departing from the lazy
-semantics must violate $\eta$ or graduality.
+We showed that any contract semantics departing from the
+implementation in theorem \ref{thm:functorial-casts} must violate
+$\eta$ or graduality.
 %
-Their completeness property is inherently eager, and so is different
-from the semantics GTT would provide, so either $\eta$ or graduality
-fails.
+Their completeness property is inherently eager, and so must be
+different from the semantics GTT would provide, so either the
+restricted $\eta$ or graduality fails.
 %
 However, since they are defining contracts within the language, they
 satisfy the restricted $\eta$ principle provided by the language, and
 so it must be graduality, and therefore meaning preservation that
 fails.
 
-Some recent work \cite{greenmanfelleisen:2018} gives a spectrum of
-differing syntactic type soundness theorems for different semantics of
-gradual typing.
-%
-Our work here is complementary, showing that certain program
-equivalences can only be achieved by certain cast semantics.
-
 Henglein's work on dynamic typing also uses an axiomatic semantics of
 casts, but axiomatizes behavior of casts at each type directly whereas
 we give a uniform definition of all casts and derive implementations
diff --git a/paper/max.bib b/paper/max.bib
index 0ff7d1f..84d08a4 100644
--- a/paper/max.bib
+++ b/paper/max.bib
@@ -1207,3 +1207,24 @@ booktitle= ecoop,
 year={2004}
 }
 
+@inproceedings{chaperonesimpersonators,
+ author = {Strickland, T. Stephen and Tobin-Hochstadt, Sam and Findler, Robert Bruce and Flatt, Matthew},
+ title = {Chaperones and Impersonators: Run-time Support for Reasonable Interposition},
+ series = oopsla,
+ year = {2012},
+}
+
+@inproceedings{XuPJC09,
+ author = {Xu, Dana N. and Peyton Jones, Simon and Claessen, Koen},
+ title = {Static Contract Checking for Haskell},
+ series = popl09,
+ year = {2009},
+}
+
+@InProceedings{hinzeJeuringLoh06,
+author="Hinze, Ralf and Jeuring, Johan and L{\"o}h, Andres",
+title="Typed Contracts for Functional Programming",
+booktitle=flops,
+year="2006",
+
+}
\ No newline at end of file
-- 
GitLab