[icfp] checkpoint: usage intro

This commit is contained in:
ben 2016-03-11 08:13:11 -05:00
parent c01e8da5a8
commit a19ca9df41
6 changed files with 97 additions and 6 deletions

View File

@ -6,7 +6,7 @@ compiled/paper_scrbl.zo: *.rkt *.scrbl
raco make -v $(PAPER).scrbl raco make -v $(PAPER).scrbl
paper.pdf: pkg compiled/paper_scrbl.zo texstyle.tex paper.pdf: pkg compiled/paper_scrbl.zo texstyle.tex
scribble ++style texstyle.tex --pdf $(PAPER).scrbl scribble ++extra fig-staging.tex ++style texstyle.tex --pdf $(PAPER).scrbl
paper.tex: pkg compiled/paper_scrbl.zo texstyle.tex paper.tex: pkg compiled/paper_scrbl.zo texstyle.tex
scribble ++style texstyle.tex --latex $(PAPER).scrbl scribble ++style texstyle.tex --latex $(PAPER).scrbl

View File

@ -136,5 +136,5 @@
(define (id x) (define (id x)
(make-element plain @format["~a" x])) (make-element plain @format["~a" x]))
(define (todo . x) (define (todo . x*)
(make-element 'bold (list x))) (make-element 'bold (cons "TODO:" x*)))

13
icfp-2016/fig-staging.tex Normal file
View File

@ -0,0 +1,13 @@
\begin{center}
\begin{tikzpicture}
\node (0) {$\bullet$};
\node (1) [right of=0,xshift=0.5cm]{$\bullet$};
\node (2) [right of=1,xshift=0.8cm] {$\bullet$};
\node (3) [right of=2,xshift=0.8cm] {$\bullet$};
\draw[->] (0) edge[bend left=50] node[above]{\emph{read}} (1);
\draw[<-] (0) edge[bend right=50] node[below]{\emph{expand}} (1);
\draw[->] (1) -- node[above]{\emph{typecheck}} (2);
\draw[->] (2) -- node[above]{\emph{compile}} (3);
\end{tikzpicture}
\end{center}

View File

@ -37,8 +37,8 @@
@include-section{intro.scrbl} @include-section{intro.scrbl}
@include-section{solution.scrbl} @include-section{solution.scrbl}
@;@include-section{usage.scrbl} @include-section{usage.scrbl}
@;@include-section{experience.scrbl} @; Merge with usage? @include-section{experience.scrbl} @; Merge with usage?
@;@include-section{implementation.scrbl} @;@include-section{implementation.scrbl}
@;@include-section{correctness.scrbl} @;@include-section{correctness.scrbl}
@;@include-section{related.scrbl} @;@include-section{related.scrbl}

View File

@ -5,6 +5,7 @@
\lstset{language=ML} \lstset{language=ML}
\usepackage[usenames,dvipsnames]{xcolor} \usepackage[usenames,dvipsnames]{xcolor}
\usepackage{multicol} \usepackage{multicol}
\usepackage{tikz}
% Override Scribble's default SecRef to numeric only % Override Scribble's default SecRef to numeric only
\renewcommand{\SecRef}[2]{~#1} \renewcommand{\SecRef}[2]{~#1}

View File

@ -1,6 +1,40 @@
#lang scribble/sigplan #lang scribble/sigplan
@require["common.rkt"]
@title{Usage} @title[#:tag "sec:usage"]{Real-World Metaprogramming}
We have defined useful letter-of-values transformations for a variety of
common programming tasks ranging from type-safe string formatting to
constant-folding of arithmetic.
These transformations are implemented in Typed Racket@~cite[TypedRacket],
which inherits Racket's powerful macro system@~cite[plt-tr1].
Our exposition does not assume any knowledge of Racket or Typed Racket, but
a key design choice of the Typed Racket language model bears mentioning:
evaluation of a Typed Racket program happens across three distinct stages,
shown in @Figure-ref{fig:staging}.
First the program is read and macro-expanded; as expanding a macro introduces
new code, the result is recursively read and expanded until no macros remain.
Next, the @emph{fully-expanded} Typed Racket program is type checked.
If checking succeeds, types are erased and the program is handed to the Racket
compiler.
For us, this means that we can implement @exact|{$\trans\ $}|
functions as macros referencing @exact|{$\interp\ $}| functions and rely
on the macro expander to invoke our transformations before the type checker runs.
@figure["fig:staging"
@list{Typed Racket language model}
@exact|{\input{fig-staging}}|
]
Though we describe each of the following transformations using in-line constant
values, our implementation applies @exact|{$\interp\ $}| functions to every
definition and let-binding in the program and then associates compile-time
data with the bound identifier.
When a defined value flows into a function like @racket[printf] without being
mutated along the way, we retrieve this cached information.
The macro system features used to implement this behavior are described in
@Secref{sec:implementation}.
@; regexp-match @; regexp-match
@; format @; format
@ -8,6 +42,41 @@
@; vectors @; vectors
@; arity @; arity
@section{Regexp}
Regular expression patterns are another common value whose structure is not
expressed by conventional type systems.
Consider the function @racket[regexp-match] from Typed Racket:
@interaction[
(regexp-match #rx"types" "types@ccs.neu.edu")
(regexp-match #rx"lambda" "types@ccs.neu.edu")
(regexp-match #rx"(.*)@(.*)" "types@ccs.neu.edu")
]
@; TODO note that nested groups cannot fail.
When called with a pattern @racket[p] and string @racket[s] to match with,
@racket[(regexp-match p s)] returns a list of all substrings in @racket[s]
matching groups in the pattern @racket[p].
The pattern itself counts for one group and parentheses within @racket[p]
delimit nested groups.
Hence the third example returns a list of three elements.
A match can also fail, in which case the value @racket[#f] is returned.
Although Typed Racket's @racket[regexp-match] has the type@note{Assuming that a
successful match implies that all nested groups successfully match.}
@racket[(Regexp String -> (U #f (Listof String)))], the number of strings
in the result list is determined by the number of groups in the input regular
expression.
Like the arity of a function or the size of a tuple, the number of groups
in a pattern is often clear to the programmer.
We could imagine using
an indexed family of @racket[regexp-match] functions for patterns of
two, three, or more groups.
Ideally though, the programming language should understand
these unconventional or domain-specific flavors of polymorphism.
@section{Database} @section{Database}
@; db @; db
@ -55,7 +124,15 @@ Calls to generic operations like @racket[query-row] are then specialized to
@; - no changes to underlying library / type system @; - no changes to underlying library / type system
@; - compile-time validation of query strings @; - compile-time validation of query strings
Incidentally, @racket[regexp-match:] is useful for parsing queries.
We also implemented @racket[query-row] to return a sized vector.
While light years away from LINQ, this technique provides at least basic While light years away from LINQ, this technique provides at least basic
safety guarantees for an existing library and demonstrates the generality of safety guarantees for an existing library and demonstrates the generality of
our technique. our technique.
@section{}
@; identifier macros
@; rename transformers