\documentclass{beamer}

%include lhs2TeX.fmt
%include polycode.fmt

\usetheme{uucs}
\usepackage{tikz}
\usepackage{textpos}

\usetikzlibrary{trees,arrows,decorations,shapes,fit,backgrounds}

\pgfdeclarelayer{background}
\pgfsetlayers{background,main}

\author{Arie Middelkoop \\ \vspace{4mm} \small{in cooperation with:}\\S. Doaitse Swierstra \\ Atze Dijkstra}
\title{Dependently-Typed Attribute Grammars}

\institute{%
  Dept.\ of Information and Computing Sciences, Utrecht University\\%
  P.O.\ Box 80.089, 3508 TB Utrecht, The Netherlands\\%
  Web pages: \url{http://www.cs.uu.nl/wiki/Center}}
\date{IFL 2010 \\ 01 Sep 2010}

%format attr = "\mathbf{attr}" 
%format data = "\mathbf{data}"
%format sem = "\mathbf{sem}"
%format itf = "\mathbf{itf}"
%format inh = "\mathbf{inh}"
%format syn = "\mathbf{syn}"
%format tail = "\mathbf{tail}"
%format match = "\mathbf{match}"
%format eval = "\mathbf{eval}"
%format child = "\mathbf{child}"
%format visit = "\mathbf{visit}"
%format order = "\mathbf{order}"
%format huse = "\mathbf{use}"
%format . = "."
%format ^^ = "\;"
%format ^^^ = "\hspace{1cm}"
%format bf x = "\emph{" x "}"

%format v1
%format v2
%format ast
%format ty = "\tau"
%format ty1
%format ty2
%format ty3
%format ty4
%format subst = "\sigma"
%format emptyset = "\emptyset"
%format e1
%format e2
%format <|> = |
%format <*> = *
%format <$> = $
%format alpha = "\alpha"

%format rulerfront = "{\mbox{\scshape ruler-front}}"
%format rulercore = "{\mbox{\scshape ruler-core}}"
%format rulerfrontagda = "{\mbox{\scshape ruler-front}_{\mbox{\scshape agda}}}"

%format . = "."
%format ^^^ = "\;\;\;"
%format ^^^^ = "\hspace{1em}"

%format epsilon = "\epsilon"
%format (sub (x) (y)) = "{" x "}_{" y "}"
%format (sup (x) (y)) = "{" x "}^{" y "}"
%format (many (x))    = "\overline{" x "}"
%format forall = "\forall"

%format Gamma = "\Gamma"
%format Sigma = "\Sigma"
%format Phi = "\Phi"
%format :- = "\vdash"
%format emptyset = "\emptyset"
%format sep = "\:;\:"
%format bar = "|"
%format ::: = "\::\:"
%format `union` = "\cup"
%format union = "\cup"
%format `intersection` = "\cap"
%format intersection = "\cap"
%format `subset` = " \subseteq "
%format .== = "\doteq"
%format `diam` = "\diamond"
%format neg a = "\neg" a
%format bottom = undefined

%format Gamma0
%format Gamma1
%format Gamma2
%format Gamma3
%format Gamma4
%format Gamma'
%format Gamma0
%format Gamma''
%format inGamma = "in" Gamma
%format inGamma'

%format Set1
%format Set2

%format _elem = "\_\in\_"
%format _subseq = "\_\sqsubseteq\_"
%format `subseq` = "\sqsubseteq{}"
%format `mbElem` = "\in_?"
%format _mbElem  = "\_\in_?\_"
%format `mbEqual` = "\equiv_?"
%format `Either` = "\uplus"

%format inj1
%format inj2
%format prv1
%format prv2
%format prv'

%format i1
%format i2
%format x1
%format x2
%format x3
%format x4
%format es1
%format es2
%format t1
%format t2
%format a1
%format a2

%format ty         = "\tau"
%format tail       = "\kw{tail}"
%format and        = "\kw{and}"
%format attr       = "\kw{attr}"
%format data       = "\kw{data}"
%format sem        = "\kw{sem}"
%format inh        = "\kw{inh}"
%format syn        = "\kw{syn}"
%format con        = "\kw{con}"
%format clause     = "\kw{clause}"
%format default    = "\kw{default}"
%format itf        = "\kw{itf}"
%format visit      = "\kw{visit}"
%format internal   = "\kw{internal}"
%format match      = "\kw{match}"
%format child      = "\kw{child}"
%format invoke     = "\kw{invoke}"
%format datasem    = "\kw{datasem}"
%format grammar    = "\kw{grammar}"
%format term       = "\kw{term}"
%format nonterm    = "\kw{nonterm}"
%format prod       = "\kw{prod}"
%format context    = "\kw{context}"
%format contexts   = "\kw{contexts}"
%format attach     = "\kw{attach}"
%format detach     = "\kw{detach}"

%format adata = "\uw{data}"
%format awhere = "\uw{where}"
%format with = "\uw{with}"
%format ainh = "inh"
%format asyn = "syn"

\newcommand\kw[1]{\ensuremath{\mathbf{#1}}}
\newcommand\uw[1]{\ensuremath{\underline{\mathsf{#1}}}}
\newcommand\comment[1]{}
\newcommand\ccontents[1]{\begin{minipage}{8em} #1 \end{minipage}}

\begin{document}

\frontmatter

\begin{frame}
  \titlepage
\end{frame}

\mainmatter

\begin{frame}
  \frametitle{Introduction}
  
  \begin{itemize}
  \item Attribute Grammar
  \item Strongly-typed attributes
  \item Ad-hoc: attributes with polymorphic types
  \item Now: attributes with dependent types
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Research}

  \centering
  \begin{tikzpicture}
    
    \node(A){Type System};
    \node[below of=A](B){Type Inferencer};
    \node[below of=B](C){Certified Type Inferencer};
    
    \draw[->] (A.south) to (B.north);
    \draw[->] (B.south) to (C.north);
    
    \node[right of=A, xshift=25mm](A1){\color{uuxred}Specification};
    \node[below of=A1](B1){\color{uuxred}Implementation};
    \node[below of=B1](C1){\color{uuxred}Proof};
    
    \node[below of=C, yshift=-10mm]{\Large{With Attribute Grammars?}};
    
  \end{tikzpicture}

\end{frame}

%format p1
%format p2
%format p3
%format n1
%format n2
%format i1
%format i2
%format s1
%format s2

\begin{frame}
  \frametitle{Attribute Grammars}
  
  \begin{itemize}
  \item Context-free grammar
    \begin{itemize}
    \item (Non)terminals
    \item Productions
    \item Parse tree, derivation tree
    \end{itemize}
  \item Attributes
    \begin{itemize}
    \item Parameters of nonterminals
    \item Inherited attributes
    \item Synthesized attributes
    \end{itemize}
  \item Rules
    \begin{itemize}
    \item Functions between attributes per production
    \end{itemize}
  \end{itemize}
  
  \begin{center}
  \begin{tikzpicture}
    [ nd/.style={circle, minimum size=12mm, very thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\footnotesize}
    , attr/.style={rectangle, minimum size=6.2mm, node distance=6mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\footnotesize}
    , inh/.style={attr}
    , syn/.style={attr}
    , leftfirst/.style={xshift=-4mm}
    , rightfirst/.style={xshift=4mm}
    , arr/.style={->,dashed, very thick}
    ]
    \node[nd](n1){|p1 : n1|}
      [sibling distance=40mm, level distance=10mm]
      child {
        node[nd](n2){|p2 : n2|}
      }
      child {
        node[nd](n3){|p1 : n1|}
          child {
            node[nd](n4){|p2 : n2|}
          }
          child {
            node[nd](n5){|p3 : n2|}
          }
      };
    
    \node[inh,leftfirst]  (n1inh1) [left of=n1] {|i1|};
    \node[syn,rightfirst] (n1syn1) [right of=n1] {|s1|};
    
    \node[inh,leftfirst] (n2inh1) [left of=n2] {|i2|};
    \node[syn,rightfirst] (n2syn1) [right of=n2] {|s2|};
    
    \node[inh,leftfirst] (n3inh1) [left of=n3] {|i1|};
    \node[syn,rightfirst] (n3syn1) [right of=n3] {|s1|};
    
    \node[inh,leftfirst] (n4inh1) [left of=n4] {|i2|};
    \node[syn,rightfirst] (n4syn1) [right of=n4] {|s2|};
    
    \node[inh,leftfirst] (n5inh1) [left of=n5] {|i2|};
    \node[syn,rightfirst] (n5syn1) [right of=n5] {|s2|};
  \end{tikzpicture}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Functional Model}
  
  \begin{itemize}
  \item AGs: attributes as a function of other attributes
  \end{itemize}
  
  \begin{center}
  %% Attributed tree with an env (inh), type (syn), and a subst (threaded)
  \begin{tikzpicture}
    [ nd/.style={circle, minimum size=12mm, very thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\footnotesize}
    , attr/.style={rectangle, minimum size=4mm, node distance=6mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\footnotesize}
    , inh/.style={attr}
    , syn/.style={attr}
    , leftfirst/.style={xshift=-4mm}
    , rightfirst/.style={xshift=4mm}
    , arr/.style={->,dashed, very thick}
    ]
    \node[nd](n1){|App|}
      [sibling distance=40mm, level distance=18mm]
      child {
        node[nd](n2){|Var|}
      }
      child {
        node[nd](n3){|App|}
          child {
            node[nd](n4){|Var|}
          }
          child {
            node[nd](n5){|Const|}
          }
      };
    
    \pause  
    
    \node[inh,leftfirst]  (n1inh1) [left of=n1]      [label={[rotate=90,xshift=4mm,yshift=-2.5mm]above:|env|}] {};
    \node[syn,rightfirst] (n1syn1) [right of=n1]     [label={[rotate=90,xshift=3mm,yshift=-2.5mm]above:|ty|}] {};
    
    \node[inh,leftfirst] (n2inh1) [left of=n2] {};
    \node[syn,rightfirst] (n2syn1) [right of=n2] {};
    
    \node[inh,leftfirst] (n3inh1) [left of=n3] {};
    \node[syn,rightfirst] (n3syn1) [right of=n3] {};
    
    \node[inh,leftfirst] (n4inh1) [left of=n4] {};
    \node[syn,rightfirst] (n4syn1) [right of=n4] {};
    
    \node[inh,leftfirst] (n5inh1) [left of=n5] {};
    \node[syn,rightfirst] (n5syn1) [right of=n5] {};
    
    \pause
    
    \draw[arr] (n2inh1) to (n1inh1);
    \draw[arr] (n3inh1) to (n1inh1);
    \draw[arr] (n4inh1) to (n3inh1);
    \draw[arr] (n5inh1) to (n3inh1);
    
    \draw[arr] (n1syn1) to (n2syn1);
    \draw[arr] (n1syn1) to (n3syn1);
    \draw[arr] (n3syn1) to (n4syn1);
    \draw[arr] (n3syn1) to (n5syn1);
    
    \draw[arr] (n2syn1.south) to [out=-90,in=-90] (n2inh1.south);
    \draw[arr] (n4syn1.south) to [out=-90,in=-90] (n4inh1.south);
    
    \pause
    
    
    \node[syn]            (n1syn2) [right of=n1syn1] [label={[rotate=90,xshift=4.5mm,yshift=-2.5mm]above:|errs|}] {};
    \node[syn] (n2syn2) [right of=n2syn1] {};
    \node[syn] (n3syn2) [right of=n3syn1] {};
    \node[syn] (n4syn2) [right of=n4syn1] {};
    \node[syn] (n5syn2) [right of=n5syn1 ] {};
    \draw[arr] (n1syn2) to (n2syn2);
    \draw[arr] (n1syn2) to (n3syn2);
    \draw[arr] (n3syn2) to (n4syn2);
    \draw[arr] (n3syn2) to (n5syn2);
    \draw[arr] (n2syn2.south) to [out=-90,in=-90] (n2inh1.south);
    \draw[arr] (n4syn2.south) to [out=-90,in=-90] (n4inh1.south);
  \end{tikzpicture}
  \end{center}
  
  \comment{arrows represents code}
  \comment{map traversal to a function from inh to syn}
\end{frame}

\begin{frame}
  
  \centering
  \Large{Just Add Some Extra Attributes (tm)}
  
  \vspace{1cm}
  \begin{itemize}
  \item Separate Specification
  \item Implicit Rules
  \end{itemize}
  
\end{frame}

\begin{frame}
  
  \begin{center}
  \Large{Algorithm = Evaluation Strategy\\+ Extra Attributes}
  \end{center}
  
  \pause
  
  With a Higher-Order AG,
  \begin{center}
  \Large{Evaluation Strategy = Basic Strategy\\+ Extra Attributes}
  \end{center}
  
\end{frame}

\begin{frame}
  
  With dependently-typed programming:
  \begin{center}
  \Large{Proof = Program + quite a bit More Program}
  \end{center}
  
\end{frame}

\begin{frame}
  \frametitle{Challenges}
  
  In theory:
  
  \begin{itemize}
  \item Termination
        \begin{itemize}
        \item Ordered Attribute Grammars
        \item Total attribute functions
      \end{itemize}
  \item Attributes may take types as values
  \item The type of an attribute may refer to an attribute
  \end{itemize}
  
  In practice (see paper):
  
  \begin{itemize}
  \item Attribute functions not total
  \item Reason: synthesized attributes not independent
  \item Example: suppose attribute |tp| and attribute |errs|,
        such that former is defined iff the latter is empty
  \end{itemize}
  
\end{frame}

\begin{frame}
  \frametitle{Example}
  
  \begin{itemize}
  \item Compiler written in Agda, using AGs
  \item Translates some source AST to a target AST
  \item Source and target language: sequence of def/use sites
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Source Language}
  
  \begin{code}
  grammar Source : Set
    prod use         term     nm     : Ident
    prod def         term     nm     : Ident
    prod _`diam`_    nonterm  left   : Source
                     nonterm  right  : Source
  \end{code}
  
  \begin{code}
    def x `diam` def y `diam` use x `diam` use y `diam` use x
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Target Language}
  
  \begin{code}
  adata Target : (Gamma : Env) -> Set awhere
    def       : (nm : Ident) -> (nm `elem` Gamma) -> Target Gamma
    use       : (nm : Ident) -> (nm `elem` Gamma) -> Target Gamma
    _`diam`_  : (left : Target Gamma)  -> (right : Target Gamma)
                                       -> Target Gamma

  adata Err : Env -> Set where
    scope : (nm : Ident) -> neg (nm `elem` Gamma) -> Err Gamma
  
  Errs : Env -> Set
  Errs env = List (Err env)

  Env : Set
  Env = List Ident
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Interface of |Source| nonterminal}
  
  \begin{code}
  itf Source
    visit analyze
      syn  gathEnv    :  Env
    visit translate 
      inh  finEnv     :  Env
      inh  gathInFin  :  asyn.gathEnv `subseq` ainh.finEnv
      syn  outcome    :  (Errs ainh.finEnv) `Either`
                         (Target ainh.finEnv)
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Support Code}
  
  \begin{code}
  adata _subseq : (Gamma1 : Env) -> (Gamma2 : Env) -> Set awhere
    trans     :  Gamma1 `subseq` Gamma2 -> Gamma2 `subseq` Gamma3 -> Gamma1 `subseq` Gamma3
    subLeft   :  Gamma1 `subseq` (Gamma1 ++ Gamma2)
    subRight  :  Gamma2 `subseq` (Gamma1 ++ Gamma2)
  \end{code}
  
  \begin{code}
  adata _elem : (nm : Ident) -> (Gamma : Env) -> Set awhere
    here :  nm `elem` (nm :: Gamma')
    next :  nm `elem` Gamma -> nm `elem` (nm' :: Gamma)
  \end{code}
  
  \begin{code}
  inSubset :  (Gamma' `subseq` Gamma) -> nm `elem` Gamma' -> nm `elem` Gamma
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Semantics - 1}
  
  \begin{code}
  datasem Source
    prod use
      lhs.gathEnv      = []
      lhs.outcome      with loc.nm `mbElem` lhs.finEnv
                       | inj1 notIn  = inj1 [ scope loc.nm notIn ]
                       | inj2 isIn   = inj2 (use loc.nm isIn)
    prod def
      lhs.gathEnv      = [ loc.nm ]
      loc.inFin        = inSubset lhs.gathInFin here
      lhs.outcome      = inj2 (def loc.nm loc.inFin)
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Semantics - 2}
  
  \begin{code}
  datasem Source
    prod _`diam`_
      left.finEnv      = lhs.finEnv
      right.finEnv     = lhs.finEnv
      
      lhs.gathEnv      = left.gathEnv ++ right.gathEnv

      left.gathInFin   = trans  subLeft lhs.gathInFin
      right.gathInFin  = trans  (subRight lhs.finEnv)
                                lhs.gathInFin

      lhs.outcome      with left.outcome
                       | inj1 es   with  right.outcome
                       | inj1 es1  | inj1 es2  = inj1 (es1 ++ es2)
                       | inj1 es1  | inj2 _    = inj1 es1
                       | inj2 t1   with  left.outcome
                       | inj2 t1   | inj1 es1  = inj1 es1
                       | inj2 t1   | inj2 t2   = inj2 (t1 `diam` t2)
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Cool Stuff}
  
  \begin{itemize}
  \item Represent (Dependent) Data Types as Attribute Grammar
          \begin{itemize}
          \item Parameters of data types are attributes
          \item E.g. |Target| can be specified with AGs
          \end{itemize}
  \item Model for representing type variables for AGs in a polymorphically typed language
          \begin{itemize}
          \item Inherited type-attr: universally quantified type var
          \item Synthesized type-attr: existential type var
          \item The type of such an attribute: a constraint (e.g. type class)
          \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Towards a Certified Compiler}
  
  \begin{itemize}
  \item Ensure termination
  \item Gradually prove more properties by adding additional attributes
  \item Negative side of the coin: manual labour, still infeasible for large compilers
  \item Unless we have reusable building blocks...
          \begin{itemize}
          \item Ongoing work on Nested Attribute Grammars
          \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Conclusion}
  
  \begin{itemize}
  \item Dependently-typed AGs: proofs are extra attributes
  \item Just Add Extra Attributes (tm)
  \item Advantage: specify total attr functions between attributes, then
        evaluation code and termination proof for free.
  \end{itemize}
  
  \begin{tikzpicture}
    [ block/.style = {rectangle, draw=black, thick, font=\scriptsize}
    , file/.style = {yshift=-5mm, font=\small}
    , remarks/.style = {yshift=-5mm, font=\scriptsize}
    , sibling distance=35mm, level distance=9mm
    ]

    \node[block] (relatedwork) {\emph{further read: \url{http://people.cs.uu.nl/ariem/}}}
          child {
            node[block] (breadthfirst) {\ccontents{Breadth-first AGs}}
          }
          child {
            node[block] (sideeffect) {\ccontents{Side-effectful AGs}}
              child {
                node[block] (iterative) {\ccontents{Iterative AGs}}
                  child {
                    node[block] (nested) {\ccontents{Nested AGs}}
                  }
                  child {
                    node[block] (gadts) {\ccontents{Use Case: GADTs}}
                      child {
                        node[block] (depend) {\ccontents{Dependently-typed AGs}}
                      }
                  }
                  child {
                    node[block] (firstclass) {\ccontents{Use Case: First-class Polymorphism}}
                  }
              }
          }
          child {
            node[block] (aspect) {\ccontents{Aspect-oriented Rules}}
              child {
                node[block] (defer) {\ccontents{Residuation}}
              }
          };
  \end{tikzpicture}
\end{frame}

\end{document}