[icfp] specifying translations and correctness

icfp-2016/bib.rkt

@@ -35,6 +35,7 @@
 (define/short sigplan-notices "SIGPLAN Notices" (string-append ACM "SIGPLAN Notices"))
 (define/short scheme-workshop "SFP" (string-append "Scheme and Functional Programming Workshop"))
 (define/short jfp "JFP" (string-append Journal "Functional Programming"))
+(define/short jsl "JSL" (string-append Journal "of Symbolic Logic"))
 (define/short hosc "HOSC" "Higher-Order and Symbolic Programming")
 (define/short lfp "LFP" "LISP and Functional Programming")
 (define/short lsc "LSC" "LISP and Symbolic Computation")
@@ -1083,3 +1084,20 @@
    #:author "Lennart Augustsson"
    #:location (proceedings-location icfp #:pages '(239 250))
    #:date 1998))
+
+(define f-popl-2016
+  (make-bib
+   #:title "Bindings as Sets of Scopes"
+   #:author "Matthew Flatt"
+   #:location (proceedings-location popl #:pages '(705 717))
+   #:date 2016))
+
+(define c-jsl-1997
+  (make-bib
+   #:title "Three Uses of the Herbrand-Gentzen theorem in relating model theory and proof theory"
+   #:author "William Craig"
+   #:location (journal-location jsl
+                                #:volume 22
+                                #:number 3
+                                #:pages '(269 285))
+   #:date 1957))

icfp-2016/intro.scrbl

@@ -69,12 +69,11 @@ Furthermore, we demonstrate applications to regular expression matching,
 
 The key to our success--and also our weakness---is that we specialize
  procedure call sites based on compile-time constant values.
-Run-time input foils our technique, but nonetheless we have found the idea useful
+Run-time input foils the technique, but nonetheless we have found the idea useful
  for many common programming tasks.
-Moreover, our approach may be implemented as a library and used as a drop-in
+Moreover, the approach may be implemented as a library and used as a drop-in
  fix for existing code.
-Simply importing the library overrides standard procedures with our specialized
+Simply importing the library overrides standard procedures with specialized ones.
- ones.
 No further annotations are necessary; if specialization fails we default to
  the program's original behavior.
 Put another way, our technique interprets the @emph{letter}
@@ -95,21 +94,21 @@ The main requirement is that the language provides a means of altering the synta
 Such tools are more formally known as @emph{macro} or @emph{syntax extension}
  systems.
 At any rate, we sketch implementations for the five languages
- listed above in our conclusion.
+ listed above in the conclusion.
 
 Until that time when we must part, this pearl first describes our general
  approach in @Secref{sec:solution} and then illustrates the approach with
  specific examples in @Secref{sec:usage}.
 We briefly report on practical experiences with our library
  in @Secref{sec:experience}.
-Adventurous readers may enjoy learning about the details of our implementation
+Adventurous readers may enjoy learning about implementation details
  in @Secref{sec:implementation}, but everyone else is invited to skip to the
  end and try implementing a letter-of-values analysis in their language of choice.
 
 
 @; =============================================================================
 
-@parag{On Lineage}
+@parag{Lineage}
 
 Herman and Meunier demonstrated how Racket macros can propagate
  information embedded in string values and syntax patterns to a
@@ -127,7 +126,7 @@ We also give a modern description of Racket's macro system and handle definition
 
 @parag{Eager Evaluation}
 
-Our implementation is freely available as a Racket package.
+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/???/???"].
 Suggestions for a new package name are welcome.

icfp-2016/solution.scrbl

@@ -1,20 +1,98 @@
-#lang scribble/sigplan
+#lang scribble/sigplan @onecolumn
+
 
 @require["common.rkt"]
 
-@title{How its made}
+@title[#:tag "sec:solution"]{Interpretations and Translations}
+
+The out-of-bounds reference in @code{[0,1,2] !! 3} is evident from the
+ definition of @code{!!} and the values passed to it.
+We also know that @code{1 `div` 0} will go wrong because division by zero is
+ mathematically undefined.
+Similar reasoning based on the meaning of @racket{%d} and the number of variables
+ bound by anonymous functions like @code{\ x y z -> x} can determine the correctness
+ of calls to @racket[printf] and @racket[curry].
+
+In general, our analysis begins with a class of predicates for extracting
+ meta-information from expressions; for example the length of a
+ list value or arity of a procedure.
+
+    @exact|{$$\interp\ : \big\{\emph{expr} \rightarrow \emph{Maybe(value)}\big\}$$}|
+
+Applying a function @code{f} @exact|{$\in \interp\ $}| to a syntactically
+ well-formed expression should either yield a value describing some aspect
+ of the input expression or return a failure result.@note{The name @emph{interp}
+  is a mnemonic for @emph{interpret} or @emph{interpolant}@~cite[c-jsl-1997].}
+Correct predicates @code{f} should recognize expressions with some common
+ structure (not necessarily the expressions' type) and apply a uniform algorithm
+ to computer their result.
+The reason for specifying @exact|{$\interp\ $}| over expressions rather than
+ values will be made clear in @Secref{sec:usage}.
+
+Once we have predicates for extracting data from the syntax of expressions,
+ we can use the data to guide program transformations.
+The main result of this pearl is defining a compelling set of such transformations.
+
+    @exact|{$$\trans : \big\{ \emph{expr} \rightarrow \emph{expr}\big\} $$}|
+
+Each @exact|{${\tt g} \in \trans$}| is a partial function such that @exact|{${\tt (g~e)}$}|
+ returns either a specialized expression @exact|{${\tt e'}$}| or fails due to a value
+ error.
+These transformations should be applied to expressions @exact|{${\tt e}$}| before
+ type-checking; the critera for correct transformations can then be given
+ in terms of the language's typing judgment @exact|{$\vdash {\tt e} : \tau$}|
+ and untyped evaluation relation @exact|{$\untyped{{\tt e}} \Downarrow {\tt v}$}|,
+ where @exact|{$\untyped{{\tt e}}$}| is the untyped erasure of @exact|{${\tt e}$}|.
+We also assume a subtyping relation @exact|{$\subt$}| on types.
+
+@itemlist[
+  @item{@emph{
+    If @exact|{$\vdash {\tt e} : \tau$}| and @exact|{$\vdash {\tt e'} : \tau'$}|
+     then @exact|{$\tau' \subt \tau$}| and both
+     @exact|{$\untyped{{\tt e}} \Downarrow {\tt v}$}| and
+     @exact|{$\untyped{{\tt e'}} \Downarrow {\tt v}$}|.
+  }}
+  @; e:t e':t' => t' <: t /\ e <=> e'
+
+  @item{@emph{
+    If @exact|{$\not\vdash {\tt e} : \tau$}| but @exact|{$\vdash {\tt e'} : \tau'$}|
+     then @exact|{$\untyped{{\tt e}} \Downarrow {\tt v}$}| and
+     @exact|{$\untyped{{\tt e'}} \Downarrow {\tt v}$}|.
+  }}
+  @; -e:t e':t' => e <=> e'
+
+  @item{@emph{
+    If @exact|{$\vdash {\tt e} : \tau$}| but @exact|{${\tt e'} = \bot$}|
+     or @exact|{$\not\vdash {\tt e'} : \tau'$}|
+     then @exact|{$\untyped{{\tt e}} \Downarrow \mathsf{wrong}$}| or diverges.
+  }}
+  @; e:t -e':t' => e^
+]
+
+If neither @exact|{${\tt e}$}| nor @exact|{${\tt e'}$}| type checks, then we have no guarantees
+ about the run-time behavior of either term.
+The hope is that both diverge, but proving this fact in a realistic language is
+ more trouble than it is worth.
+
+@; Erasure, moral, immoral
+Finally, we say that a translation @exact|{${\tt (g~e) = e'}$}| is @emph{moral} if
+ @exact|{$\untyped{{\tt e}}$}| is @exact|{$\alpha$}|-equivalent to @exact|{$\untyped{{\tt e'}}$}|.
+Otherwise, the tranlation has altered more than just type annotations and is
+ @emph{immoral}.
+All our examples in @Secref{sec:intro} can be implemented as moral translations.
+Immoral translations are harder to show correct, but also much more useful.
+
+
+@; @section{Model}
+@; Traditional descriptions of typed calculi follow a two-stage approach.
+@; Expressions are first type-checked, then evaluated.
+@; For our framework we need to introduce a first step, elaboration,
+@;  which takes place before type checking.
+@; 
+@; To this end, we adapt the macro system model from Flatt@~cite[f-popl-2016]
+@;  with a simple type system.
+@; Syntactically-valid expressions in the language are initially untyped.
+@; The first set of 
 
-We describe our technique in terms of four functions on syntax objects.
-Our implementation is in Typed Racket, but we believe
-      Clojure,
-      Haskell,
-      Javascript,
-      OCaml,
-      Rust,
-  and Scala
- could reproduce our results.@note{We list two non-essential difficulties in
-  @todo{secref}.}
-@; The hope in listing these languages up-front is to spark readers' imagination
-@; before we give our own solution in Section 3
 
 

icfp-2016/texstyle.tex

@@ -1,6 +1,7 @@
 % Better horizontal rules
 \usepackage{booktabs}
 \usepackage{listings}
+\usepackage{stmaryrd}
 \lstset{language=ML}
 \usepackage[usenames,dvipsnames]{xcolor}
 \usepackage{multicol}
@@ -28,3 +29,8 @@
 \let\llcorner\relax
 \let\lrcorner\relax
 \usepackage{amssymb}
+
+\newcommand{\interp}{\llbracket\emph{interp}\rrbracket}
+\newcommand{\untyped}[1]{\lfloor #1 \rfloor}
+\newcommand{\trans}{\llbracket\emph{transform}\rrbracket}
+\newcommand{\subt}{\mathbf{<:\,}}