start GTT

notes/strength.tex

+The principle at work here is that while call-by-push-value gives us a
+syntax for an adjunction (between value and computation categories)
+with a syntax for the profunctor the adjunction represents (the term
+morphisms), we can also consider the \emph{Kleisli} categories of the
+adjunction, which are equivalent to the images of the $\u F$ and $U$
+types.
+%
+These are precisely the categories corresponding to call-by-value and
+call-by-name languages respectively.
+%
+Then we can ask in what sense the connectives extend from functors on
+the value and computation categories to ``functors'' on the
+corresponding Kleisli and co-Kleisli categories.
+%
+We put ``functor'' in quotes because in fact, these will not quite
+satisfy the ordinary sense of functoriality in multiple arguments.
+%
+Instead, the functors will be \emph{separately functorial} in each
+argument, whereas ordinarily functor in several argument means
+\emph{jointly functorial}.
+%
+So for example let $\cat C, \cat D , \cat E$ be categories, then we
+would say that a separately functorial function $F : \cat C, \cat D
+\to \cat E$ would consist of first an action on objects $F_0 : \cat
+C_0, \cat D_0 \to \Cat E_0$ and then two actions: taking any object $d
+\in D_0$ to a functor $F(-,id_d) : \cat C \to \cat E$ and similarly
+one taking any object $c \in C_0$ to a functor $F(id_c,=): \cat D \to
+\cat E$.
+%
+Then we have two candidates for a true joint functorial action that
+are in general not equal: $F(f,id)\circ F(id,g)$ and vice-versa
+$F(id,g) \circ F(f,id)$.
+%
+The fact that these are \emph{not} models the fact that evaluation
+order matters.
+
+\begin{theorem}[Effectful Functors]
+  Given a call-by-push-value adjunction model $V,C,R,F,U$ and given
+  any jointly functorial functor $G : D_1,\ldots,D_n \to E$ where all
+  of $D_1,\ldots,D_n,E$ are either $V,C,V^o,C^o$, that is
+  \emph{strong} in that for each argument category $D_i$, there are
+  morphisms of one of the following forms (whichever is well-sorted
+  for $G$ and $D_i$)
+
+  \[ G(D_1,\ldots,F(D_i),\ldots,D_n) \to F(G(D_1,\ldots,D_n)) \]
+  \[ G(D_1,\ldots,U(D_i),\ldots,D_n) \to F(G(D_1,\ldots,D_n)) \]
+  \[ G(D_1,\ldots,F(D_i),\ldots,D_n) \to U(G(D_1,\ldots,D_n)) \]
+  \[ G(D_1,\ldots,U(D_i),\ldots,D_n) \to U(G(D_1,\ldots,D_n)) \]
+  
+  then there is an
+  associated separately functorial functor $\hat G : \hat
+  D_1,\ldots,\hat D_n \to \hat E$ where
+
+  
+  \begin{align*}
+    \hat V = F(V)\\
+    \hat C = U(C)\\
+    \hat D^o = (\hat D)^o
+  \end{align*}
+\end{theorem}
+\begin{proof}
+  
+\end{proof}

paper/gtt.tex

