157 lines
5.1 KiB
TeX
157 lines
5.1 KiB
TeX
\begin{schemeregion}
|
|
|
|
Having described the basics of occurrence typing and the \lts
|
|
calculus, in this chapter we extend the calculus with paths into
|
|
compound data structures as well as complex logical propositions.
|
|
|
|
\section{Adding Paths}
|
|
\label{sec:paths}
|
|
|
|
The base \lts calculus deals with predicates applied to variables.
|
|
To accommodate compound data structures, however, the base system
|
|
is insufficient. For example, \scheme|(number? (car
|
|
x))| has only a trivial filter set in our base system,
|
|
because the object for \scheme|(car x)| cannot be a variable, so it
|
|
must be $\noeffect$. In this section, we extend the system to
|
|
overcome this limitation.
|
|
|
|
The key concept that allows us to typecheck this is the
|
|
\emph{path}.\footnote{The term is due to Cartwright et
|
|
al.~\citep{cartwright:paths} in distantly related work.}
|
|
A path is simply a sequence of data structure
|
|
selectors. For example, the expression \scheme|(cdr (cdr (car x)))|
|
|
follows the path $\pecdr,\pecdr,\pecar$ from \scheme|x|.
|
|
|
|
\subsection{Extending the Language}
|
|
|
|
\tiny
|
|
\begin{figure}
|
|
\PathSyntax
|
|
\caption{Grammar Extensions for Paths}
|
|
\label{fig:path}
|
|
\end{figure}
|
|
\normalsize
|
|
|
|
\begin{figure}
|
|
\deltaext
|
|
\caption{Operational Semantics for Pairs}
|
|
\label{fig:oppath}
|
|
\end{figure}
|
|
|
|
To model paths and data structure access in \lts, we extend the
|
|
language in several ways. Figures~\ref{fig:path} and
|
|
figure~\ref{fig:oppath} specifies the extended grammar and operation
|
|
semantics. The extensions to the expression grammar are minor: a
|
|
\scheme|(cons e e)| form is added, and a pair of values is itself a
|
|
value. The accessors are \scheme|car| and \scheme|cdr|, and there is
|
|
a predicate, \scheme|cons?|, for pairs. Similarly, a pair type is
|
|
added, written $\consty{-}{-}$. The operational semantics merely adds
|
|
additional evaluation contexts and $\delta$ rules.
|
|
|
|
The more significant changes concern filters and
|
|
objects. A filter with a path $\t{\pi(\x{})}$ means that the portion of \x{}
|
|
selected by path $\pi$ has type \t{}. Similarly, a latent filter
|
|
includes a path, so that the function
|
|
|
|
\begin{schemedisplay}
|
|
(lambda ([x : (Pair Any Any)]) (number? (car x)))
|
|
\end{schemedisplay}
|
|
|
|
\noindent
|
|
has the latent filter set $\num_{\pecar}|\comp{\num}_{\pecar}$.
|
|
|
|
Objects also include paths, which describe which portion of
|
|
the environment is accessed. Latent objects are merely paths, with
|
|
the singleton latent object $\bullet$ now representing the empty
|
|
path.
|
|
|
|
\subsection{Extending the Type Rules}
|
|
|
|
Adding paths to the system requires a change to all those parts of the
|
|
type system that manipulate filters and objects. In particular, the
|
|
{\sc T-Abs} and {\sc T-App} rules change to compute objects with paths.
|
|
For revised rules, see figure~\ref{fig:pathty}. We
|
|
also need new rules for typechecking the use of \scheme|cons|,
|
|
\scheme|car| and \scheme|cdr|, which are presented in
|
|
figure~\ref{fig:pairty}, along with the subtyping rule for pair types.
|
|
\footnote{With a polymorphic type
|
|
system, these could be simply treated as function applications by
|
|
the type system.}
|
|
|
|
\begin{figure}
|
|
\[
|
|
\absrule
|
|
\]
|
|
\[
|
|
\apprule
|
|
\]
|
|
\[
|
|
\subpairrule
|
|
\]
|
|
\caption{Modified Type Rules for Paths}
|
|
\label{fig:pathty}
|
|
\end{figure}
|
|
|
|
\begin{figure}
|
|
\pairRules
|
|
\caption{New Type Rules for Pairs}
|
|
\label{fig:pairty}
|
|
\end{figure}
|
|
|
|
The rule for \scheme|cons| is straightforward---it produces a pair
|
|
type, and, like all other non-\scheme|#f| values, pairs are always
|
|
true. {\sc T-Car} and {\sc T-Cdr} are
|
|
similar to {\sc T-App}. Note that the expression \scheme|(car x)| has
|
|
the filter set $\comp{\fft}_{\pecar(\x{})}|{\fft}_{\pecar(\x{})}$,
|
|
since if it evaluates to \scheme|#f|, the \scheme|car| field of
|
|
\scheme|x| must have type \fft.
|
|
|
|
\begin{figure*}
|
|
\FilterMeta
|
|
\hrule
|
|
\EnvPlusUpdate
|
|
\caption{New Metafunctions for Paths}
|
|
\label{fig:newmeta}
|
|
\end{figure*}
|
|
|
|
\paragraph{Metafunctions}
|
|
|
|
|
|
In addition to the new typing rules, several of the metafunctions must also
|
|
be revised:
|
|
|
|
\begin{itemize}
|
|
\item Paths in filters and latent filters are propagated in \absf and the environment update operation ($\G{} + \op{}$).
|
|
\item $\metafont{update}$ follows the path to update the relevant type.
|
|
\item \appf composes the path of the object and of the filter.
|
|
\end{itemize}
|
|
\noindent
|
|
The new definitions are in figure~\ref{fig:newmeta}.
|
|
|
|
|
|
\subsection{An Example}
|
|
|
|
We can now return to example~\ref{ex:numcar} from section~\ref{sec:informal} and
|
|
see how the extended type system typechecks it
|
|
correctly:
|
|
|
|
\begin{schemedisplay}
|
|
(if (number? (car p))
|
|
(add1 (car p))
|
|
7)
|
|
\end{schemedisplay}
|
|
\noindent
|
|
We begin with the type environment $\Gamma = p :
|
|
\consty{\top}{\top}$. Considering the test expression first, the
|
|
expression \scheme|p| has object $p$. Thus \scheme|(car p)| has the
|
|
object $\pecar(p)$ and type $\top$. When combined with the latent
|
|
filter set of \scheme|number?|, this results in the filter set
|
|
$\num_{\pecar(p)}|\comp{\num}_{\pecar(p)}$ for the test expression.
|
|
|
|
The type environment for the \tbranch is therefore $\Gamma +
|
|
\num_{\pecar(p)}$, which is $p : \metafont{update}(\consty{\top}{\top},
|
|
\num_{\pecar})$. This gives us the desired environment $p :
|
|
\consty{\num}{\top}$ to bless the \tbranch.
|
|
|
|
\end{schemeregion}
|