From a3ece184bc085bedf8d45dab4c38eff847a10612 Mon Sep 17 00:00:00 2001 From: ben Date: Wed, 16 Mar 2016 05:08:55 -0400 Subject: [PATCH] [icfp] a happy ending --- icfp-2016/conclusion.scrbl | 89 ++++++++++++++++---------------------- 1 file changed, 38 insertions(+), 51 deletions(-) diff --git a/icfp-2016/conclusion.scrbl b/icfp-2016/conclusion.scrbl index 091251e..8c263fb 100644 --- a/icfp-2016/conclusion.scrbl +++ b/icfp-2016/conclusion.scrbl @@ -3,56 +3,43 @@ @title[#:tag "sec:conclusion"]{Closing the Books} -@; TODO yuck approach to ... to -This pearl described an approach to using a macro system to enhance - the analysis of an existing type system. +This pearl described a class of macros called @emph{textualist elaborators} + designed to enhance the analysis of an existing type system without any + input from programmers. +The main idea is to interpret values from the source code of a program + and elaborate the same code into a form that helps the type system see what is + obvious to a human reader. +From an engineering perspective, we used tools provided by Racket's macro + system to enable local, compositional, and lexically-scoped reasoning + when designing new elaborators. + +A key hypothesis of this pearl is that our framework could be implemented in + a variety of languages using their existing type and syntax extension systems. +Typed Clojure's macros@~cite[clojure-macros], + Rust's compiler plugins@~cite[rust-compiler-plugins], + and Scala's LMS framework@~cite[ramho-hosc-2013] + seem especially well-suited to the task. +Template Haskell@~cite[spj-haskell-2002] and OCaml ppx@note{@url["http://whitequark.org/blog/2014/04/16/a-guide-to-extension-points-in-ocaml/"]} could + also reproduce the core ideas, albeit + after the programmer modifies function call-sites. + Whereas types support reasoning independent of data representations, - we hope to have shown that reflecting a little value information - into the compile-time environment can pay off for common programming tasks. -@; Moreover, can do without programmer annotations + we have argued that at least the source code details of values + are worth taking into account during type checking. +Doing so will catch more errors and enable unconventional forms of polymorphism, + all without changes to the language's type system or the programmer's code. -Indeed, a tempting subtitle for this pearl would be - @emph{compile-time constant propagation}, because that is precisely what we do. -Each application in @Secref{sec:usage} is a way that constant data - can be turned into type constraints. - -A key thesis behind this work is that the analysis can be implemented - in a variety of languages using their existing type and syntax extension - systems. -Indeed: -@; TODO shorten this - -@parag{Typed Clojure} has a flexible macro system derived from Common Lisp. -Built-in functions @tt{macroexpand} and @tt{with-meta} correspond to Racket's - @racket[local-expand] and @racket[syntax-property]; with help from a library - implementing identifier macros,@note{@url["https://github.com/clojure/tools.macro"]} - we were able to implement a basic prototype untyped Clojure. - - -@parag{Template Haskell} could reproduce all the examples in @Secref{sec:usage} - as they are written, with constants in-line at each call site. -We are less sure how to associate and retrieve data regarding bound variables - at compile-time, idiomatically. - -@parag{OCaml} ppx - - -@parag{Rust} has a stable, pattern-based macro system and a powerful API - for writing compiler plugins. -The macro system appears too weak to reimplement our analyses, - but it would be interesting to explore the plugin API and try reimplementing - ideas like syntax classes and rename transformers. - - -@parag{Scala} users have at least two macro systems to choose from. -Both Scala Macros@~cite[b-scala-2013] and Lightweight Modular Staging@~cite[ro-gpce-2010] - - - -With out last words, we look to the future. -Although we gave criteria for correct predicates and translations - in @Secref{sec:solution}, we only claimed that the functions - shown in @Secref{sec:implementation} are correct. -Short of proving operational equivalence, could we concisely or automatically - show that our translations are correct? -Slightly more pressingly, can we relive the burden of propagating syntax properties? +@; @; ============================================================================= +@; +@; @parag{Lineage} +@; +@; Herman and Meunier demonstrated how Racket macros can propagate +@; data embedded in string values and syntax patterns to a +@; static analyzer@~cite[hm-icfp-2004]. +@; Their illustrative examples were format strings, regular expressions, +@; and database queries. +@; 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 definition forms is also new. +@;