\documentclass{beamer}
\usetheme{boxes}

\newcommand{\notepr}[1]{}

%% \newif\ifshort
%% \newif\iflong

%% \shorttrue
%% %% \longtrue

\usepackage{rotating}
\usepackage{listings}
\usepackage{xcolor}
\lstset{
  basicstyle=\ttfamily,
  escapeinside=~~
}

\usepackage{microtype}
\usepackage{latexsym,amsmath,amssymb,amsthm}
\usepackage{mathpartir}
\usepackage{tikz}
\usepackage{tikz-cd}
\input{talk-defs}
\newcommand{\ltdyn}{\dynr}
\newcommand{\uarrow}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
\newcommand{\darrow}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
\renewcommand{\upcast}[2]{\langle{#2}\uarrow{#1}\rangle}
\renewcommand{\dncast}[2]{\langle{#1}\darrow{#2}\rangle}
\newcommand{\gtdyn}{\sqsupseteq}
\AtBeginSection[]
{
  \begin{frame}<beamer>
    %% \frametitle{Outline for section \thesection}
    \tableofcontents[currentsection]
  \end{frame}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% WARNING: I changed these commands
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\u}{\underline}

\newcommand{\pipe}{\,\,|\,\,}
\newcommand{\dynv}{{?}}
\newcommand{\dync}{\u {\text{?`}}}
\newcommand{\result}{\text{result}}
\newcommand{\Set}{\text{Set}}
\newcommand{\relto}{\to}
\newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square}
\newcommand{\lett}{\kw{let}}
\newcommand{\letXbeYinZ}[2]{\lett#2 = #1;}
\newcommand{\bindXtoYinZ}[2]{\kw{bind}#2 \leftarrow #1;}
\newcommand{\too}{\kw{to}}
\newcommand{\case}{\kw{case}}
\newcommand{\kw}[1]{\texttt{#1}\,\,}
\newcommand{\absurd}{\kw{absurd}}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\caseofX}[1]{\case #1}
\newcommand{\thenY}{\{}
\newcommand{\elseZ}[1]{\pipe #1 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
\newcommand{\pmpairWtoinZ}[2]{\kw{split} #1\,\kw{to} (). #2}
\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
\newcommand{\ret}{\kw{ret}}
\newcommand{\thunk}{\kw{thunk}}
\newcommand{\force}{\kw{force}}
\newcommand{\abort}{\kw {abort}}
\newcommand{\with}{\mathbin{\&}}
\DeclareMathOperator*{\With}{\&}


\title{A Type Theoretic Approach to Gradual Typing}
\author{Max S. New}
\institute{Northeastern University}
\date{\today}

\begin{document}

\begin{frame}
  \titlepage
  \begin{small}
    Joint work with\\
    Amal Ahmed (Northeastern),\\
    Dan Licata (Wesleyan)
  \end{small}
\end{frame}

\begin{frame}
  \frametitle{Outline}
  \tableofcontents
\end{frame}

\section{Intro to Gradual Typing}

\begin{frame}[fragile]{Gradual Typing is about Program Evolution}
\begin{columns}
\begin{column}{0.5\textwidth}
\begin{onlyenv}<1>
\begin{footnotesize}
\begin{lstlisting}
view(st) -> { ... }

update(event, state) -> {
  if first(state)
  then ... ; Loading
  else ... ; Valid Data
}

main() -> {
  st = initial_state;
  while true {
    evt = input();
    state = update(evt,st);
    display(view(st));
  }
}
\end{lstlisting}        
\end{footnotesize}
\end{onlyenv}
\begin{onlyenv}<2->
\begin{footnotesize}
\begin{lstlisting}
view(st) -> { ... }

update(event, state) -> {
  if first(state)
  then ... ; Loading
  else ... ; Valid Data
}

main() -> { .. }
\end{lstlisting}
\end{footnotesize}
\end{onlyenv}
\end{column}
\begin{column}{0.1\textwidth}
  \begin{onlyenv}<3->
  $\Longrightarrow$
\end{onlyenv}
\end{column}
\begin{column}{0.5\textwidth}{%
\begin{footnotesize}
\begin{onlyenv}<3->
\begin{lstlisting}
view(st) -> { ... }

~\colorbox{green}{type State = (Boolean, ?)}~
~\colorbox{green}{update : (?, State) -> State}~
update(event, state) -> {
  if first(state)
    then ... ; Loading
    else ... ; Valid Data
}
                
main() -> { ... }
\end{lstlisting}
\end{onlyenv}
\end{footnotesize}} \end{column}
\end{columns}
\end{frame}

\begin{frame}[fragile]{Gradual Typing is about Program Evolution}
\begin{columns}
\begin{column}{0.5\textwidth}{%
\begin{footnotesize}
\begin{onlyenv}<1->
\begin{lstlisting}
view(st) -> { ... }

~\colorbox{green}{type State = (Boolean, ?)}~
~\colorbox{green}{update : (?, State) -> State}~
update(event, state) -> {
  if first(state)
    then ... ; Loading
    else ... ; Valid Data
}
                
main() -> { ... }
\end{lstlisting}
\end{onlyenv}
\end{footnotesize}}
\end{column}
\begin{column}{0.1\textwidth}
\begin{onlyenv}<2->
  $\Longrightarrow$
\end{onlyenv}
\end{column}
\begin{column}{0.5\textwidth}{%
\begin{footnotesize}
\begin{onlyenv}<2->
\begin{lstlisting}
view(st) -> { ... }
~\colorbox{green}{type State = (Boolean, Num)}~
~\colorbox{green}{type Evt = NewData Num }~
        ~\colorbox{green}{| Cancel}~
~\colorbox{green}{update : (Evt, State) -> State}~
update(event, state) -> {
  if first(state)
  then ... ; Loading
  else ... ; Up to date
}
            
main() -> { ... }
\end{lstlisting}
\end{onlyenv}
\end{footnotesize}}
\end{column}
\end{columns}
\begin{onlyenv}<3->
  Code runs at every point, even though only \texttt{update} is typed.
\end{onlyenv}
\end{frame}

\begin{frame}{Gradual Typing Goals}
  Gradually Typed languages let dynamically typed and statically typed
  code interoperate within a single language.
  \begin{enumerate}
  \item Can write scripts, experimental code in the dynamically typed
    fragment.
  \item Can later add types to enforce interfaces, add documentation,
    prevent future bugs.
  \item But don't have to add types to the \emph{entire} program to
    run it!
  \end{enumerate}
\end{frame}

\begin{frame}{What do the Types Mean?}
  How do the types affect the semantics of the program?
  Two answers.
  \begin{enumerate}
  \item Optional Typing: they don't, just run the type erased
    programs. Dynamic typing is already safe anyway.
  \item Gradual Typing: a type system should give us a type
    \emph{soundness} theorem, need to check types at runtime in order
    to satisfy that.
  \end{enumerate}
\end{frame}

\begin{frame}{Cast Insertion}
  \begin{mathpar}
  \inferrule
  {\Gamma \vdash t : A \to B \and u : A' \and
    A \sim A'}
  {\Gamma \vdash t u : B}
  \end{mathpar}
  elaborates to a term with an explicit cast
  \[ t (\obcast{A'}{A}u) \]
\end{frame}

\begin{frame}{Semantics of Casts}
  \begin{center}
    \includegraphics[width=\textwidth,height=0.8\textheight,keepaspectratio]{Wadler-Findler-operational-semantics}
  \end{center}
\end{frame}

\begin{frame}{Semantics of Casts}
  \begin{align*}
    \obcast{A}{A}v &\mapsto v\\
    \obcast{A\to B}{A'\times B'}v & \mapsto \err\\
    \obcast{A\to B}{A' \to B'}v &\mapsto \lambda x. \obcast{B}{B'}(v (\obcast{A'}{A}x))\\
    \cdots
  \end{align*}
\end{frame}

\begin{frame}{}
  \begin{itemize}
  \item Many different semantics of casts
    \begin{itemize}
    \item For simple types alone: lazy, eager, up-down, partially
      eager, transient
    \end{itemize}
  \item Some seem especially natural: functorial interpretation.
  \end{itemize}
  What are the underlying principles?
  Which of them give us sound typing?
\end{frame}

\begin{frame}{A Type Theoretic Approach}
  \begin{enumerate}
  \item Simple axiomatization of the desired properties of types and
    casts.
  \item \emph{Derive} semantics of casts from these properties.
  \item We prove certain cast semantics are the only ones that satisfy
    our desired properties.
  \end{enumerate}
  Caveat: applies directly to the cast calculus, not the surface
  gradual language. See Abstracting Gradual Typing for a good
  explanation of the surface type checking.
\end{frame}

\begin{frame}{Properties of Gradual Typing}
  \begin{enumerate}
  \item \pause Dynamic Typing: Have a dynamic type into which all types can
    be encoded.
  \item \pause Type Soundness: Types should give associated
    reasoning principles: $\beta, \eta$ equality.
  \item \pause \emph{Graduality}: Transition from dynamic to static
    typing should only add type checking, not otherwise change
    behavior.
  \end{enumerate}
\end{frame}

\begin{frame}[fragile]{Graduality}
\begin{columns}
\begin{column}{0.5\textwidth}
\begin{onlyenv}<1->
\begin{footnotesize}
\begin{lstlisting}
view(st) -> { ... }

update(event, state) -> {
  if first(state)
  then ... ; Loading
  else ... ; Valid Data
}

main() -> { .. }
\end{lstlisting}
\end{footnotesize}
\end{onlyenv}
\end{column}
\begin{column}{0.1\textwidth}
  \begin{onlyenv}<1>
  $\Longrightarrow$
  \end{onlyenv}
  \begin{onlyenv}<2->
  $\gtdyn$
\end{onlyenv}
\end{column}
\begin{column}{0.5\textwidth}{%
\begin{footnotesize}
\begin{onlyenv}<1->
\begin{lstlisting}
view(st) -> { ... }

~\colorbox{green}{type State = (Boolean, ?)}~
~\colorbox{green}{update : (?, State) -> State}~
update(event, state) -> {
  if first(state)
    then ... ; Loading
    else ... ; Valid Data
}
                
main() -> { ... }
\end{lstlisting}
\end{onlyenv}
  \end{footnotesize}}
\end{column}
\end{columns}
  \begin{onlyenv}<2->
    Adding types \emph{refines} program behavior
  \end{onlyenv}
\end{frame}

\begin{frame}{Graduality}
  Syntactically,
  \[ t \ltdyn t' \]
  if $t$ and $t'$ have the same type erasure, and every type in $t$ is
  ``less dynamic'' than the corresponding type in $t'$

  \pause Operationally, if $t, t' : \texttt{Bool}$, then
  \begin{enumerate}
  \item $t$ runs to a type error (and $t'$ can do anything)
  \item $t$ and $t'$ diverge
  \item $t \mapsto \texttt{true}$ and $t' \mapsto \texttt{true}$
  \item $t \mapsto \texttt{false}$ and $t' \mapsto \texttt{false}$
  \end{enumerate}

  \pause
  \begin{itemize}
  \item Originally called the ``gradual guarantee'' in SNAPL '15
    (Siek-Vitousek-Cimini-Boyland)
  \item ``Graduality from Embedding-projection Pairs'' ICFP '18 with
    Amal Ahmed for more on the operational semantics POV
  \end{itemize}
\end{frame}

%% \begin{frame}{Evaluation in Gradual Typing}
%%   Say we have a function $\lambda x. t : \texttt{bool} \to \texttt{string}$ and
%%   we apply it to a dynamically typed value $v : \dyn$.
%%   \pause
%%   If $v$ is a boolean, fine
%%   \[ (\lambda x. t)(\texttt{true}) \mapsto t[\texttt{true}/x]
%%   \]
%%   \pause
%%   Otherwise, we raise an error
%%   \[ (\lambda x. t)(5) \mapsto \texttt{type error: expected ...}
%%   \]
%% \end{frame}

%% \begin{frame}{Evaluation in Gradual Typing}
%%   What if it's is a higher order function $\lambda x.t :
%%   (\texttt{number} \to \texttt{string})\to \texttt{num}$?
%%   \pause
%%   If $v$ is not a function, we error
%%   \[ (\lambda x.t)(\texttt{true}) \mapsto \texttt{type error:...}\]
%%   But if $v$ is a function? How can we verify that it takes numbers
%%   to strings?
%%   \begin{enumerate}
%%   \item\pause Run the type checker at runtime :(
%%   \item\pause Findler-Felleisen wrapping implementation:
%%     \[ (\lambda x.t)(\lambda y. u) \mapsto t[\lambda y. \texttt{string?}(u)/x]\]
%%   \item \pause Some combination: Annotate every value with best-known type
%%     information, use wrapping if the type information is not precise
%%     enough to tell.
%%   \end{enumerate}
%% \end{frame}

%% \begin{frame}{Type Soundness}
%%   \begin{enumerate}
%%   \item For simple types, usually defined as a safety property: if $t
%%     : A$ then $t$ diverges or $t$ runs to one of the allowed errors or
%%     $t$ runs to a value that has type $A$.
%%   \item \pause But there are also stronger, \emph{relational} soundness
%%     theorems
%%     \begin{enumerate}
%%     \item Function extensionality: $f_1 = f_2 : A \to B$ if for every
%%       $x : A$,  $f_1(x)$ has the same behavior as $f_2(x)$.
%%     \item Universal Polymorphism: $v : \forall \alpha. A$, then
%%       $v[B_1]$ and $v[B_2]$ ``do the same thing''.
%%     \item Local State/Existential Polymorphism: If I don't expose my
%%       representation, I can change it without breaking the program.
%%     \end{enumerate}
%%   \end{enumerate}
%% \end{frame}

\section{CBN Gradual Type Theory}

\begin{frame}{Call-by-name Gradual Type Theory}
  Start simple: $\lambda$ calculus with only negative types $\to,
  \times, 1$. Since effects are involved this is call-by-name
  evaluation. \\

  ``Call-by-name Gradual Type Theory'', FSCD 2018 with Dan Licata.
\end{frame}

\subsection{Syntax of GTT}

\begin{frame}{Syntax of Gradual Type Theory}
  4 sorts in Gradual Type Theory
  \begin{enumerate}
  \item Types $A,B,C$
  \item Terms $x_1 : A_1,\ldots, x_n:A_n \vdash t : A$
  \item \pause Type Dynamism: $A \ltdyn B$
  \item Term Dynamism: $x_1 \ltdyn y_1 : A_1 \ltdyn B_1,\ldots \vdash t \ltdyn u : A \ltdyn B$
  \end{enumerate}
\end{frame}

\begin{frame}{Types and Terms}
  Add dynamic type, casts, error to typed lambda calculus.
  \begin{mathpar}
    \begin{array}{rrl}
      \text{types} & A,B,C \bnfdef & \colorbox{lightgray}{$\dyn$} \bnfalt A \to B \bnfalt A \times B \bnfalt 1\\
      \text{terms} & s,t,u \bnfdef& x \bnfalt \lambda (x : A). t \bnfalt t u\\&&
      \bnfalt (t, u) \bnfalt \pi_i t \bnfalt ()\\&&
      \bnfalt \colorbox{lightgray}{$\err_{A}$} \bnfalt \colorbox{lightgray}{$\upcast A B t$} \bnfalt \colorbox{lightgray}{$\dncast A B t$}
    \end{array}
  \end{mathpar}
\end{frame}
%% \begin{frame}{Terms}
%%   Terms are all intrinsically typed, we have variables and
%%   substitution as usual.
%%   %% and we can also add function symbols as
%%   %% primitives.

%%   \begin{mathpar}
%%     \inferrule
%%     {x:A \in \Gamma}
%%     {\Gamma \vdash x : A}

%%     \inferrule
%%     {\Gamma \vdash u : B\and
%%       \Gamma, x: B \vdash t : A}
%%     {\Gamma \vdash t[u/x] : A}

%%     \inferrule
%%     {\Gamma \vdash t_1 : A_1,\ldots, \Gamma \vdash t_n : A_n \and f : (A_1,\ldots,A_n) \to B}
%%     {\Gamma \vdash f(t_1,\ldots,t_n) : B}
%%   \end{mathpar}
%% \end{frame}

\begin{frame}{Type Dynamism}
  \[ A \ltdyn B \]
  read: $A$ is ``less dynamic''/''more precise'' than $B$. \\
  \begin{itemize}
  \item Syntactic intuition: $B$ has more $\dyn$s in it.
  \item Semantic intuition: $A$ supports fewer interactions than $B$.
  \end{itemize}
\end{frame}

\begin{frame}{Type Dynamism Axioms}
  \begin{mathpar}
  \inferrule{~}{A \dynr A}\and
  \inferrule{A \dynr B \and B \dynr C}{A \dynr C}\and
  \inferrule{~}{A \ltdyn \dyn}\\
  \inferrule{A \ltdyn A' \and B \ltdyn B'}{A \to B \ltdyn A' \to B'}\and
  \inferrule{A \ltdyn A' \and B \ltdyn B'}{A \times B \ltdyn A' \times B'}
  \end{mathpar}
  NB: Covariant function rule
\end{frame}

%% \begin{frame}{Term Dynamism INTUITION}
%%   Models the refinement relation of gradual guarantee. Here's an example
%%   \emph{model} for intuition.\\
%%   \pause
%%   For every $A \ltdyn A'$, if
%%   \begin{mathpar}
%%     \cdot  \vdash t \ltdyn t' : A \ltdyn A'
%%   \end{mathpar}
%%   Then either
%%   \begin{enumerate}
%%   \item $t$ runs to a type error.
%%   \item $t,t'$ both diverge
%%   \item $t \Downarrow v$ and $t' \Downarrow v'$ and $v \ltdyn v'$.
%%   \end{enumerate}
  
%%   \notepr{
%%   The $A \ltdyn A'$ restriction ensures we have a sensible
%%   way to interpret that.
%%   }
%% \end{frame}

\begin{frame}{Term Dynamism}
  \begin{mathpar}
    x_1 \ltdyn x_1' : A_1 \ltdyn A_1' ,\ldots \vdash t \ltdyn t' : B \ltdyn B' 
  \end{mathpar}
  read: ``if all the $x_i$s are less than $x_i'$s then $t$ is less than $t'$''.\\
  \pause
  Note that it is only well formed if all of the $A_i \ltdyn A_i'$ and
  $B \ltdyn B'$. and
  \begin{mathpar}
    x_1:A_1,\ldots\vdash t : B\\
    x_1':A_1',\ldots\vdash t' : B'\\
  \end{mathpar}
  %% We sometimes abbreviate the context ordering as $\Phi \vdash t
  %% \ltdyn t' : B \ltdyn B'$.
  \pause
  This very explicit notation gets very big, so I'll simplify in the
  talk. Abbreviate the above as:
  \[
  \Phi \vdash t \ltdyn t' : B \ltdyn B'
  \]
\end{frame}

\begin{frame}{Type Error}
  The type error is the \emph{least} dynamic term, modeling
  graduality.

  \[ \Phi \vdash \err_A \ltdyn t : A \ltdyn A' \]
\end{frame}

\begin{frame}{Term Dynamism Axioms}
  Identity and substitution are monotone.
  %% For open terms, identity and substitution properties that should
  %% evoke a logical relation interpretation. Substitution says that
  %% every term is monotone in its free variables.
  \begin{mathpar}
    \inferrule
    {(x \ltdyn x' : A \ltdyn A') \in \Phi}
    {\Phi \vdash x \ltdyn x' : A \ltdyn A'}

    \inferrule
        {x \ltdyn x' : A \ltdyn A' \vdash t \ltdyn t' \and
      u \ltdyn u' : A \ltdyn A'}
    {t[u/x] \ltdyn t'[u'/x']}
  \end{mathpar}
  %% \pause Note that these are the same as ordinary identity and
  %% substitution but ``monotonically''.
\end{frame}

\begin{frame}{Term Dynamism}
  Like type dynamism, term dynamism has reflexivity and transitivity
  rules:
  %% note
  %% how well-formedness relies on the reflexivity and transitivity of
  %% type dynamism

  \begin{mathpar}
    \inferrule
    {\vdash t : B}
    {t \ltdyn t : B \ltdyn B}

    \inferrule
    {t \ltdyn t' : B \ltdyn B'\\
     t' \ltdyn t'' : B' \ltdyn B''}
    {t \ltdyn t'' : B \ltdyn B''}
  \end{mathpar}
\end{frame}

%% \begin{frame}[fragile]{Term Dynamism Squares}
%%   These can be nicely visualized as squares:
%%   For $\Phi : \Gamma \ltdyn \Gamma'$, we can think of 
%%   \[ \Phi \vdash t \ltdyn t' : A \ltdyn A' \]
%%   as
%%   \[
%%   \begin{tikzcd}
%%     \Gamma \arrow[ dashed , r, "\preciser" ] \arrow[ d, swap, "t" ]
%%     &
%%     \Gamma' \arrow[d , "t'"]
%%     \\
%%     A \arrow[ dashed , r, "\preciser" ]
%%     &
%%     A'
%%   \end{tikzcd}
%%   \]
  
%% \end{frame}

\begin{frame}[fragile]{Graphical View of Dynamism}
  Can help to visualize these as \emph{squares}.
  \[
  x \ltdyn x' : A \ltdyn A' \vdash t \ltdyn t' : B \ltdyn B'
  \]

  becomes
  \begin{tikzcd}
    x:A \arrow[dd] \arrow[rr, "t"] &  & B \arrow[dd] \\
    & \sqsubseteq &  \\
    x':A' \arrow[rr, "t'"] &  & B'
  \end{tikzcd}        
\end{frame}

\begin{frame}[fragile]{Graphical View of Dynamism}
  Substitution principle/monotonicity corresponds to horizontal
  composition of squares.
    \begin{columns}
    \begin{column}{0.45\textwidth}
  \begin{tikzcd}
    A \arrow[r,"u"]\arrow[d] & B \arrow[r,"t"]\arrow[d] & C\arrow[d]\\
    A' \arrow[r,"u'"] & B'\arrow[r,"t'"]& C
  \end{tikzcd}
    \end{column}
    \begin{column}{0.45\textwidth}
      \begin{tikzcd}
        A \arrow[d] \arrow[r, "id"] & A \arrow[d] \\
        B \arrow[r, "id"] & B
      \end{tikzcd}      
    \end{column}
    \end{columns}
    \begin{columns}
    \begin{column}{0.45\textwidth}
      \begin{mathpar}
        \inferrule{x \ltdyn x' \vdash t \ltdyn t'\\ u \ltdyn u'}
                  {t[u/x] \ltdyn t'[u'/x]}
      \end{mathpar}
    \end{column}
    \begin{column}{0.45\textwidth}
      \begin{mathpar}
          \inferrule
          {}
          {x\ltdyn x' : A \ltdyn A' \vdash x \ltdyn x' : A \ltdyn A'}
      \end{mathpar}
    \end{column}
    \end{columns}
\end{frame}

\begin{frame}[fragile]{Graphical View of Dynamism}
  Vertical composition of squares is \emph{transitivity and reflexivity}.
    \begin{columns}
    \begin{column}{0.45\textwidth}
  \begin{tikzcd}
\Gamma \arrow[d] \arrow[r,"t"] & A \arrow[d] \\
\Gamma' \arrow[d] \arrow[r,"t'"] & A' \arrow[d] \\
\Gamma'' \arrow[r,"t''"] & A''
  \end{tikzcd}
    \end{column}
    \begin{column}{0.45\textwidth}
      \begin{tikzcd}
A \arrow[d, "id"] \arrow[r, "t"] & B \arrow[d, "id"] \\
A \arrow[r, "t"] & B
\end{tikzcd}
    \end{column}
    \end{columns}
    \begin{columns}
    \begin{column}{0.45\textwidth}
      \begin{mathpar}
        \inferrule{\Gamma \ltdyn \Gamma' \vdash t \ltdyn t' : A \ltdyn A'\\
          \Gamma' \ltdyn \Gamma'' \vdash t' \ltdyn t'' : A' \ltdyn A''}
                  {\Gamma \ltdyn \Gamma'' \vdash t \ltdyn t'' : A \ltdyn A''}
      \end{mathpar}
    \end{column}
    \begin{column}{0.45\textwidth}
      \begin{mathpar}
          \inferrule
          {\Gamma \vdash t : A}
          {\Gamma \ltdyn \Gamma \vdash t \ltdyn t : A \ltdyn A}
      \end{mathpar}
    \end{column}
    \end{columns}
    \pause Aside: Squares can be thought of as 2-cells in a double
    category, which was the inspiration for the whole approach.
\end{frame}

\begin{frame}{Function Type}
  First, we give have the usual term structure for the function type
  \begin{mathpar}
    \inferrule
    {\Gamma, x : A \vdash t : B}
    {\Gamma \vdash \lambda x:A. t : A \to B}

    \inferrule
    {\Gamma \vdash t : A \to B\and \Gamma \vdash u : A}
    {\Gamma \vdash t u : B}
  \end{mathpar}
  \pause
  And we add the $\beta, \eta$ laws as ``equi-dynamism'' axioms:

  \begin{mathpar}
    \inferrule
    {}
    {(\lambda x:A. t) u \equidyn t[u/x]}

    \inferrule
    {t : A \to B}
    {t \equidyn (\lambda x:A. t x)}
  \end{mathpar}
\end{frame}

\begin{frame}{Function Type}
  Next to model graduality, we add \emph{congruence} rules.
  \begin{mathpar}
    \inferrule
    {A \ltdyn A' \and B \ltdyn B'}
    {A \to B \ltdyn A' \to B'}\\
    \inferrule
    {x \ltdyn x' : A \ltdyn A' \vdash t \ltdyn t' : B \ltdyn B'}
    {\lambda x:A. t \ltdyn \lambda x':A'.t' }

    \inferrule
    {t \ltdyn t' : A \to B \ltdyn A' \to B'\and
      u \ltdyn u' : A \ltdyn A' %% \and B \ltdyn B'
    }
    {t\, u \ltdyn t'\, u' : B \ltdyn B'}
  \end{mathpar}
\end{frame}

\begin{frame}{Product Type}
  Product and (unit types) get a similar treatment.
  \begin{mathpar}
    \inferrule
    {\Gamma  \vdash t_1 : A_1\\ \Gamma \vdash t_2 : A_2}
    {\Gamma \vdash (t_1,t_2) : A_1 \times A_2}

    \inferrule
    {\Gamma \vdash t : A_1 \times A_2}
    {\Gamma \vdash \pi_i t : A_i}\\

    \inferrule
    {}
    {\pi_i(t_1,t_2) \equidyn t_i}

    \inferrule
    {t : A_1 \times A_2}
    {t \equidyn (\pi_1 t, \pi_2 t)}\\

    \inferrule{t_1 \ltdyn t_1' : A_1 \ltdyn A_1' \and t_2 \ltdyn t_2' : A_2 \ltdyn A_2'}{(t_1,t_1') \ltdyn (t_2,t_2') : A_1 \times A_2 \ltdyn A_1' \times A_2'}
    
    \inferrule{t \ltdyn t' : A_1 \times A_2 \ltdyn A_1' \times A_2' \and A_i \ltdyn A_i'}{\pi_i t \ltdyn \pi_i t' : A_i \ltdyn A_i'}
  \end{mathpar}
\end{frame}

\begin{frame}{Casts}
  How to define the casts axiomatically?
  \begin{itemize}
  \item We \emph{characterize} them by a property with respect to $\ltdyn$.
  \item We can do this when our casts are \emph{upcasts} or
    \emph{downcasts}.
  \end{itemize}
\end{frame}

\begin{frame}{Casts}
  When $A \ltdyn B$, we get two functions: the \emph{upcast} $\upcast
  A B$ and the \emph{downcast} $\dncast A B$.

  \begin{mathpar}
    \inferrule
    {\Gamma \vdash t : A \and A \ltdyn B}
    {\Gamma \vdash \upcast A B t : B}

    \inferrule
    {\Gamma \vdash u : B \and A \ltdyn B}
    {\Gamma \vdash \dncast A B u : A}
  \end{mathpar}
\end{frame}

\begin{frame}{Oblique Casts}
  Not every cast in gradual typing is an upcast or a downcast, for
  instance the cast

  \[ \obcast {\texttt{Bool} \times \dyn} {\dyn \times \texttt{Bool}} \]

  But in almost every gradual system, these are equivalent to casting
  through the dynamic type:

  \[ \obcast{A}{B}t = \dncast B \dyn \upcast A \dyn t\]
\end{frame}

\begin{frame}{Casts}
  How should casts behave?
  %% Intuition: the casted term should act as much like the original term
  %% as possible while still satisfying the new type.
  \pause

  So for a downcast, the casted term should refine the original:
  %% ``Elimination Rule''
  \begin{mathpar}
    \inferrule
    {u : B \and A \ltdyn B}
    {\dncast A B u \ltdyn u : A \ltdyn B}
  \end{mathpar}

  \pause But this would be satisfied even by the type error $\err_A$.
  \pause
  We want to make sure that the casted term has \emph{as much}
  behavior as possible: i.e., it's the \emph{biggest} term below
  $u$.
  \begin{mathpar}
    \inferrule
    {\Phi \vdash t \ltdyn u : A \ltdyn B}
    {\Phi \vdash t \ltdyn \dncast A B u : A}
  \end{mathpar}
  \pause Order-theoretic summary: $\dncast A B u$ is the greatest
  lower bound of $u$ in $A$.
\end{frame}

\begin{frame}{Casts}
  Upcasts are the exact dual

  For an upcast, the casted term should be \emph{more} dynamic than
  the original:
  \begin{mathpar}
    \inferrule
    {t : A \and A \ltdyn B}
    {t \ltdyn \upcast A B t : A \ltdyn B}
  \end{mathpar}

  But it has no more behaviors than dictated by the original term,
  it's the \emph{least} term above $t$.

  \begin{mathpar}
    \inferrule
    {\Phi \vdash t \ltdyn u : A \ltdyn B}
    {\Phi \vdash \upcast A B t \ltdyn u : B}
  \end{mathpar}
  \pause Order-theoretic summary: $\upcast A B u$ is the least upper
  bound of $t$ in $B$.
\end{frame}

\begin{frame}{Casts}
  \begin{enumerate}
  \item Note that this is a \emph{precise} specification because lubs
    and glbs are unique (up to $\equidyn$).
  \item Category theoretic terminology: this is a \emph{universal
    property} for upcasts and downcasts.
  \item Since they are exact \emph{duals} most theorems about one
    dualize for the other.
  \end{enumerate}
\end{frame}

\subsection{Theorems in GTT}

\begin{frame}{Consequences of GTT}
  \begin{itemize}
  \item Now we have a simple ``logic'' of term dynamism, what can we
    \emph{prove} in the theory?
  \item Theorems in the theory apply to any model, i.e. a simple lazy
    gradually typed language.
  \end{itemize}
\end{frame}

\begin{frame}{Derivation of Function Casts}
  We can prove that the ``function contract'' is the unique
  implementation of casts between function types. I.e. if $A \ltdyn
  A'$ and $B \ltdyn B'$ and $t : A' \to B'$ then

  \[
  \dncast {A \to B} {A' \to B'} t \equidyn \lambda x:A. \dncast{B}{B'}(t (\upcast A {A'} x))
  \]
  and
  \[
  \upcast {A \to B} {A' \to B'} t \equidyn \lambda x':A'. \upcast{B}{B'}(t (\dncast A {A'} x'))
  \]
\end{frame}

\begin{frame}{Derivation of Function Casts}
  One direction:
  To prove
  \[ \dncast {A \to B} {A' \to B'} t \ltdyn \lambda x:A. \dncast{B}{B'}(t (\upcast A {A'} x))
  \]
  By $\eta$, it is sufficient to show
  \[
  x : A \vdash (\dncast {A \to B} {A' \to B'} t) x \ltdyn \dncast{B}{B'}(t (\upcast A {A'} x))
  \]
  Then it follows by congruence because:
  \begin{enumerate}
  \item $(\dncast {A \to B} {A' \to B'} t)\ltdyn t$
  \item $x \ltdyn \upcast A {A'} x$
  \item if $u \ltdyn u'$ then $u \ltdyn \dncast {B} {B'} u'$
  \end{enumerate}
  \pause
  Other 3 cases are similar/dual.
  \pause
  All just $\beta,\eta$ and congruence. Applies to any type defined
  this way: $\times$, $1$.
\end{frame}

\begin{frame}{Casts are Galois Connections}
  \notepr{  First, we can show that every pair of upcast and downcast forms a
  Galois connection, which}

  Two ``round-trip'' properties:
  \pause
  Casting down and back up has ``more errors''
  \begin{mathpar}
    \inferrule
    {u : B \and A \ltdyn B}
    {\upcast A B \dncast A B u \ltdyn u : B}
  \end{mathpar}
  \pause
  And casting up and back down has ``fewer errors''
  \begin{mathpar}
    \inferrule
    {t : A \and A \ltdyn B}
    {t \ltdyn \dncast A B \upcast A B t : A}
  \end{mathpar}
  \pause In practice, we strengthen this to an
  equality, so we can add the ``retract axiom'' as well to the system
  (though none of the theorems I'll show depend on it):
  \begin{mathpar}
    \inferrule*[right=RETRACT-AXIOM]
    {t : A \and A \ltdyn B}
    {\dncast A B \upcast A B t \ltdyn t : A}
  \end{mathpar}
  but only need to add it as an axiom for ``base casts''
\end{frame}

\begin{frame}{Identity and Composition}
  Reflexivity gives the identity cast and transitivity gives the
  composition of casts
  \begin{enumerate}
  \item $\dncast A A t \equidyn t$
  \item If $A \ltdyn B \ltdyn C$, then $\dncast A C t \equidyn \dncast A B \dncast B C t$
  \end{enumerate}
  \pause
  These are part of the operational semantics for instance:
  \begin{align*}
    \dncast{\dyn}{\dyn} v &\mapsto v\\
    \dncast{A \to B}{\dyn} v &\mapsto \dncast {A \to B}{\dyn \to \dyn}\dncast {\dyn \to \dyn} \dyn v
  \end{align*}
\end{frame}

%% \begin{frame}{Identity Cast}
%%   The upcast/downcast from $A$ to $A$ is the identity function,
%%   i.e. $\upcast A A t \equidyn t$.  Each direction is an instance of
%%   the specification of upcasts:

%%   \begin{mathpar}
%%   \inferrule*[right=UR]
%%       {~}
%%       {t \ltdyn \upcast{A}{A}{t} : A}\and

%%   \inferrule*[right=UL]
%%       {t \ltdyn t : A \ltdyn A}
%%       {\upcast{A}{A}{t} \ltdyn t : A}
%%   \end{mathpar}

%%   Downcast proof is precise dual.
%% \end{frame}

%% \begin{frame}{Casts (de)compose}
%%   If $A \ltdyn B \ltdyn C$ then a cast between $A$ and $B$ factors
%%   through $C$:

%%   \begin{mathpar}
%%     \inferrule
%%     {A \ltdyn B \ltdyn C}
%%     {\dncast A B \dncast B C t \equidyn \dncast A C t}
%%   \end{mathpar}

%%   Example: casts between dynamic type and function types factor
%%   through ``most dynamic'' function type:
%%   \begin{mathpar}
%%     \dncast {A \to B}{\dyn \to \dyn}\dncast \dyn {\dyn \to \dyn} t \equidyn \dncast{A \to B}{\dyn} t
%%   \end{mathpar}
%%   This is often a rule of the operational semantics.
%% \end{frame}

\begin{frame}{Non-theorem: Disjointness of Constructors}
  The only standard operational rules we cannot prove are the ones like
  \[
  \obcast {A \times B} {A' \to B'} t \mapsto \err
  \]
  that say that the type constructors $\times, \to, 1$ are all
  disjoint.

  Independent of the axioms: have models where it's true and
  false. This is the actual ``design space''.

  %% In fact, written as equidynamism instead of stepping, these are
  %% \emph{independent} of the other axioms: we can construct adequate
  %% models where it's true and ones where it's false(!)

  %% The reason is that our definition of function types, product types
  %% et cetera only defines them \emph{up to isomorphism}, not up to cast
  %% equivalence. And we know very little about the dynamic type, just
  %% that everything embeds in it.
\end{frame}

%% \begin{frame}{Term Dynamism Reduces to Globular Dynamism}
%%   The presence of the casts means that we can reduce all type dynamism
%%   to ordering \emph{at the same type}, which is more typical for
%%   logical relations.
%%   \begin{mathpar}
%%     {x \ltdyn y : A \ltdyn B \vdash t \ltdyn u : C \ltdyn D}\\
%%     \iff\\
%%     {x \ltdyn x : A \ltdyn A \vdash t \ltdyn \dncast C D u[\upcast A B x/y] : C \ltdyn C}\\
%%     \iff\\
%%     {x \ltdyn x : A \ltdyn A \vdash \upcast C D t \ltdyn u[\upcast A B x/y] : D \ltdyn D}\\
%%     \iff\\
%%     {y \ltdyn y : B \ltdyn B \vdash \upcast C D t[\dncast A B y/x] \ltdyn u : D \ltdyn D}\\
%%     \iff\\
%%     {y \ltdyn y : B \ltdyn B \vdash t[\dncast A B y/x] \ltdyn \dncast C D u : C \ltdyn C}\\
%%   \end{mathpar}
%% \end{frame}

\subsection{Models of GTT}

\begin{frame}{Models of GTT}
  \begin{enumerate}
  \item In FSCD Paper,
    \begin{enumerate}
    \item Sound and complete category theoretic semantics using double
      categories.
    \item Adequate domain theoretic model where domains have domain
      structure and error ordering modeling $\ltdyn$.
    \end{enumerate}
  \end{enumerate}
\end{frame}

\begin{frame}{Summary}
  \begin{enumerate}
  \item Can derive that the functorial interpretation of casts is the
    only one that satisfies graduality and $\beta, \eta$.
  \item In practice, other cast semantics break $\eta$, breaking
    type-based reasoning!
  \end{enumerate}
\end{frame}

\section{CBPV Gradual Type Theory}

\subsection{Overview of Call-by-push-value}

\begin{frame}{Call-by-push-value GTT}
  Want to extend theorems to CBV, but still want a simple axiomatic
  presentation of the type theory that works with positives, negatives
  and effects.

  Answer is a polarized type theory: Call-by-push-value.\\
  
  Conditionally accepted to POPL 2018: ``Gradual Type Theory'' with
  Dan Licata and Amal Ahmed.
\end{frame}

\begin{frame}{Types, Judgments of CBPV}
  \begin{mathpar}
    \begin{array}{rl}
      \text{value types}\,\,A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2\\
      \text{computation types}\,\,\u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
      \text{types}\,\, T ::= & A \mid \u B\\
      \Gamma ::= & x:A,\ldots\\
      \Delta ::= & \bullet : \u B\\
    \end{array}
  \end{mathpar}
  Three judgments
  \begin{enumerate}
  \item Computations $\Gamma \vdash M : \u B$: effectful terms
  \item Values $\Gamma \vdash V : A$: pure function that returns an $A$
  \item Stacks $\Gamma \pipe \bullet:B \vdash S : B'$, strict function
    that forces the hole $\bullet : B$ whenever it is forced.
  \end{enumerate}
\end{frame}

\begin{frame}{Functions}
  \begin{mathpar}
    \inferrule
    {\Gamma, x : A \vdash M : B}
    {\Gamma \vdash \lambda x. M : A \to B}

    \inferrule
    {\Gamma \vdash M : A \to B \and
    \Gamma \vdash V : A}
    {\Gamma \vdash M V : B}

    (\lambda x. M) V \equiv M[V/x]\\
    (M : A \to B) \equiv \lambda x. M x\\

    \pause
    \inferrule
    {\Gamma, x: A \pipe \Delta \vdash S : B }
    {\Gamma \pipe \Delta \vdash \lambda x. S : A \to B}

    \inferrule
    {\Gamma \pipe \Delta \vdash S : A \to B\and
      \Gamma \vdash V : A}
    {\Gamma \pipe \Delta \vdash S V : B}
  \end{mathpar}
\end{frame}

\begin{frame}{Strict Pairs}
  \begin{mathpar}
    \inferrule
    {\Gamma \vdash V_i : A_i}
    {\Gamma \vdash (V_1,V_2) : A_1\times A_2}

    \inferrule
    {\Gamma \vdash V : A_1\times A_2\and
      \Gamma, x_1:A_1,x_2:A_2 \vdash E : T}
    {\Gamma \vdash \pmpairWtoXYinZ V {x_1} {x_2} E : T}

    \pmpairWtoXYinZ {(V_1,V_2)} {x_1} {x_2} E \equiv E[V_1/x_1][V_2/x_2]\\
    x : A_1\times A_2 \vdash E \equiv \pmpairWtoXYinZ x {x_1}{x_2} E[(x_1,x_2)/x]
  \end{mathpar}
\end{frame}

\begin{frame}{Shifts}
  A computation of type $\u F A$ is something that performs effects
  and returns $A$s.
  \begin{mathpar}
    \inferrule
    {\Gamma \vdash V : A}
    {\Gamma \vdash \ret V : \u F A}

    \inferrule
    {\Gamma \vdash M : \u F A\and
      \Gamma, x : A \vdash N : \u B}
    {\Gamma \vdash \bindXtoYinZ M x N : \u B}

    \inferrule
    {\Gamma\pipe\Delta \vdash S : \u F A\and
      \Gamma, x : A \vdash N : \u B}
    {\Gamma \vdash \bindXtoYinZ S x N : \u B}

    \bindXtoYinZ {\ret V} x N \equiv N[V/x]\\
    \bullet : \u F A \vdash S \equiv \bindXtoYinZ \bullet x S[\ret x/\bullet]
  \end{mathpar}
\end{frame}

\begin{frame}{Shifts}
  A value of type $U \u B$ is a thunk that when forced behaves as $\u B$.
  \begin{mathpar}
    \inferrule
    {\Gamma \vdash M : \u B}
    {\Gamma \vdash \thunk M : U \u B}

    \inferrule
    {\Gamma \vdash V : U \u B}
    {\Gamma \vdash \force V : \u B}\\

    \force \thunk M \equiv M\\
    V : U \u B \equiv \thunk \force V
  \end{mathpar}
\end{frame}

\begin{frame}{Embedding CBV, CBN}
  CBV types become value types:
  \begin{align*}
    (A \mathop{+_{cbv}} A') &= A + A'\\
    (A \mathop{\to_{cbv}} A') &= U(A \to \u F A')
  \end{align*}
  And CBV computations:
  \[ \Gamma \mathrel{\vdash^{cbv}} M : A \Rightarrow \Gamma \vdash M : \u F A \]
  CBN types become computation types:
  \begin{align*}
    (\u B \mathop{+_{cbn}} \u B') &= \u F (U\u B + U \u B')\\
    (\u B \mathop{\to_{cbn}} \u B') &= U\u B \to \u B'
  \end{align*}
  And CBN computations:
  \[
  x_1:\u B_1,\ldots \vdash M : \u B \Rightarrow x_1:U\u B_1,\ldots \vdash M : \u B
  \]
\end{frame}

\subsection{Casts and Dynamic Types}

\begin{frame}{CBPV Gradual Type Theory}
  Goal: gradualize CBPV. Should reproduce our CBN work and the
  existing CBV semantics.

  \begin{enumerate}
  \item Add dynamism ordering $\ltdyn$.
  \item Define casts by universal property.
  \item Add dynamic type(s?)
  \end{enumerate}
\end{frame}

\begin{frame}{Dynamism Ordering}
  Easy: new ordering judgment for types and values/stacks/computations.
  Everything is monotone.

  \begin{mathpar}
    \inferrule
    {A \ltdyn A'}
    {\u F A \ltdyn \u F A'}

    \inferrule
    {A_1 \ltdyn A_1' \and A_2 \ltdyn A_2'}
    {A_1 \times A_2 \ltdyn A_1' \times A_2'}\\

    \inferrule
    {\u B \ltdyn \u B'}
    {U \u B \ltdyn U \u B'}

    \inferrule
    {A \ltdyn A' \and \u B \ltdyn \u B'}
    {A \to \u B \ltdyn A' \to \u B'}
  \end{mathpar}
\end{frame}

\begin{frame}{Errors}
  \begin{mathpar}
    \Gamma \vdash \err : \u B\\

    \inferrule
    {}
    {\Gamma \vdash \err \ltdyn M : \u B}

    \inferrule
    {}
    {\Gamma \vdash S[\err/\bullet] \equidyn \err : \u B}
  \end{mathpar}
\end{frame}

\begin{frame}{Which casts?}
  If we embed from cbv, cbn. we get ``Kleisli'' and ``CoKleisli''
  casts.

  From CBV:
  \begin{mathpar}
    \inferrule
    {\Gamma \vdash V : A \and A \ltdyn A'}
    {\Gamma \vdash \upcast{A}{A'}V : \u F A'}

    \inferrule
    {\Gamma \vdash V : A' \and A \ltdyn A'}
    {\Gamma \vdash \dncast{A}{A'}V : \u F A}
  \end{mathpar}

  From CBN:
  \begin{mathpar}
    \inferrule
    {\Gamma \vdash V : U \u B \and \u B \ltdyn \u B'}
    {\Gamma \vdash \upcast{\u B}{\u B'}V : \u B'}

    \inferrule
    {\Gamma \vdash V : U \u B' \and \u B \ltdyn \u B'}
    {\Gamma \vdash \dncast{\u B}{\u B'}V : \u B}
  \end{mathpar}
\end{frame}

\begin{frame}{Embeddings are Values, Projections are Stacks}
  Observation from CBV: in practice the upcasts are ``pure'': the
  basic ones are sum type injections, others are functorial liftings
  of pure functions.

  CBPV lets us axiomatize this directly, along with the \emph{dual}
  that downcasts \emph{stacks} between computation types:
  \begin{mathpar}
    \inferrule
    {\Gamma \vdash V : A}
    {\Gamma \vdash \upcast{A}{A'}V : A'}

    %% \inferrule
    %% {\Gamma \vdash M : \u B}
    %% {\Gamma \vdash \dncast{\u B}{\u B'}M : \u B'}

    \inferrule
    {\Gamma\pipe \Delta \vdash S : \u B}
    {\Gamma\pipe \Delta \vdash \dncast{\u B}{\u B'}S : \u B'}
  \end{mathpar}
  Should be useful for compilation/optimization.
\end{frame}

\begin{frame}{Embeddings are Values, Projections are Stacks}
  ``Missing'' casts come from the shifts:
  \begin{mathpar}
    \inferrule
    {\Gamma \vdash V : A \and A \ltdyn A'}
    {\Gamma \vdash \upcast{A}{A'}V : A'}

    %% \inferrule
    %% {\Gamma \vdash M : \u B}
    %% {\Gamma \vdash \dncast{\u B}{\u B'}M : \u B'}

    \inferrule
    {\Gamma\pipe \Delta \vdash S : \u B \and \u B \ltdyn \u B'}
    {\Gamma\pipe \Delta \vdash \dncast{\u B}{\u B'}S : \u B'}

    \inferrule
    {\Gamma \vdash M : \u F A \and \inferrule{A \ltdyn A'}{\u F A \ltdyn \u F A'}}
    {\Gamma \vdash \dncast{\u F A}{\u F A'}M : \u F A}

    \inferrule
    {\Gamma \vdash V : U \u B \and
      \inferrule{\u B \ltdyn \u B'}{U \u B \ltdyn U \u B'}}
    {\Gamma \vdash \upcast{U \u B}{U \u B'}V : U\u B'}
  \end{mathpar}
\end{frame}

\begin{frame}{Cast Universal Properties}
  Just like for CBN:
  \begin{mathpar}
    \inferrule
    {V : A \and A \ltdyn A'}
    {V \ltdyn \upcast A {A'} V : A \ltdyn A'}

    \inferrule
    {V \ltdyn V' : A \ltdyn A'}
    {\upcast A {A'} V \ltdyn V' : A'}

    \inferrule
    {M : \u B \and \u B \ltdyn \u B'}
    {\dncast{\u B}{\u B'}M \ltdyn M}

    \inferrule
    {M \ltdyn M' : \u B \ltdyn \u B'}
    {M \ltdyn \dncast {\u B}{\u B'} M' : \u B}
  \end{mathpar}
\end{frame}

\begin{frame}{Strict Product Cast}
  Derivable:
  \begin{mathpar}
    \upcast{A_1 \times A_2}{A_1'\times A_2'}V \equidyn\\
    \pmpairWtoXYinZ V {x_1}{x_2} (\upcast{A_1}{A_1'}x_1, \upcast{A_2}{A_2'}x_2)\\
    \end{mathpar}

    \begin{mathpar}
      
    \dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)}{M}\\
    \begin{array}{rcl}
&
      \equidyn & 
      \bindXtoYinZ{M}{p'} {\pmpairWtoXYinZ{p'}{x_1'}{x_2'}{}}\\
      & & \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1}\\
      & & \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} {\ret (x_1,x_2) }\\
    \end{array}
    \end{mathpar}
    Note: evaluation order of the two casts doesn't matter.
\end{frame}

\begin{frame}{CBV and CBN Uniqueness Principles}
  \begin{mathpar}
    \dncast{A \to \u B}{A' \to \u B'}M \equidyn
    \lambda x. \dncast{\u B}{\u B'}(M (\upcast{A}{A'}x))
  \end{mathpar}
  \begin{mathpar}
      \upcast{U (A \to \u B)}{U (A' \to \u B')}{f} \equidyn
    \begin{array}{ll}
      \thunk (\lambda x'. & \bindXtoYinZ{\dncast{\u F A}{\u F A'}{(\ret x')}}{x}{} \\
      & { \force{(\upcast{U \u B}{U \u B'}{(\thunk{(\force{f}\,x)})})}})
    \end{array}
  \end{mathpar}
\end{frame}

\begin{frame}{Two Dynamic Types}
  Add a dynamic value type $\dynv$ and a dynamic computation type
  $\dync$.

  \begin{mathpar}
    \inferrule
    {}
    {A \ltdyn \dynv}

    \inferrule
    {}
    {\u B \ltdyn \dync}
  \end{mathpar}

  So we always have casts:
  \begin{mathpar}
    \inferrule{V : A}{\upcast{A}{\dynv}V : \dynv}\and
    \inferrule{M : \dync}{\dncast{\u B}{\dync}M : \u B}
  \end{mathpar}
\end{frame}

%% \begin{frame}{Translation to CBPV}
%%   A model of GTT in CBPV
%%   \begin{enumerate}
%%   \item A gradual value type $A$ denotes a pair of a type $[A]$ and an
%%     interpretation of the upcast $\upcast{[A]}{[\dynv]}$ and the
%%     downcast $\dncast{\u F [A]}\u F{\dynv}$ that form an ep pair.
%%   \item A gradual computation type $\u B$ is a pair of type $[\u B]$
%%     and interpretations of $\dncast{\u B}{\dync}$ and $\upcast{U \u
%%       B}{U\u \dync}$ that form an ep pair.
%%   \item $A \ltdyn A'$ is modeled by an ep pair $\upcast{[A]}{[A']}$
%%     and $\dncast{\u F [A]}{\u F [A']}$ that factorizes the casts for
%%     $A, A'$.
%%   \end{enumerate}
%% \end{frame}

\begin{frame}{Implementing Two Dynamic Types}
  Can use CBPV as a metalanguage to define models of CBPV GTT.
  \pause
  \begin{mathpar}
    \dynv \cong (1+1) + U\dync + (\dynv \times \dynv)\\
    \dync \cong (\dynv \to \u F \dync)
  \end{mathpar}

  $\dynv$: S-expressions.\\

  $\dync$: supports call-by-value single argument functions as the
  only computation type, similar to ML.
\end{frame}

\begin{frame}{Implementing Two Dynamic Types}
  Can use CBPV as a metalanguage to define models of CBPV GTT.
  \begin{mathpar}
    \dynv \cong (1+1) + U\dync + (\dynv \times \dynv)\\
    \dync \cong (\dynv \to \dync) \with \u F \dynv
  \end{mathpar}

  $\dynv$: S-expressions.\\

  $\dync$: Supports Scheme's multi-argument and variable-arity
  functions.
\end{frame}

\section{Conclusion}

\begin{frame}{Summary}
  \begin{enumerate}
  \item Deconstructed gradual typing to basic axioms
  \item By axiomatizing term precision/dynamism, we can give casts a
    specification.
  \item Graduality + $\beta\eta$ = functor interpretation of casts, so
    all other cast semantics sacrifice one or the other.
  \item Polarized Languages make effectful equations as easy as
    non-effectful.
  \end{enumerate}
\end{frame}

\begin{frame}{Conclusion}
  \begin{itemize}
  \item Type theoretic approach justifies the ``most canonical''
    version of gradual typing. Can other semantics be similarly
    justified?
  \item Plays nicely with good type theories: what to gradualize next?
    Polarized session types?
  \item Papers: FSCD '18, ICFP'18, POPL'19
  \end{itemize}
  
  \pause
  \begin{mathpar}
    \inferrule
    {u : B \and A \ltdyn B}
    {\dncast A B u \ltdyn u : A \ltdyn B}

    \inferrule
    {\Phi \vdash t \ltdyn u : A \ltdyn B}
    {\Phi \vdash t \ltdyn \dncast A B u : A}\\

    \inferrule
    {t : A \and A \ltdyn B}
    {t \ltdyn \upcast A B t : A \ltdyn B}

    \inferrule
    {\Phi \vdash t \ltdyn u : A \ltdyn B}
    {\Phi \vdash \upcast A B t \ltdyn u : B}
  \end{mathpar}

\end{frame}
\end{document}

%% Local Variables:
%% compile-command: "pdflatex talk.tex"
%% End:
