From 2a46d38539c7299654b25c34cd6cb08b4f01518a Mon Sep 17 00:00:00 2001
From: ben <benjaminlgreenman@gmail.com>
Date: Tue, 1 Mar 2016 19:57:16 -0500
Subject: [PATCH] [icfp] update teaser, after M.meeting

---
 icfp-2016/teaser.tex | 89 +++++++++++++++++++++++++++++++++++---------
 1 file changed, 72 insertions(+), 17 deletions(-)

diff --git a/icfp-2016/teaser.tex b/icfp-2016/teaser.tex
index 3bd41b7..6744f43 100644
--- a/icfp-2016/teaser.tex
+++ b/icfp-2016/teaser.tex
@@ -1,4 +1,6 @@
 \documentclass{article}
+\usepackage{amsmath}
+\usepackage{mathpartir}
 \usepackage{palatino}
 \begin{document}
 \begin{abstract}
@@ -15,30 +17,70 @@
    give a nice experience.
 \end{abstract}
 
-\subsection*{Outline}
-
 Technique works by identifying common properties of a set of
  values and using these properties in a macro transformation.
 
+\subsubsection*{Key Functions}
 \begin{itemize}
-  \item Context-free, syntactic, curry-style ``type'' checking.
-  \subitem  {\texttt{typeof : (-> Syntax (TypeTag x MetaData))}}
-  \item Operations using the type tag \& metadata.
-  \subitem  {\texttt{transformations : (-> TypeTag (Set (-> Syntax Syntax)))}}
+\item Context-free, syntactic way of associating a Curry-style ``type'' to a value.
+\subitem  $\mathsf{typeof} : Syntax \rightarrow TypeTag$
+\item (Optional) Propogate metadata to future references of an identifier
+\subitem $\mathsf{attach} : Syntax \times Meta \rightarrow Syntax$
+\item Tag-indexed family of functions that extract data from a syntactic value.
+\subitem $\mathsf{analyze} : TypeTag \rightarrow (Syntax \rightarrow Meta$
+\item Transform a context based on metadata-augmented syntax for the hole.
+\subitem $\mathsf{transform : (-> Context (Syntax x Meta) Syntax$
 \end{itemize}
 
+\subsubsection*{Correctness}
+
+Suppose {\tt transform} $E~e = e'$.
+A correct transformation should only catch bugs in $e$.
+
+% Is this novel at all?
+\begin{mathpar}
+  \inferrule*{
+    \vdash e : \tau
+    \\
+    \vdash e' : \tau'
+  }{
+    \tau' <: \tau
+    \\
+    e \Uparrow \iff e' \Uparrow
+    \\
+    e \Downarrow v \iff e' \Downarrow v
+  }
+
+  \inferrule*{
+    \vdash e : \tau
+    \\
+    \not\vdash e' : \tau'
+  }{
+    e \Uparrow
+  }
+
+  \inferrule*{
+    \not\vdash e : \tau
+  }{
+    \not\vdash e' : \tau'
+  }
+\end{mathpar}
+
+
+\subsubsection*{Examples}
+
 Table defines type tags and related \texttt{transformations}.
 
 \vspace{0.4cm}
 \begin{center}
-\hspace{-4cm}\begin{tabular}{l l l l l}
-  Type          &    Syntax Category          &    Metadata    &    Applications    \\\hline\hline
-\\Format String &       {\tt string}          &     \#/$\tau$ of fmt chars & Check args to {\tt printf}
-\\Regexp        &  {\tt string} / {\tt bytes} & \# groups & Check paren-matching${}^*$, smarter return type
-\\Query String  &  {\tt string}               & \# of {\tt \$} vars & Check arity
-\\Function      &  {\tt (lambda ...)}         & Arity        & Compile-time arity check for {\tt apply}
-\\Numbers       &  {\tt number}               & Value & Constant folding, accurate types
-\\Vectors       &  {\tt `\#( ... )}            & Length & Access, size, fast operations
+\hspace{-3cm}\begin{tabular}{l l l l l}
+  Type          &    Syntax Category          &    Metadata            &    Applications    \\\hline\hline
+\\Format String &  {\tt string}               & \#/$\tau$ of fmt chars & Check args to {\tt printf}
+\\Regexp        &  {\tt string} / {\tt bytes} & \# groups              & Check paren-matching${}^*$, smarter return type
+\\Query String  &  {\tt string}               & \# of {\tt \$} vars    & Check arity
+\\Function      &  {\tt (lambda ...)}         & Arity                  & Compile-time arity check for {\tt apply}
+\\Numbers       &  {\tt number}               & Value                  & Constant folding, accurate types
+\\Vectors       &  {\tt `\#( ... )}           & Length                 & Access, size, fast operations
 \end{tabular}
 \end{center}
 
@@ -54,8 +96,21 @@ Table defines type tags and related \texttt{transformations}.
   \subitem $\circ~$ Write macro that looks for \& uses tags {\tt equal?}
 \end{itemize}
 
-P.S. Our goal is not to discourage dependent types, but rather to advertise macros.
-P.P.S. Jack Firth might be using the library. Email him?
-P.P.P.S Should work in other languages, hard part will be rename transformers
+~
+\\P.S. Our goal is not to discourage dependent types, but rather to advertise macros.
+\\P.P.S. Jack Firth might be using the library. Email him?
+\\P.P.P.S Should work in other languages, hard part will be rename transformers
+
+
+\subsubsection*{Outline}
+\begin{itemize}
+\item Examples of ``syntactically obvious'' dependent types.
+\item Not-so-obvious examples, i.e. regular expressions \& vector operations.
+\item High-level solution
+\item Racket implementation, brief correctness argument
+\subitem (Cool things like {\tt set!-transformer})
+\item Limitations \& near misses
+\item Experience report?
+\end{itemize}
 
 \end{document}