117 lines
4.1 KiB
TeX
117 lines
4.1 KiB
TeX
\documentclass{article}
|
|
\usepackage{amsmath}
|
|
\usepackage{mathpartir}
|
|
\usepackage{palatino}
|
|
\begin{document}
|
|
\begin{abstract}
|
|
The transformative \emph{and} analytic power of macros can turn
|
|
a polymorphic type system into a dependent type system, at least
|
|
for common programming tasks.
|
|
By analyzing program syntax and propogating known information about program
|
|
\emph{values} at compile-time, we can express many of the practical
|
|
motivations for dependent types without requiring programmer annotations
|
|
or changes to the underlying type system.
|
|
|
|
Our macro-expanded types are not proving new theorems,
|
|
but they recognize facts obvious to the programmer and hopefully
|
|
give a nice experience.
|
|
\end{abstract}
|
|
|
|
Technique works by identifying common properties of a set of
|
|
values and using these properties in a macro transformation.
|
|
|
|
\subsubsection*{Key Functions}
|
|
\begin{itemize}
|
|
\item Context-free, syntactic way of associating a Curry-style ``type'' to a value.
|
|
\subitem $\mathsf{typeof} : Syntax \rightarrow TypeTag$
|
|
\item (Optional) Propogate metadata to future references of an identifier
|
|
\subitem $\mathsf{attach} : Syntax \times Meta \rightarrow Syntax$
|
|
\item Tag-indexed family of functions that extract data from a syntactic value.
|
|
\subitem $\mathsf{analyze} : TypeTag \rightarrow (Syntax \rightarrow Meta$
|
|
\item Transform a context based on metadata-augmented syntax for the hole.
|
|
\subitem $\mathsf{transform : (-> Context (Syntax x Meta) Syntax$
|
|
\end{itemize}
|
|
|
|
\subsubsection*{Correctness}
|
|
|
|
Suppose {\tt transform} $E~e = e'$.
|
|
A correct transformation should only catch bugs in $e$.
|
|
|
|
% Is this novel at all?
|
|
\begin{mathpar}
|
|
\inferrule*{
|
|
\vdash e : \tau
|
|
\\
|
|
\vdash e' : \tau'
|
|
}{
|
|
\tau' <: \tau
|
|
\\
|
|
e \Uparrow \iff e' \Uparrow
|
|
\\
|
|
e \Downarrow v \iff e' \Downarrow v
|
|
}
|
|
|
|
\inferrule*{
|
|
\vdash e : \tau
|
|
\\
|
|
\not\vdash e' : \tau'
|
|
}{
|
|
e \Uparrow
|
|
}
|
|
|
|
\inferrule*{
|
|
\not\vdash e : \tau
|
|
}{
|
|
\not\vdash e' : \tau'
|
|
}
|
|
\end{mathpar}
|
|
|
|
|
|
\subsubsection*{Examples}
|
|
|
|
Table defines type tags and related \texttt{transformations}.
|
|
|
|
\vspace{0.4cm}
|
|
\begin{center}
|
|
\hspace{-3cm}\begin{tabular}{l l l l l}
|
|
Type & Syntax Category & Metadata & Applications \\\hline\hline
|
|
\\Format String & {\tt string} & \#/$\tau$ of fmt chars & Check args to {\tt printf}
|
|
\\Regexp & {\tt string} / {\tt bytes} & \# groups & Check paren-matching${}^*$, smarter return type
|
|
\\Query String & {\tt string} & \# of {\tt \$} vars & Check arity
|
|
\\Function & {\tt (lambda ...)} & Arity & Compile-time arity check for {\tt apply}
|
|
\\Numbers & {\tt number} & Value & Constant folding, accurate types
|
|
\\Vectors & {\tt `\#( ... )} & Length & Access, size, fast operations
|
|
\end{tabular}
|
|
\end{center}
|
|
|
|
|
|
\subsubsection*{Caveats / Extras}
|
|
\begin{itemize}
|
|
\item Regular expressions should work with partial groups and warn about unvalidated user input.
|
|
\subitem i.e. \texttt{\#rx"prefix (" $+$ \#rx"mid" $+$ \#rx") suffix"} should work
|
|
\item {Will hijack \texttt{define} to get procedure arity}
|
|
\item {Add smarter runtime assertions, like \texttt{assert-length} and a remembering \texttt{index?}}
|
|
\item Typeclass / Darais-class operations?
|
|
\subitem $\circ~$ Define a {\tt TypeTag}, extend \texttt{typeof}
|
|
\subitem $\circ~$ Write macro that looks for \& uses tags {\tt equal?}
|
|
\end{itemize}
|
|
|
|
~
|
|
\\P.S. Our goal is not to discourage dependent types, but rather to advertise macros.
|
|
\\P.P.S. Jack Firth might be using the library. Email him?
|
|
\\P.P.P.S Should work in other languages, hard part will be rename transformers
|
|
|
|
|
|
\subsubsection*{Outline}
|
|
\begin{itemize}
|
|
\item Examples of ``syntactically obvious'' dependent types.
|
|
\item Not-so-obvious examples, i.e. regular expressions \& vector operations.
|
|
\item High-level solution
|
|
\item Racket implementation, brief correctness argument
|
|
\subitem (Cool things like {\tt set!-transformer})
|
|
\item Limitations \& near misses
|
|
\item Experience report?
|
|
\end{itemize}
|
|
|
|
\end{document}
|