From 54dcc0344fea6ac376dd1747d2e8a16c42de1a9b Mon Sep 17 00:00:00 2001 From: ben Date: Sun, 13 Mar 2016 22:05:37 -0400 Subject: [PATCH] [icfp] conclusion outline --- icfp-2016/conclusion.scrbl | 34 ++++++++++++++++++++++++++++++---- icfp-2016/intro.scrbl | 1 + icfp-2016/paper.scrbl | 2 +- icfp-2016/related.scrbl | 3 --- icfp-2016/solution.scrbl | 2 ++ 5 files changed, 34 insertions(+), 8 deletions(-) delete mode 100644 icfp-2016/related.scrbl diff --git a/icfp-2016/conclusion.scrbl b/icfp-2016/conclusion.scrbl index 5f366b0..afb2491 100644 --- a/icfp-2016/conclusion.scrbl +++ b/icfp-2016/conclusion.scrbl @@ -1,8 +1,34 @@ #lang scribble/sigplan -@section{Conclusion} +@title[#:tag "sec:conclusion"]{Closing the Books} -Meta-programming and compile-time constants. +@; TODO yuck approach to ... to +This pearl described an approach to using a macro system to enhance + the analysis of an existing type system. +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. -We're hardly fancy and handily defeated by lambdas. -CFA would help. +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: + +@parag{Typed Clojure} has + +@parag{Haskell} +@parag{OCaml} +@parag{Rust} +@parag{Scala} + +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? diff --git a/icfp-2016/intro.scrbl b/icfp-2016/intro.scrbl index 24edf2b..5aac8a3 100644 --- a/icfp-2016/intro.scrbl +++ b/icfp-2016/intro.scrbl @@ -5,6 +5,7 @@ @; : can you give more example? @; : too generous to other languages -- why didn't you do the entire paper in hs? @; - a note on macro-land? where truthy & boolean monads are king? +@; - transf vs. macro @require["common.rkt"] diff --git a/icfp-2016/paper.scrbl b/icfp-2016/paper.scrbl index 4d30209..d54bdcd 100644 --- a/icfp-2016/paper.scrbl +++ b/icfp-2016/paper.scrbl @@ -41,7 +41,7 @@ @include-section{experience.scrbl} @; Merge with usage? @include-section{implementation.scrbl} @;@include-section{related.scrbl} -@;@include-section{conclusion.scrbl} +@include-section{conclusion.scrbl} @;@section[#:style 'unnumbered]{Acknowledgments} @; diff --git a/icfp-2016/related.scrbl b/icfp-2016/related.scrbl deleted file mode 100644 index 0251674..0000000 --- a/icfp-2016/related.scrbl +++ /dev/null @@ -1,3 +0,0 @@ -#lang scribble/sigplan - -@section{Related Work} diff --git a/icfp-2016/solution.scrbl b/icfp-2016/solution.scrbl index 85dd0f6..2c58684 100644 --- a/icfp-2016/solution.scrbl +++ b/icfp-2016/solution.scrbl @@ -20,6 +20,8 @@ Generalizing these observations, our analysis begins with a class of @exact|{$$\interp\ : \big\{\emph{expr} \rightarrow \emph{Maybe\,(value)}\big\}$$}| +@; TODO list footnote, state "predicate" as word of choice (for lack ofa better one) + Applying a function @exact|{${\tt f} \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}