show wf blame soundness => thunkable/linear

paper/gtt.tex

@@ -307,6 +307,9 @@ This has the benefit that equivalence and approximation properties can
 be stated and proven entirely syntactically, and allows for multiple
 different concrete interpertations using logical relations, domains,
 etc.
+%
+This way we can add gradual typing as a sort of ``axiomatic mixin''
+that can be added modularly to the axioms of an existing logic.
 
 To study gradual typing axiomatically, we first need to understand the
 relational principles that gradual typing should satisfy.
@@ -489,11 +492,11 @@ This shows us that a stack out of a function type \emph{calls the
 %
 Generalizing further, a stack out of an iterated function type $A_1
 \to A_2 \to \u B$ \emph{supplies all of the arguments}
-%
-
 
 \subsection{Casts}
 
+
+
 It is not immediately obvious how to add type casts to
 call-by-push-value, but we can use previous work on call-by-value and
 call-by-name gradual typing, combined with the embeddings of CBV and
@@ -685,25 +688,67 @@ omega paper?)
 It should be the case that the terms in AGT are the subset of ours
 that are definable using the upcasts and downcasts in that language.
 
-\paragraph{Blame and the Tangram Theorem}
+\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, and in our contract implementation we can parameterize the
-upcasts and downcasts by a blame label and raise an error with the
-blame information rather than the uninformative $\err$.
-%
-Also, our judicious division of casts into upcasts and downcasts
-naturally pairs with the blame soundness properties given in
-\cite{wadler-findler}: 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.
-
-TODO: can we relate this and the tangram theorem more directly to what
-we're doing?
-%
-The association we propose of upcasts to (positive) value types and
-downcasts to (negative) computation types
+add it.
+%
+The division of casts into upcasts and downcasts naturally pairs with
+the blame soundness properties given in \cite{wadler-findler}: 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.
+%
+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
+whether the positive party or negative party is at fault.
+%
+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 to prevent blame, 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.
+%
+Since downcasts should be refine their inputs, it is not possible for
+the downcast to use the argument twice, since printing twice does not
+refine printing once.
+%
+So if the cast is not linear, that means it fails without ever forcing
+its input, in which case it knows nothing about the positive party and
+so must blame the negative party.
+
+%% This argument shows intuitively that if upcasts never raise positive
+%% blame, they must be thunkable (and similarly for downcasts and
+%% linearity).
+%% %
+%% To explain the converse, we note again the harmony between shifts and
+%% variance in the system: besids $\u F, U$ every type constructor has
+%% covariant arguments of the same sort and contravariant arguments of
+%% the dual sort.
+%% %
+%% Furthermore, every value connective besides $U$ is a \emph{positive}
+%% type, meaning its elimination rule is invertible, i.e. that any
+%% well-typed continuation 
+
+%% The association we propose of upcasts to (positive) value types and
+%% downcasts to (negative) computation types
 
 \paragraph{$\eta$ Law in Practice}
 
@@ -751,7 +796,7 @@ covariant arguments of the opposite sort as the connective.
 %
 Because of this, they would need to be treated carefully, in a similar
 way as the $U, \u F$ connectives.
-%
+v%
 In addition, the connectives are not operationally well-behaved.
 %
 For instance adding a value function space would mean also including a