suzanne.soy/trivial
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

[icfp] a happy ending

Browse Source
This commit is contained in:
ben 2016-03-16 05:08:55 -04:00
parent b50773ee46
commit a3ece184bc
1 changed files with 38 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

89
icfp-2016/conclusion.scrbl
View File

@ -3,56 +3,43 @@
@title[#:tag "sec:conclusion"]{Closing the Books} @title[#:tag "sec:conclusion"]{Closing the Books}
@; TODO yuck approach to ... to This pearl described a class of macros called @emph{textualist elaborators}
This pearl described an approach to using a macro system to enhance designed to enhance the analysis of an existing type system without any
the analysis of an existing type system. 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, Whereas types support reasoning independent of data representations,
we hope to have shown that reflecting a little value information we have argued that at least the source code details of values
into the compile-time environment can pay off for common programming tasks. are worth taking into account during type checking.
@; Moreover, can do without programmer annotations 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 @; @parag{Lineage}
can be turned into type constraints. @;
@; Herman and Meunier demonstrated how Racket macros can propagate
A key thesis behind this work is that the analysis can be implemented @; data embedded in string values and syntax patterns to a
in a variety of languages using their existing type and syntax extension @; static analyzer@~cite[hm-icfp-2004].
systems. @; Their illustrative examples were format strings, regular expressions,
Indeed: @; and database queries.
@; TODO shorten this @; Relative to their pioneering work, we adapt Herman & Meunier's
@; transformations to a typed language by inserting type annotations and boolean
@parag{Typed Clojure} has a flexible macro system derived from Common Lisp. @; guards into the programs.
Built-in functions @tt{macroexpand} and @tt{with-meta} correspond to Racket's @; Our treatment of definition forms is also new.
@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?