Skip to content
Snippets Groups Projects
Commit 9fb1e45d authored by Max New's avatar Max New
Browse files

the dynamic type is Scheme!

parent cef6c9ca
Branches
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 101 additions and 18 deletions
paper/gtt.tex
+ 101
− 18
View file @ 9fb1e45d
...@@ -191,7 +191,7 @@ ...@@ -191,7 +191,7 @@
\newcommand{\thunk}{\kw{thunk}} \newcommand{\thunk}{\kw{thunk}}
\newcommand{\force}{\kw{force}} \newcommand{\force}{\kw{force}}
\newcommand{\abort}{\kw {abort}} \newcommand{\abort}{\kw {abort}}
\newcommand{\with}{\mathop{\&}} \newcommand{\with}{\mathbin{\&}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document} \begin{document}
...@@ -767,16 +767,11 @@ translation, but we leave this to future work. ...@@ -767,16 +767,11 @@ translation, but we leave this to future work.
In particular the aim of this section is to establish the following In particular the aim of this section is to establish the following
theorems: theorems:
\begin{theorem}{Consistency of GTT} \begin{theorem}{Graduality}
There exists a judgment $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn
M_2 : B_1 \ltdyn B_2$ that is not provable.
\end{theorem}
\begin{theorem}{Contextual Approximation}
If $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn M_2 : B_1 \ltdyn If $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn M_2 : B_1 \ltdyn
B_2$, then for any context $C : (\Gamma_1 \vdash B_1) \Rightarrow B_2$, then for any GTT context $C : (\Gamma_1 \vdash B_1)
(\cdot \vdash \u F 2)$, and any valid interpretation of the dynamic \Rightarrow (\cdot \vdash \u F 2)$, and any valid interpretation of
types, one of the following holds the dynamic types, one of the following holds
\begin{enumerate} \begin{enumerate}
\item $\sem{C[M_1]} \Downarrow \err$ \item $\sem{C[M_1]} \Downarrow \err$
\item $\sem{C[M_1]}, \sem{C[\dncast{B_1}{B_2}M_2[\upcast{\Gamma_1}{\Gamma_2}{\Gamma_1}]]} \Uparrow$ \item $\sem{C[M_1]}, \sem{C[\dncast{B_1}{B_2}M_2[\upcast{\Gamma_1}{\Gamma_2}{\Gamma_1}]]} \Uparrow$
...@@ -786,6 +781,17 @@ theorems: ...@@ -786,6 +781,17 @@ theorems:
\end{enumerate} \end{enumerate}
\end{theorem} \end{theorem}
As a consequence we get the consistency of the type theory:
\begin{corollary}{Consistency of GTT}
There exists a judgment $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn
M_2 : B_1 \ltdyn B_2$ that is not provable.
\end{corollary}
\begin{proof}
$\ret \tru \ltdyn \ret \fls$ is not provable since they are
distinguished by the empty context.
\end{proof}
As described in the previous section, almost all of the contract As described in the previous section, almost all of the contract
translation is uniquely determined already: casts between function translation is uniquely determined already: casts between function
types must wrap inputs and outputs, pairs cast each component, etc. types must wrap inputs and outputs, pairs cast each component, etc.
...@@ -930,13 +936,75 @@ on the other tags. ...@@ -930,13 +936,75 @@ on the other tags.
We We
\end{proof} \end{proof}
The inclusion of sums, and negative products as tags on the dynamic The inclusion of sums, and negative products as primitives is uncommon
type is uncommon in dynamically typed languages. in dynamically typed languages.
%
Instead, sums are usually encoded using a kind of fresh atomic values
to distinguish between different constructors, i.e. using
\emph{nominal} features.
%
Treating this fresh generation of values is out of scope for this
current paper.
However, a sum injection $\sigma_{1} V$ can also be encoded using
a pair of a boolean and the value $V$: $(1, V)$.
%
This is for example used in minimalist dialects of Scheme and Lisp,
where rather than a boolean value, a \emph{symbol} that has an
informative name is used.
%
The next interpretation we present is based on this idea.
%
The dynamic value type is the type of binary trees whose leaves are
booleans or (opaque) closures, which we can think of as a basic type
of S-expressions.
%
We define this in the standard way as a recursive type $\mu X. (1 + 1)
+ U\dync + (X \times X)$.
The dynamic computation type looks a bit strange at first: it is
defined as a lazy pair of a function $\dynv \to \dync$ and a returner
$\u F \dynv$.
%
However, consider its infinite unfolding:
\[ (\u F \dynv) \with (\dynv \to \u F \dynv) \with (\dynv \to \dynv \to \u F \dynv) \with \cdots \]
%
Taking the session-typing view that a lazy product is a selection of
options for a consumer, this says that the consumer can \emph{call}
the function with any number of arguments pushed onto the stack.
% %
Instead, sums can be encoded using a pair of some atomic enumeration We observe that this is isomorphic to the more common type: $\dynv^*
type and the payload. \to \u F \dynv$ where $A^* = \mu X. 1 + (A \times X)$ is the type of
finite lists, which we can prove as follows:
\begin{align*}
&(\u F \dynv) \with (\dynv \to \u F \dynv) \with (\dynv \to \dynv \to \u F \dynv) \with \cdots\\
&\cong (1 \to \u F \dynv) \with (\dynv \times 1 \to \u F \dynv) \with (\dynv \times (\dynv \times 1) \to \u F \dynv) \with \cdots\\
&\cong (1 + (\dynv \times 1) + (\dynv \times \dynv \times 1) + \cdots) \to \u F \dynv\\
&\cong (\mu X. 1 + (\dynv \times X)) \to \u F \dynv\\
&= \dynv^* \to \u F \dynv
\end{align*}
%
However, operationally, our definition as a recursive computation type
is more true to the implementation of Scheme-like languages, where
multi-argument function application simply pushes all of the arguments
onto the stack.
%
The type $\dynv^* \to \u F \dynv$ on the other hand corresponds to an
implementation that constructs a cons-list and then passes it as a
single argument on the stack.
%
The introduction form of this language corresponds to something very
much like Scheme's ``case-lambda'' operator for defining
multi-argument functions.
Thinking of $\with$ as a kind of constructor for objects, we can think
of a term of type $\dync$ as representing an object with one method
for every natural number that takes that many S-expressions and
returns an S-expression.
% %
The next interpreation we present is based on this idea. In other words, this interpretation of $\dync$ says that all
computations in GTT can be implemented as \emph{variable-arity
multi-argument functions}, another
% %
We use booleans as the atomic enumeration for simplicity, but we could We use booleans as the atomic enumeration for simplicity, but we could
of course use some larger type of machine integers in an of course use some larger type of machine integers in an
...@@ -951,10 +1019,10 @@ pairs are interpreted as a sigma type and functions as a pi type. ...@@ -951,10 +1019,10 @@ pairs are interpreted as a sigma type and functions as a pi type.
In addition, we can drop the $1$ case by interpreting it as one of the In addition, we can drop the $1$ case by interpreting it as one of the
booleans. booleans.
\begin{definition}[Sums-as-pairs Dynamic Type Interpretation] \begin{definition}[Scheme-like Dynamic Type Interpretation]
The following defines a dynamic type interpretation. The following defines a dynamic type interpretation.
\begin{align*} \begin{align*}
\rho(\dynv) &= (1 + 1) + (\rho(\dynv) \times \rho(\dynv)) + U\rho(\dync) \\ \rho(\dynv) &= (1 + 1) + U\rho(\dync) + (\rho(\dynv) \times \rho(\dynv)) \\
\rho(\dync) &= (\rho(\dynv) \to \rho(\dync)) \with \u F \rho(\dynv) \rho(\dync) &= (\rho(\dynv) \to \rho(\dync)) \with \u F \rho(\dynv)
\end{align*} \end{align*}
and define for each $G$, and define for each $G$,
...@@ -1350,6 +1418,8 @@ Next, we give the inequational theory for our CBPV language. ...@@ -1350,6 +1418,8 @@ Next, we give the inequational theory for our CBPV language.
\subsection{Graduality Logical Relation} \subsection{Graduality Logical Relation}
\begin{figure} \begin{figure}
\begin{mathpar} \begin{mathpar}
{\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\ {\logty{i}{A}} \subseteq \{ \cdot \vdash V : A \}^2 \quad\qquad{\logty{i}{\u B}}\subseteq \{ \cdot \pipe \u B \vdash S : \u F (1 + 1) \}^2\quad\qquad {\logc{i}} \subseteq \{ \cdot \vdash M : \u F (1 + 1) \}^2\\
...@@ -1395,6 +1465,7 @@ Next, we give the inequational theory for our CBPV language. ...@@ -1395,6 +1465,7 @@ Next, we give the inequational theory for our CBPV language.
\ipole \omega M_3$ then $M_1 \ipole i M_3$. \ipole \omega M_3$ then $M_1 \ipole i M_3$.
% TODO: might as well make error the least element? not sure % TODO: might as well make error the least element? not sure
\item Error awareness: For all $i \in \nats$, $\err \ipole i \err$. \item Error awareness: For all $i \in \nats$, $\err \ipole i \err$.
\end{enumerate} \end{enumerate}
\end{definition} \end{definition}
...@@ -1839,7 +1910,11 @@ with errors, in order to efficiently arrive at a concrete operational ...@@ -1839,7 +1910,11 @@ with errors, in order to efficiently arrive at a concrete operational
interpretation. interpretation.
% %
It may be of interest to develop a more general notion of model of GTT It may be of interest to develop a more general notion of model of GTT
for which we can prove soundness and completeness theorems. for which we can prove soundness and completeness theorems, as in
\cite{cbn-gtt}.
%
% %
Furthermore, the ordered CBPV with errors should also have a sound and Furthermore, the ordered CBPV with errors should also have a sound and
complete notion of model, and so our contract translation should have complete notion of model, and so our contract translation should have
...@@ -1880,6 +1955,14 @@ This gives some evidence that the specific choice of connectives of ...@@ -1880,6 +1955,14 @@ This gives some evidence that the specific choice of connectives of
CBPV occupies a certain ``sweet spot'' between semantic expressivity CBPV occupies a certain ``sweet spot'' between semantic expressivity
and amenability to extensions. and amenability to extensions.
\paragraph{Dynamically Typed Call-by-push-value}
Our interpretation of the dynamic types in CBPV suggests a design for
a Scheme-like language with a value and computation distinction.
%
This may be of interest for designing an extension of Type Racket that
efficiently supports CBN or a scheme-like language with codata types.
\appendix \appendix
In this appendix we present for the reader who is unfamiliar with In this appendix we present for the reader who is unfamiliar with
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment