From 257556f0330c8bf02813db452f05f9f0819c9167 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Wed, 8 Jan 2020 11:45:04 -0500
Subject: [PATCH] cbv syntax, op semantics, translation
---
jfp-paper/defs.tex | 7 ++-
jfp-paper/jfp-gtt.tex | 141 +++++++++++++++++++++++++++++++++++++++++-
2 files changed, 143 insertions(+), 5 deletions(-)
diff --git a/jfp-paper/defs.tex b/jfp-paper/defs.tex
index 6f1ee2d..ab761f1 100644
--- a/jfp-paper/defs.tex
+++ b/jfp-paper/defs.tex
@@ -24,7 +24,7 @@
\newcommand{\cbpv}{CBPV}
\newcommand{\cbpvstar}{CBPV*}
\newcommand{\cbpvtxt}{\cbpv}
-\newcommand{\sem}[1]{[[#1]]}
+\newcommand{\sem}[1]{\llbracket{#1}\rrbracket}
\newcommand{\sdncast}[2]{\sem{\dncast{#1}{#2}}}
\newcommand{\supcast}[2]{\sem{\upcast{#1}{#2}}}
\newcommand{\srho}[1]{\sem{#1}_\rho}
@@ -159,8 +159,9 @@
\newcommand\errordivergeright[0]{\ltdyn\succeq}
\newcommand\errordivergerightop[0]{\preceq\gtdyn}
-\newcommand\bvtopv[1]{#1^{c}}
-\newcommand\bvtopvpure[1]{#1^{v}}
+\newcommand\cbvtocbpvcomp[1]{#1^{c}}
+\newcommand\cbvtocbpvval[1]{#1^{v}}
+\newcommand\cbvtocbpvty[1]{#1^{ty}}
\newcommand\purely{\downarrow}
%% Local Variables:
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index 62a0a78..b6826a7 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -4,8 +4,8 @@
\newif\ifshort
\newif\iflong
%% Pick long or short version:
-%% \shorttrue
-\longtrue
+\shorttrue
+%% \longtrue
\usepackage{amssymb}
%% \usepackage{amsthm}
@@ -3939,6 +3939,143 @@ Theorem~\ref{thm:monadic-comonadic-casts} gives the result.
%% In order for this duality to be \emph{perfect}, we use the version of
%% casts that are \emph{not} assumed to be
+\section{Application: Deriving Call-by-value Operational Semantics}
+
+To show how GTT can be used to inform language design, we show how the
+uniqueness principles of Theorem~\ref{thm:casts-unique} justify most
+of the operational behavior of a standard Call-by-value cast calculus.
+
+\begin{figure}
+ \begin{mathpar}
+ \begin{array}{lrcl}
+ \mbox{Types} & A & \bnfdef &
+ {\dyn} \alt {A \to A} \alt {1}\alt {A \times A}\alt 0 \alt {A + A}\\
+ \mbox{Tags} & G & \bnfdef & \dyn \to \dyn \alt 1 \alt \dyn \times \dyn \alt 0 \alt \dyn + \dyn\\
+ \mbox{Terms} & M,N & \bnfdef &
+ \err \alt x \alt
+ \obcast{A}{A}M\alt
+ () \alt \pmpairWtoinZ M N\alt
+ (M,N) \alt \pmpairWtoXYinZ M x y N\\
+ & & \alt &
+ \inl M\alt \inr M\alt
+ \caseofXthenYelseZ M {x_1. N_1}{x_2. N_2} \alt
+ \lambda x:A. M \alt M\,N\\
+
+ \mbox{Values} & V & \bnfdef &
+ \obcast G \dyn V \alt \lambda x:A. M \alt () \alt (V,V) \alt \inl V \alt \inr V \\
+ \mbox{Evaluation Contexts} & S & \bnfdef &
+ \bullet \alt \obcast B A S\alt
+ (S,N)\alt (M, S) \alt \pmpairWtoXYinZ S x y N\\
+ &&\alt&
+ \inl S \alt \inr S \alt \caseofXthenYelseZ S {x_1.N_1}{x_2.N_2}\alt
+ S\,N\alt V\,S\\
+ \mbox{Environments} & \Gamma & \bnfdef & \cdot \alt \Gamma,x:A\\
+ \mbox{Substitutions} & \gamma & \bnfdef & \cdot \alt \gamma, V/x
+ \end{array}
+ \end{mathpar}
+ \caption{CBV Cast Calculus}
+\end{figure}
+
+\begin{figure}
+ \begin{mathpar}
+ E[\letXbeYinZ V x N] \step E[N[V/x]]\and
+ E[(\lambda x:A. M)\,V] \step E[M[V/x]]\and
+ E[\pmpairWtoinZ V N] \step E[N]\and
+ E[\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{x_2} N] \step E[N[V_1/x_1][V_2/x_2]]\and
+ E[\caseofXthenYelseZ {\inl V}{x_1. N_1}{x_2. N_2}] \step E[N_1[V/x_1]]\and
+ E[\caseofXthenYelseZ {\inr V}{x_1. N_1}{x_2. N_2}] \step E[N_2[V/x_2]]\\\\
+ \inferrule
+ {}
+ {\obcast{\dyn}{\dyn}V \step E[V]}\and
+ \inferrule
+ {A \ltdyn G}
+ {E[\obcast \dyn A V] \step E[\obcast{\dyn}{G}\obcast{G}{A}V]}\and
+ \inferrule
+ {A \ltdyn G}
+ {E[\obcast A \dyn V] \step E[\obcast A G \obcast G \dyn V]}\and
+ \inferrule
+ {}
+ {E[\obcast G \dyn \obcast \dyn G V] \step E[V]}\and
+ \inferrule
+ {G \neq G'}
+ {E[\obcast {G'} \dyn \obcast \dyn {G} ]}\and
+ \inferrule
+ {A \ltdyn G_A \and B \ltdyn G_B \and G_A \neq G_B}
+ {E[\obcast B A V] \step \err}\and
+ \inferrule
+ {}
+ {E[\obcast{A_1' \to A_2'}{A_1 \to A_2}V]\step
+ E[\lambda x:A_1'. \obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}x))]}\and
+ \inferrule
+ {}
+ {E[\obcast 1 1 ()] \step E[()]}\and
+ \inferrule
+ {}
+ {E[\obcast{A_1' \times A_2'}{A_1 \times A_2}(V_1,V_2)] \step
+ E[(\obcast{A_1'}{A_1}V_1,\obcast{A_2'}{A_2}V_2)]}\and
+ \inferrule
+ {}
+ {E[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inl V)}]\step
+ E[\obcast{A_1'}{A_1}V]}\and
+ \inferrule
+ {}
+ {E[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inr V)}]\step
+ E[\obcast{A_2'}{A_2}V]}
+ \end{mathpar}
+ \caption{CBV Cast Calculus Operational Semantics}
+\end{figure}
+
+\begin{figure}
+ \begin{align*} % ?, ->, 1, *, 0, +
+ \cbvtocbpvty{\dyn} &= \dyn\\
+ \cbvtocbpvty{(A \to A')} &= \cbvtocbpvty{A} \to \cbvtocbpvty{A'}\\
+ \cbvtocbpvty{1} &= 1\\
+ \cbvtocbpvty{(A_1 \times A_2)} &= \cbvtocbpvty{A_1} \times \cbvtocbpvty{A_2}\\
+ \cbvtocbpvty{0} &= 0\\
+ \cbvtocbpvty{(A_1 + A_2)} &= \cbvtocbpvty{A_1} + \cbvtocbpvty{A_2}\\\\
+ \cbvtocbpvcomp{x} &= \ret x\\
+ \cbvtocbpvcomp{(\letXbeYinZ M x N)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp{M}} x {\cbvtocbpvcomp{N}}\\
+ \cbvtocbpvcomp{(\obcast{A_2}{A_1}M)} &=
+ \bindXtoYinZ M x
+ \dncast{F \cbvtocbpvty{A_2}}{F \dyn}{(\ret {\upcast{\cbvtocbpvty{A_1}}{\dyn}x})}\\
+ \cbvtocbpvcomp{(\lambda x:A. M)} &=
+ \ret (\thunk {(\lambda x:\cbvtocbpvty{A}. \cbvtocbpvcomp{M})})\\
+ \cbvtocbpvcomp{(M\,N)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp M} f
+ \bindXtoYinZ {\cbvtocbpvcomp N} x
+ \force f\,x\\
+ \cbvtocbpvcomp{()} &= \ret ()\\
+ \cbvtocbpvcomp{(\pmpairWtoinZ M N)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp M} z \pmpairWtoinZ z N\\
+ \cbvtocbpvcomp{(M_1,M_2)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp {M_1}} {x_1}
+ \bindXtoYinZ {\cbvtocbpvcomp {M_2}} {x_2}
+ \ret (x_1,x_2)\\
+ \cbvtocbpvcomp{(\pmpairWtoXYinZ M x y N)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp M} z
+ \pmpairWtoXYinZ z x y {\cbvtocbpvcomp N}\\
+ \cbvtocbpvcomp{(\abort M)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp M} z {\abort z}\\
+ \cbvtocbpvcomp{(\inl M)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp{M}} x \ret \inl x\\
+ \cbvtocbpvcomp{(\inr M)} &=
+ \bindXtoYinZ {\cbvtocbpvcomp{M}} x \ret \inr x\\
+ \cbvtocbpvcomp{(\caseofXthenYelseZ M {x_1. N_1}{x_2. N_2})} &=
+ \bindXtoYinZ {\cbvtocbpvcomp M} z
+ \caseofXthenYelseZ z {x_1. \cbvtocbpvcomp {N_1}}{x_2. \cbvtocbpvcomp {N_2}}\\\\
+ \cbvtocbpvval{(\obcast{\dyn}{G}V)} &= \upcast{\cbvtocbpvty{G}}{\dyn}V\\
+ \cbvtocbpvval{(\lambda x:A. M)} &=
+ \thunk {(\lambda x:\cbvtocbpvty{A}. \cbvtocbpvcomp{M})}\\
+ \cbvtocbpvval{()} &= ()\\
+ \cbvtocbpvval{(V_1,V_2)} &= (\cbvtocbpvval {V_1}, \cbvtocbpvval {V_2})\\
+ \cbvtocbpvval{(\inl V)} &= \inl \cbvtocbpvval V \\
+ \cbvtocbpvval{(\inr V)} &= \inr \cbvtocbpvval V \\
+ \end{align*}
+ \caption{CBV to GTT translation}
+\end{figure}
+
+
\section{Contract Models of GTT}
\label{sec:contract}
--
GitLab