[icfp] conclusion outline

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?

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"]

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}
 @;

icfp-2016/related.scrbl

@@ -1,3 +0,0 @@
-#lang scribble/sigplan
-
-@section{Related Work}

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}