From 33b0529b6c579ec63c8850e9b84d82d42104610b Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Fri, 19 Jan 2024 09:09:43 -0500
Subject: [PATCH] some intro work and add macros for comments
---
paper-new/intro.tex | 40 +++++++++++++++++++++++++++-------------
paper-new/paper.tex | 7 ++++++-
2 files changed, 33 insertions(+), 14 deletions(-)
diff --git a/paper-new/intro.tex b/paper-new/intro.tex
index f04fba3..4c4a3a2 100644
--- a/paper-new/intro.tex
+++ b/paper-new/intro.tex
@@ -11,10 +11,9 @@ program is free of type errors, and moreover, soundness of the equational theory
that program optimizations are valid.
Meanwhile, dynamic typing allows the programmer to rapidly prototype
their application code without needing to commit to fixed type signatures for their
-functions. Unfortunately, most languages choose between static or dynamic typing.
-As a result, programmers that initially write their code in a dynamically typed language
-in order to benefit from faster prototyping and development time will need to rewrite the
-entire codebase in a static language if they would like to receive the benefits of static
+functions. Most languages choose between static or dynamic typing and as a result, programmers that initially write their code in a dynamically typed language
+in order to benefit from faster prototyping and development time need to rewrite the
+some or all of their codebase in a static language if they would like to receive the benefits of static
typing once their codebase has matured.
\emph{Gradually-typed languages} \cite{siek-taha06, tobin-hochstadt06} seek to resolve this tension
@@ -36,7 +35,6 @@ dynamic to static, and allow for those different parts to interact with one anot
Moreover, gradually-typed languages should support the smooth migration from
dynamic typing to static typing, in that the programmer can initially leave off the
typing annotations and provide them later without altering the meaning of the program.
-
% Sound gradual typing
Furthermore, the parts of the program that are written in a dynamic style should soundly
interoperate with the parts that are written in a static style.
@@ -53,16 +51,32 @@ violated the typing contract imposed by statically typed code.
% this interaction should respect the guarantees made by the static types.
% Graduality property
-Formally speaking, gradually typed languages should satisfy the
+One of the fundamental theorems for gradually typed languages is
\emph{dynamic gradual guarantee}, originally defined by Siek, Vitousek, Cimini,
-and Boyland \cite{siek_et_al:LIPIcs:2015:5031}.
-This property is also referred to as \emph{graduality} \cite{new-ahmed2018},
+and Boyland \cite{siek_et_al:LIPIcs:2015:5031}, also called \emph{graduality} \cite{new-ahmed2018},
by analogy with parametricity.
-Intuitively, graduality says that going from a dynamic to static style should not
-introduce changes in the meaning of the program.
-More specifically, making the types more precise by adding typing annotations
-will either result in the same behavior as the original, less precise program,
-or will result in a type error.
+Informally, graduality says that going from a dynamic to static style should only allow for the introduction of static or dynamic type errors, and not otherwise change the meaning of the program.
+%
+This is a way to capture programmer intuition that increasing type
+precision corresponds to a generalized form assertions at runtime
+only, and so they can trust that prior observed behavior of their
+dynamically typed code will remain unchanged as long as it satisfies
+the new stricter typing discipline.
+
+Additionally, gradually typed languages should offer some of the
+benefits of static typing. While classical type soundness, that
+well-typed programs are free from runtime errors, is not compatible
+with runtime type errors, we can instead focus on \emph{type-based
+reasoning}. For instance, while dynamically typed $\lambda$ calculi
+only satisfy $\beta$ equality for their type formers, statically typed
+$\lambda$ calculi additionally satisfy type-dependent $\eta$
+properties that ensure that functions are determined by their behavior
+under application and that pattern matching on data types
+is safe and exhaustive.
+
+Our goal in this work is to provide a reusable semantic framework for
+gradually typed languages that can be used to prove the aforementioned
+properties: graduality and type-based reasoning. \max{TODO: say more here}
\subsection{Current Approaches to Proving Graduality}
diff --git a/paper-new/paper.tex b/paper-new/paper.tex
index 0f96c97..8a62495 100644
--- a/paper-new/paper.tex
+++ b/paper-new/paper.tex
@@ -1,4 +1,4 @@
-\documentclass[sigconf,anonymous,review,screen]{acmart}
+\documentclass[sigconf,anonymous,review,screen,9pt]{acmart}
\let\Bbbk\relax
\usepackage{quiver}
@@ -124,6 +124,11 @@
% 5. Formalization in Guarded Cubical Agda
+\newif\ifdraft
+\drafttrue
+\renewcommand{\max}[1]{\ifdraft{\color{blue}[{\bf Max}: #1]}\fi}
+\newcommand{\eric}[1]{\ifdraft{\color{orange}[{\bf Steven}: #1]}\fi}
+\newcommand{\tingting}[1]{\ifdraft{\color{red}[{\bf Pedro}: #1]}\fi}
\input{intro}
--
GitLab