From 3d276633a4a53791911913d95c39776b6ac79121 Mon Sep 17 00:00:00 2001 From: ben Date: Fri, 11 Mar 2016 06:50:13 -0500 Subject: [PATCH] [icfp] specifying translations and correctness --- icfp-2016/bib.rkt | 18 +++++++ icfp-2016/intro.scrbl | 15 +++--- icfp-2016/solution.scrbl | 106 +++++++++++++++++++++++++++++++++------ icfp-2016/texstyle.tex | 6 +++ 4 files changed, 123 insertions(+), 22 deletions(-) diff --git a/icfp-2016/bib.rkt b/icfp-2016/bib.rkt index 70c0c0b..7b6b247 100644 --- a/icfp-2016/bib.rkt +++ b/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)) diff --git a/icfp-2016/intro.scrbl b/icfp-2016/intro.scrbl index c3f3cba..72c8f76 100644 --- a/icfp-2016/intro.scrbl +++ b/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 - ones. +Simply importing the library overrides standard procedures with specialized 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. diff --git a/icfp-2016/solution.scrbl b/icfp-2016/solution.scrbl index 4d04686..2761bc5 100644 --- a/icfp-2016/solution.scrbl +++ b/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 diff --git a/icfp-2016/texstyle.tex b/icfp-2016/texstyle.tex index 6676b4e..4a2a643 100644 --- a/icfp-2016/texstyle.tex +++ b/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{<:\,}}