+%% For double-blind review submission
+\documentclass[acmsmall,anonymous,review]{acmart}\settopmatter{printfolios=true}
+%% For single-blind review submission
+%\documentclass[acmlarge,review]{acmart}\settopmatter{printfolios=true}
+%% For final camera-ready submission
+%\documentclass[acmlarge]{acmart}\settopmatter{}
+
+%% Note: Authors migrating a paper from PACMPL format to traditional
+%% SIGPLAN proceedings format should change 'acmlarge' to
+%% 'sigplan,10pt'.
+
+%% Some recommended packages.
+% \usepackage{booktabs}   %% For formal tables:
+%                         %% http://ctan.org/pkg/booktabs
+% \usepackage{subcaption} %% For complex figures with subfigures/subcaptions
+%                         %% http://ctan.org/pkg/subcaption
+
+\makeatletter\if@ACM@journal\makeatother
+%% Journal information (used by PACMPL format)
+%% Supplied to authors by publisher for camera-ready submission
+\acmJournal{PACMPL}
+\acmVolume{1}
+\acmNumber{1}
+\acmArticle{1}
+\acmYear{2017}
+\acmMonth{1}
+\acmDOI{10.1145/nnnnnnn.nnnnnnn}
+\startPage{1}
+\else\makeatother
+%% Conference information (used by SIGPLAN proceedings format)
+%% Supplied to authors by publisher for camera-ready submission
+\acmConference[PL'17]{ACM SIGPLAN Conference on Programming Languages}{January 01--03, 2017}{New York, NY, USA}
+\acmYear{2017}
+\acmISBN{978-x-xxxx-xxxx-x/YY/MM}
+\acmDOI{10.1145/nnnnnnn.nnnnnnn}
+\startPage{1}
+\fi
+%% Copyright information
+%% Supplied to authors (based on authors' rights management selection;
+%% see authors.acm.org) by publisher for camera-ready submission
+\setcopyright{none}             %% For review submission
+%\setcopyright{acmcopyright}
+%\setcopyright{acmlicensed}
+%\setcopyright{rightsretained}
+%\copyrightyear{2017}           %% If different from \acmYear
+
+
+%% Bibliography style
+\bibliographystyle{ACM-Reference-Format}
+%% Citation style
+%% Note: author/year citations are required for papers published as an
+%% issue of PACMPL.
+% \citestyle{acmauthoryear}   %% For author/year citations
+% 
+
+\title{Gradual Type Theory}
+
+%% Author information
+%% Contents and number of authors suppressed with 'anonymous'.
+%% Each author should be introduced by \author, followed by
+%% \authornote (optional), \orcid (optional), \affiliation, and
+%% \email.
+%% An author may have multiple affiliations and/or emails; repeat the
+%% appropriate command.
+%% Many elements are not rendered, but should be provided for metadata
+%% extraction tools.
+%% Author with single affiliation.
+\author{Max S. New}
+\affiliation{
+ %% \department{CCIS}              %% \department is recommended
+  \institution{Northeastern University}            %% \institution is required
+%  \streetaddress{Street1 Address1}
+%  \city{City1}
+%  \state{State1}
+%  \postcode{Post-Code1}
+%  \country{Country1}
+}
+\email{maxnew@ccs.neu.edu}          %% \email is recommended
+
+\author{Daniel R. Licata}
+\affiliation{
+%  \department{Department1}              %% \department is recommended
+  \institution{Wesleyan University}            %% \institution is required
+%  \streetaddress{Street1 Address1}
+%  \city{City1}
+%  \state{State1}
+%  \postcode{Post-Code1}
+%  \country{Country1}
+}
+\email{dlicata@wesleyan.edu}          %% \email is recommended
+
+\author{Amal Ahmed}
+\affiliation{
+%  \department{Department1}              %% \department is recommended
+  \institution{Northeastern University}            %% \institution is required
+  \institution{Inria Paris}            %% \institution is required
+%  \streetaddress{Street1 Address1}
+%  \city{City1}
+%  \state{State1}
+%  \postcode{Post-Code1}
+%  \country{Country1}
+}
+\email{amal@ccs.neu.edu}          %% \email is recommended
+
+\begin{document}
+
+\begin{abstract}
+  We present Gradual Type Theory: an axiomatic semantics of gradual
+  typing.
+  Gradual Type Theory gives specifications to the cast semantics that
+  are normally part of the language definition of gradual typing.
+  Since it is based on Levy's Call-by-push-value language, it supports
+  embeddings of call-by-value and call-by-name gradually typed
+  languages, and proves uniqueness theorems for cast/contracts in
+  call-by-value and call-by-name languages with both positive and
+  negative type connectives.
+\end{abstract}
+
+%% 2012 ACM Computing Classification System (CSS) concepts
+%% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
+\begin{CCSXML}
+<ccs2012>
+<concept>
+<concept_id>10011007.10011006.10011008</concept_id>
+<concept_desc>Software and its engineering~General programming languages</concept_desc>
+<concept_significance>500</concept_significance>
+</concept>
+<concept>
+<concept_id>10003456.10003457.10003521.10003525</concept_id>
+<concept_desc>Social and professional topics~History of programming languages</concept_desc>
+<concept_significance>300</concept_significance>
+</concept>
+</ccs2012>
+\end{CCSXML}
+
+\ccsdesc[500]{Software and its engineering~General programming languages}
+\ccsdesc[300]{Social and professional topics~History of programming languages}
+%% End of generated code
+
+
+%% Keywords
+%% comma separated list
+% \keywords{keyword1, keyword2, keyword3}  %% \keywords is optional
+
+
+%% \maketitle
+%% Note: \maketitle command must come after title commands, author
+%% commands, abstract environment, Computing Classification System
+%% environment and commands, and keywords command.
+\maketitle
+
+\section{Introduction}
+
+...
+
+Previous work has built towards this goal from two directions.
+%
+First, \cite{cbn-gtt} provided an axiomatic semantics for the
+negative fragment of call-by-name in which upcasts and downcasts were
+specified as certain joins and meets respectively.
+%
+There, they proved two ``contract uniqueness principles'' for
+call-by-name gradual typing: if the language satisfies a property
+called graduality\footnote{an extensional version of \cite{refined}'s
+  dynamic gradual guarantee} and the $\eta$ laws for functions and
+products, then the casts between function types (respectively product
+types) must be equivalent to the classic ``wrapping'' implementation.
+
+Second, \cite{cbv-gt-lr} provided a logical relation interpretation of
+graduality in terms of a nonstandard ``observational error
+approximation'' relation.
+%
+They synthesized the casts from the syntax of type dynamism proofs and
+decomposed the graduality property into observational error
+approximation ``up to cast''.
+
+Each paper had certain limitations: \cite{cbn-gtt} only dealt with the
+negative fragment of call-by-name, and did not have an accompanying
+operational semantic interpreation.
+%
+On the other hand, \cite{cbv-gt-lr} dealt with positive and negative
+types in call-by-value, but only allowed for contextual equivalence
+proofs in a \emph{single} language, because it was not based on an
+axiomatic semantics.
+%
+In this paper, we resolve all of these problems by developing a new
+axiomatic system we dub \emph{Gradual Type Theory} (GTT), and a
+logical relation model for it using observational error approximation
+in a variant of Levy's \emph{Call-by-push-value}.
+%
+Gradual Type Theory is built by applying the type theoretic
+methodology used to design Call-by-name GTT to Call-by-push-value.
+%
+We chose call-by-push-value because it follows a similar type
+theoretic discipline as the negative type lambda calculus: all
+connectives internalize some property of the judgmental structure of
+the system.
+
+
+\end{document}
+
+%% Local Variables:
+%% compile-command: "latexmk -C gtt.tex; pdflatex gtt.tex"
+%% End: