From 4fcd414971f74b18cd6a0dc71d166ad24909af0b Mon Sep 17 00:00:00 2001 From: ben Date: Tue, 15 Mar 2016 07:05:47 -0400 Subject: [PATCH] [icfp] checkpoint, usage just starting --- icfp-2016/Makefile | 2 +- icfp-2016/README.md | 9 +++- icfp-2016/intro.scrbl | 6 +-- icfp-2016/paper.scrbl | 2 +- icfp-2016/solution.scrbl | 2 - icfp-2016/texstyle.tex | 9 ++-- icfp-2016/usage.scrbl | 94 ++++++++++++++++------------------------ 7 files changed, 57 insertions(+), 67 deletions(-) diff --git a/icfp-2016/Makefile b/icfp-2016/Makefile index da3b672..230468d 100644 --- a/icfp-2016/Makefile +++ b/icfp-2016/Makefile @@ -6,7 +6,7 @@ compiled/paper_scrbl.zo: *.rkt *.scrbl raco make -v $(PAPER).scrbl paper.pdf: pkg compiled/paper_scrbl.zo texstyle.tex - scribble ++extra fig-experience.tex ++extra fig-stxclass.tex ++extra fig-stats.tex ++extra fig-staging.tex ++style texstyle.tex --pdf $(PAPER).scrbl + scribble ++extra fig-experience.tex ++extra fig-stxclass.tex ++extra fig-stats.tex ++style texstyle.tex --pdf $(PAPER).scrbl paper.tex: pkg compiled/paper_scrbl.zo texstyle.tex scribble ++style texstyle.tex --latex $(PAPER).scrbl diff --git a/icfp-2016/README.md b/icfp-2016/README.md index 463fb88..8dddf04 100644 --- a/icfp-2016/README.md +++ b/icfp-2016/README.md @@ -1,7 +1,14 @@ trivial @ icfp 2016, hopefully === -TODO +@parag{Eager Evaluation} + +Our implementation is available as a Racket package. +To install the library, download Racket and then run @racket[raco pkg install ???]. +The source code is on Github at: @url["https://github.com/???/???"]. + +Really, elaboration is the whole story. + "United States v. Hayes, 555 U.S. 415 (2009)") > (regexp-match #rx"(a*)b" "aab") '("aab" "aa") diff --git a/icfp-2016/intro.scrbl b/icfp-2016/intro.scrbl index 620ff51..40ca12a 100644 --- a/icfp-2016/intro.scrbl +++ b/icfp-2016/intro.scrbl @@ -102,11 +102,11 @@ The elaborator @emph{also} handles the common case where the regular expression ; Other code here -(define rxm regexp-match) +(define r-m regexp-match) (define (get-plaintiff (s : String)) : String (cond - [(rxm rx-case s) + [(r-m rx-case s) => cadr] [else "J. Doe"])) } @@ -126,5 +126,5 @@ Their illustrative examples were format strings, regular expressions, Relative to their pioneering work, we adapt Herman & Meunier's transformations to a typed language by inserting type annotations and boolean guards into the programs. -Our treatment of @racket[define] and @racket[let] forms is also new. +Our treatment of definition forms is also new. diff --git a/icfp-2016/paper.scrbl b/icfp-2016/paper.scrbl index eebb74b..860d742 100644 --- a/icfp-2016/paper.scrbl +++ b/icfp-2016/paper.scrbl @@ -23,7 +23,7 @@ analysis of an existing type system on existing code without changing the type system. We have implemented the technique as a Typed Racket library. - From the programmers' perspective, simply importing the library makes the type + From the programmers' viewpoint, simply importing the library makes the type system more perceptive---no annotations or new syntax required. } diff --git a/icfp-2016/solution.scrbl b/icfp-2016/solution.scrbl index ee0c4a0..31eb01c 100644 --- a/icfp-2016/solution.scrbl +++ b/icfp-2016/solution.scrbl @@ -6,8 +6,6 @@ @title[#:tag "sec:solution"]{Interpretations, Elaborations} -The main result of this pearl is defining a compelling set of - @emph{textualist elaborators}. A textualist elaborator (henceforth, @emph{elaborator}) is a specific kind of macro, meant to be run on the syntax of a program before the program is type-checked. diff --git a/icfp-2016/texstyle.tex b/icfp-2016/texstyle.tex index 0c9645d..420e116 100644 --- a/icfp-2016/texstyle.tex +++ b/icfp-2016/texstyle.tex @@ -31,9 +31,12 @@ \let\lrcorner\relax \usepackage{amssymb} -\newcommand{\interp}{\llbracket\emph{interp}\rrbracket} -\newcommand{\untyped}[1]{\lfloor #1 \rfloor} -\newcommand{\trans}{\llbracket\emph{transform}\rrbracket} +\newcommand{\interp}{\mathcal{I}} +\newcommand{\untyped}[1]{\hat{#1}} +\newcommand{\trans}{\mathcal{T}} +\newcommand{\elab}{\mathcal{E}} +\newcommand{\elabfe}[1]{\llbracket #1 \rrbracket} +\newcommand{\elabf}{\elabfe{\cdot}} \newcommand{\subt}{\mathbf{<:\,}} \newcommand{\tos}{\mathsf{types_of_spec}} \newcommand{\trt}[1]{\emph{#1}} diff --git a/icfp-2016/usage.scrbl b/icfp-2016/usage.scrbl index 4dd86b4..944add5 100644 --- a/icfp-2016/usage.scrbl +++ b/icfp-2016/usage.scrbl @@ -10,69 +10,52 @@ @; | > (f x) @; | y @; +------------ -@; TODO -- maybe a better title is "what can we learn from values"? @; TODO remove all refs to implementation? +@title[#:tag "sec:usage"]{What we can learn from Values} -@title[#:tag "sec:usage"]{Real-World Metaprogramming} -@;@(define base-eval -@; (make-evaluator 'racket/base -@; (sandbox-output 'string) -@; (sandbox-error-output 'string) -@; (error-display-handler (lambda (x y) (displayln "wepa"))))) - -We have defined useful letter-of-values transformations for a variety of +We have defined useful elaborators 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]. -For us, this means that Typed Racket comes equipped with powerful tools - for analyzing and transforming the syntax of programs before any type checking - occurs. - -@;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. -@;@; TODO stronger distinction between read/expand and typecheck -@;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 and rely on the macro expander to invoke our -@; transformations before the type checker runs. -@;The transformations can use @exact|{$\interp$}| functions as -@; needed to complete their analysis. -@; -@;@figure["fig:staging" -@; @list{Typed Racket language model} -@; @exact|{\input{fig-staging}}| -@;] - +These elaborators are implemented in Typed Racket@~cite[TypedRacket], a macro-extensible + typed language that compiles into Racket@~cite[plt-tr1]. +An important component of Typed Racket's design is that all macros in a program + are fully expanded before type-checking begins. +This convention lets us implement our elaborators as macros that expand into + typed code. @parag{Conventions} -Interpretation and transformation functions are defined over syntactic expressions - and values. -To make clear the difference between Typed Racket terms and syntactic representations +@itemlist[ + @item{ +Interpretation and elaboration functions are defined over symbolic expressions + and values; specifically, over @emph{syntax objects}. +To make clear the difference between Typed Racket terms and representations of terms, we quote the latter and typeset it in green. Using this notation, @racket[(λ (x) x)] is a term implementing the identity - function and @racket['(λ (x) x)] is a syntactic object that will evaluate + function and @racket['(λ (x) x)] is a representation that will evaluate to the identity function. Values are typeset in green because their syntax and term representations are identical. - +} @item{ In practice, syntax objects carry lexical information. -Such information is extremely important, but to simplify our presentation we - pretend it does not exist. -Think of this convention as removing the oyster shell to get a clear view of the pearl. - -Using infix @tt{:} for type annotations, for instance @racket[(x : Integer)]. -These are normally written as @racket[(ann x Integer)]. - -sql is short for postgresql - +Such information is extremely important, especially for implementing @racket[define] + and @racket[let] forms that respect @exact{$\alpha$}-equivalence, but + to simplify our presentation we omit it. +} @item{ +We use an infix @tt{:} to write explicit type annotations and casts, + for instance @racket[(x : Integer)]. +These are normally @racket[(ann x Integer)] and @racket[(cast x Integer)], + respectively. +} @item{ +In @Secref{sec:sql}, @tt{sql} is short for @tt{postgresql}, i.e. + the code we present in that section is only implemented for the @tt{postgresql} + interface. +} @item{ +Until @Secref{sec:def-overview}, we use @racket[define] and @racket[let] forms sparingly. +In fact, this practice aligns with our implementation---once the interpretations + and elaborations are defined, extending them to handle arbitrary definitions + and renamings is purely mechanical. +} +] @; ============================================================================= @section{String Formatting} @@ -80,10 +63,9 @@ sql is short for postgresql @; TODO add note about the ridiculous survey figure? Something like 4/5 doctors Format strings are the world's second most-loved domain-specific language (DSL). @; @~cite[wmpk-algol-1968] -At first glance, a format string is just a string; in particular, any string - used as the first argument in a call to @racket[printf]. -But between the quotation marks, format strings may contain @emph{format directives} - that tell @emph{where} and @emph{how} values can be spliced into the format string. +All strings are valid format strings; additionally, a format string may contain + @emph{format directives} describing @emph{where} and @emph{how} values can be + spliced into the format string. @; TODO scheme or common lisp? Racket follows the Lisp tradition@~cite[s-lisp-1990] of using a tilde character (@tt{~}) to prefix format directives. @@ -359,7 +341,7 @@ Each operation match the length of its arguments at compile-time and expand @; ============================================================================= -@section{Database Queries} +@section[#:tag "sec:sql"]{Database Queries} @; db @; TODO Ocaml, Haskell story @; TODO connect to ew-haskell-2012 os-icfp-2008