From c8782a81ff1b6b2a245db5662a94567fa930191f Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 26 Jun 2018 12:28:06 -0400
Subject: [PATCH] shorter abstract
---
paper/gtt.tex | 114 +++++++++++++++++---------------------------------
1 file changed, 39 insertions(+), 75 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 1b8c8bb..2bf0408 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -5,6 +5,12 @@
%% For final camera-ready submission
%\documentclass[acmlarge]{acmart}\settopmatter{}
+\newif\ifshort
+\newif\iflong
+%% Pick long or short version:
+%% \shorttrue
+\longtrue
+
%% Note: Authors migrating a paper from PACMPL format to traditional
%% SIGPLAN proceedings format should change 'acmlarge' to
%% 'sigplan,10pt'.
@@ -238,90 +244,48 @@
\begin{abstract}
Gradually typed languages are designed to support both dynamically
- typed and statically typed programming styles and preserve the
- benefits of each: dynamic code can be used without conforming to the
- syntactic type discipline, and static code provides sound reasoning
- principles that formally justify type-based refactorings and
- optimizations.
- %
- The linchpin to the design is the semantics of runtime casts that
- ensure that the typed reasoning principles are valid by checking
- types of dynamically typed code at runtime.
- %
- However, very few previous works have actually proven that the
- runtime casts ensure correctness of type based optimizations.
+ typed and statically typed programming styles without sacrificing
+ the soundness of type-based refactorings and optimizations.
%
- In fact, we show that one of the most commonly proposed semantics of
- runtime casts, the ``eager'' semantics \emph{invalidates} certain
- type based optimization for function types that are valid in
- statically typed languages.
+ However, establishing the correctness of program transformations is
+ technically difficult and often neglected in the metatheory of these
+ languages.
%
- This shows that eager semantics is ``over-eager'' to find bugs:
- while it catches syntactic type errors earlier than the lazy
- semantics, it disables the type-based optimizations and refactorings
- that gradual typing is intended to enable.
+ In this paper we propose an \emph{axiomatic} account of program
+ equivalence in a gradual cast calculus, which we formalize in a
+ logic we call \emph{gradual type theory} (GTT).
%
- On the other hand, we show the simpler ``lazy'' semantics of runtime
- casts does validate the optimization.
- %
- This presents the question: are there other semantics that also
- validate these optimizations?
+ Based on Levy's call-by-push-value, GTT gives an axiomatic account
+ of both call-by-value and call-by-name gradual languages.
- To study this question, we define Gradual Type Theory (GTT): an
- axiomatic semantics of gradual typing.
- %
- To axiomatize type based reasoning, GTT includes the $\beta, \eta$
- equalities that are valid for effectful programs.
+ Based on our axiomatic account we prove many theorems that justify
+ optimizations and refactorings in gradually typed languages.
%
- To constrain the design, we also axiomatize the \emph{graduality} of
- the system, an extensional variant of Siek-Vitousek-Cimini-Boyland's
- gradual guarantee.
- %
- We base the type theory on Levy's Call-by-push-value to correctly
- accomodate the $\eta$ principles in the presence of effects, and as
- a consequence we model both call-by-value and call-by-name gradual
- typing in the same system.
-
- We use gradual type theory to show that the combination of the
- graduality property and the $\beta, \eta$ principles \emph{uniquely
- determines} the behavior of almost all casts of gradual typing.
- %
- This shows that any gradual language that supports both must be
- equivalent to the ``wrapping'' semantics, and any system that
- differs from it must violate graduality or extensionality (typically
- the latter), extending a previous result for a fragment of
- call-by-name to full call-by-name and call-by-value.
+ For example, we show what we call \emph{uniqueness principles} for
+ gradual type connectives that show that if the $\beta\eta$ laws hold
+ for a connective, then casts between that connective must be
+ equivalent to the ``lazy'' cast semantics.
%
- On the other hand the structure of the dynamic type itself, which is
- taken for granted to be a sum in previous work, is not uniquely
- determined by the axiomatics, and we present several designs for
- dynamic types that to varying degrees support interoperability
- between call-by-value and call-by-name programs.
-
- Furthermore, taking advantage of call-by-push-value's fine-grained
- reasoning about effects, we prove the validity of another class of
- optimizations under very mild conditions on the dynamic type.
+ As a contrapositive, this shows that ``eager'' cast semantics
+ violates the extensionality of function types.
%
- Specifically, we show that all upcasts are pure (thunkable) and that
- all downcasts are strict (linear).
+ Additionally, we show that gradual upcasts are pure functions and
+ dually gradual downcasts are strict functions, an equational
+ analogue of Wadler-Findler's blame soundness theorem.
+
+ We show the consistency and applicability of our axiomatic
+ theory by proving that a contract-based implementation using the
+ lazy cast semantics gives a model of our type theory where
+ equivalence in GTT implies contextual equivalence of the programs.
%
- These two properties are extremely useful for optimizations because
- pure terms in call-by-value can be freely moved and strict terms in
- call-by-name can justify elimination of unnecessary thunks.
+ Since GTT also axiomatizes the dynamic gradual guarantee, our
+ logical relation also establishes this central theorem of gradual
+ typing.
%
- We argue that these properties are the intended meaning of the blame
- soundness theorem.
-
- Finally, to show the consistency of our type theory, and its
- relation to operational semantics, we give a \emph{contract
- translation} of our gradual language into typed
- call-by-push-value, and prove that it preserves graduality and
- $\beta, \eta$ by developing a logical relation for
- call-by-push-value's operational semantics.
- %
- Using the rich types of call-by-push-value, we vary the structure of
- the dynamic type and produce several translations that all model the
- axioms of GTT.
+ Finally, we define \emph{multiple} contract-based implementations by
+ varying the structure of the dynamic types, giving a family of
+ implementations that validate type-based optimization and the
+ gradual guarantee.
\end{abstract}
%% 2012 ACM Computing Classification System (CSS) concepts
--
GitLab