diff --git a/icfp-2016/.gitignore b/icfp-2016/.gitignore index 5fa8838..caf533d 100644 --- a/icfp-2016/.gitignore +++ b/icfp-2016/.gitignore @@ -5,3 +5,4 @@ *.log *.out *.pdf +paper.tex diff --git a/icfp-2016/outline.scrbl b/icfp-2016/outline.scrbl index 624fd4e..4004c4b 100644 --- a/icfp-2016/outline.scrbl +++ b/icfp-2016/outline.scrbl @@ -1,5 +1,115 @@ -#lang scribble/sigplan +#lang scribble/manual + +@(require "common.rkt") @title{Outline} @; Applications +(Our goal is not to discourage dependent types, but rather to advertise macros.) +(Jack Firth might be using the library. Email him?) + +Each application is works by identifying common properties of a set of + values and using these properties in a macro transformation. + +@itemlist[ + @item{@tt{typeof : (-> Syntax TypeTag)}} + @item{@tt{transformations : (-> TypeTag (Set (-> Syntax Syntax))}} +] + +The following table defines type tags and related @tt{transformations}. + +@exact|{ +\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 & Type for {\tt apply} +\\Numbers & {\tt number} & Value & Constant folding, accurate types +\\Vectors & {\tt '\#( ... )} & Length & Access, size, fast operations +\end{tabular} +}| + +Caveats / Extras: +@itemlist[ + @item{Regular expressions should work with partial groups and warn about unvalidated user input. + i.e. @tt{#rx"prefix (" + #rx"mid" + #rx") suffix"} should work} + @item{Will hijack @tt{define} to get procedure arity} + @item{Add smarter runtime assertions, like @tt{assert-length} and a remembering @tt{index?}} +] + + +@;@section{String DSLs} +@;Predicate is @tt{string?}. +@; +@;@subsection{format} +@;Format strings contain format characters. +@;Type tag is @tt{string:format}. +@;Transformations are @tt{format} and @tt{printf}. +@; +@;Analysis parses format characters and determines the number & type +@; of remaining arguments. +@; +@;@;@exact|{$\Pi (x:String) . FormatType(x) \rightarrow String$}| +@; +@; +@;@subsection{regexp-match} +@;Regular expressions have primitive syntax, but any string or byte string +@; is also a valid regular expression. +@;Type tag is @tt{string:regexp} +@;Transformation is @tt{regexp-match}. +@; +@;Analysis parses groups. +@;Looks for matched parentheses and counts the number of groups. +@; +@; +@;@subsection{database} +@;Query strings recognized by the @racket[db] library. +@;Type tag is @tt{string:query}. +@;The dollar sign (@tt{$}) is for DB variables. +@;Transformations are query functions. +@; +@;Analysis matches arguments with number of DB variables. +@; +@;TODO: database connection needs to carry row information +@; +@; +@;@section{arithmetic} +@;In Typed Racket, @tt{0} has type @tt{Zero} but @tt{(- 5 5)} has type @tt{Integer}. +@;We fix this. +@; +@;Type tag is @tt{number}. +@;Predicate is @tt{number?} +@;Transformations are basic arithmetic @tt{+ - * /}. +@; +@;Analysis folds constants, so @tt{(- 5 5)} is @tt{0} at runtime. +@; +@;TODO: attach actual values to variables, remember that i.e. @tt{5} can +@; be @tt{sub1}'d 5 times before changing type to @tt{Integer}. +@;Can we do the same for @tt{Index} and @tt{add1}? +@; +@; +@;@section{map} +@;For variable-arity polymorphism. +@; +@;Type tag is @tt{procedure}. +@;Predicate is @tt{procedure?} +@;Transformations are functions like @tt{map} and @tt{apply}. +@; +@;Analysis matches known arities with given argument counts. +@; +@;Not sure how this improves over polydots, except for @tt{apply}. +@; +@; +@;@section{sized vectors} +@; +@;Track length of vectors. +@;Type tag is @tt{vector}. +@;Predicate is @tt{vector?}. +@; +@;Analysis: +@;@itemlist[ +@; @item{Faster versions of code} +@; @item{Propogate length through functions like append} +@; @item{Catch index out-of-bounds} +@;] diff --git a/icfp-2016/paper.scrbl b/icfp-2016/paper.scrbl index 1db6f6f..b672848 100644 --- a/icfp-2016/paper.scrbl +++ b/icfp-2016/paper.scrbl @@ -1,4 +1,5 @@ -#lang scribble/sigplan @onecolumn +#lang scribble/manual +@;#lang scribble/sigplan @onecolumn @(require "common.rkt") @@ -9,13 +10,25 @@ @title{Functional Pearl: Do we @emph{really} need Dependent Types?} @; Trivial differences, little things that count @; Recall 'fexprs are trivial'? +@; Syntactically dependent types @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 programming experience. + } -@category["D.3.3" "Programming Languages" "Language Constructs and Features"] -@terms{Performance, Experimentation, Measurement} +@;@category["D.3.3" "Programming Languages" "Language Constructs and Features"] +@;@terms{Performance, Experimentation, Measurement} @;@keywords{Gradual typing, performance evaluation} @include-section{outline.scrbl} diff --git a/icfp-2016/teaser.tex b/icfp-2016/teaser.tex new file mode 100644 index 0000000..83a6b3e --- /dev/null +++ b/icfp-2016/teaser.tex @@ -0,0 +1,55 @@ +\documentclass{article} +\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} + +\subsection*{Outline} + +Technique works by identifying common properties of a set of + values and using these properties in a macro transformation. + +\begin{itemize} + \item {\texttt{typeof : (-> Syntax TypeTag)}} + \item {\texttt{transformations : (-> TypeTag (Set (-> Syntax Syntax))}} +\end{itemize} + +Table defines type tags and related \texttt{transformations}. + +\vspace{0.4cm} +\begin{center} +\hspace{-3.5cm}\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 & Type 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?}} +\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? + +\end{document}