\documentclass{beamer}

%include lhs2TeX.fmt
%include polycode.fmt

\usepackage{tikz}
\usepackage{textpos}
\usepackage{mathpartir}

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

\author{Arie Middelkoop}
\title{Fun with Attribute Grammars}

%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 . = "."
%format ^^ = "\;"
%format ^^^ = "\hspace{1cm}"

%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

\newcommand\comment[1]{}
\newcommand\intermission[1]{
  \begin{frame}
    \begin{center}
      \Large{#1}
    \end{center}
  \end{frame}
}

\begin{document}

\maketitle

\section{Outline}

\begin{frame}
  \frametitle{Outline}

  \begin{itemize}
  \item Attribute Grammars (AGs)
    \begin{itemize}
    \item Theory: specification of semantics of programming languages
    \item Practice: tree walks that decorate ASTs
    \end{itemize}
    \comment{People in the room will have some experience with these}
  \item Motivation: Utrecht Haskell Compiler (UHC)
    \begin{itemize}
    \item Makes heavy use of AGs
       \comment{using the UUAG system, which has:}
       \comment{separate specification of rules for attributes}
       \comment{copy rules (collection attributes) + many more meta-programming patterns}
       \comment{higher-order attributes}
    \item Problem: some tree walks cannot be described
    \end{itemize}
  \item Use case: unification
    \begin{itemize}
    \item Case distinction on multiple trees
    \item (Order of evaluation concerning substitution)
    \end{itemize}
    \comment{other use-cases in paper}
  \item Visit Functions
    \begin{itemize}
    \item AGs are a front-end for visit functions
    \item This talk: another front-end for visit functions
      \comment{That resemble attribute grammars}
    \item (Static constraints on the life-time of attributes)
      \comment{... and thus the order of evaluation}
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Sometimes programming is like...}
  
  \begin{center}
  \includegraphics[width=7cm]{DSC00564.JPG}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{But you rather want it like...}
  
  \begin{center}
  \includegraphics[width=9cm]{DSC00561.JPG}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{*A-team sound here*}
  
  \begin{center}
  \begin{tikzpicture}
    \node[cloud callout, cloud puffs=15, aspect=2.5, cloud puff arc=120, shading=ball, color=white]
      {\bf\huge{ATTRIBUTE GRAMMARS!}};
  \end{tikzpicture}
  \end{center}
\end{frame}

\section{Motivation}

\intermission{Motivation}

\begin{frame}
  \frametitle{Utrecht Haskell Compiler}

  \begin{itemize}
  \item Compiler for a complex language
  \item Goal: platform for experimentation with language features
  \end{itemize}

  \begin{itemize}
  \item Architecture: long pipeline of transformations
  \item Each transformation step: analysis + actual transformation
  \item Implemented with (higher-order) attribute grammars
  \end{itemize}

  \begin{itemize}
    \item Computation of attributes in terms of other attributes
      \begin{itemize}
      \item Easy to add new attributes
      \item Automatic ordering of computations
      \item Separate specification
      \end{itemize}
    \item Automatic generation of trivial computations
      \begin{itemize}
      \item Code more robust against changes in the AST structure
      \end{itemize}
      \comment{Would be nice to have a figure about how many percent of the rules are actually copy-rules}
    \item Sanity checks (e.g. cycle check)
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Challenge}
  
  \begin{itemize}
  \item Question: can we stretch AG formalism to cover an even larger part of the code base?
  \item Why: more concise code
  \end{itemize}
  
  Goal:
  \begin{itemize}
  \item Implement unification with AGs
  \item Challenge: AGs unsuitable to express simultaneous traversals over multiple ASTs
  \item Solution: decorate a virtual tree that represents the traversal itself
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Unification with Type Rules}
  
  \begin{mathpar}
    \inferrule*[right=m.con]
      {}
      {|Ty_Con s1 == Ty_Con s1 ^^ & emptyset|}
    
    \inferrule*[right=m.app]
      {|ty1 == ty3 ^^ & e1| \\ |ty2 == ty4 ^^ & e2|}
      {|Ty_App ty1 ty2 == Ty_App ty3 ty4 ^^ & (e1 ++ e2)|}
    
    \inferrule*[right=m.clash]
      {}
      {|ty1 == ty2 ^^ & {Err_UnifyClash}|}
  \end{mathpar}
\end{frame}

\begin{frame}
  \frametitle{Code starts like this: EH1, full unification}
  
  \footnotesize{
  \begin{code}
  fitsIn :: Ty -> Ty -> FIOut
  fitsIn ty1 ty2
    =  f ty1 ty2
    where
              res t                                   = emptyFO {foTy = t}
              f  Ty_Any               t2              = res t2                                -- m.any.l
              f  t1                   Ty_Any          = res t1                                -- m.any.r
              f  t1@(Ty_Con s1)                                                               -- m.con
                 t2@(Ty_Con s2)
                   | s1 == s2                         = res t2
              f  t1@(Ty_App (Ty_App (Ty_Con c1) ta1) tr1)                                     -- m.arrow
                 t2@(Ty_App (Ty_App (Ty_Con c2) ta2) tr2)
                   | hsnIsArrow c1 && c1 == c2
                   = comp ta2 tr1 ta1 tr2 (\a r -> [a] `mkArrow` r)
              f  t1@(Ty_App tf1 ta1)                                                          -- m.prod
                 t2@(Ty_App tf2 ta2)
                   = comp tf1 ta1 tf2 ta2 Ty_App
              f  t1                   t2              = err [Err_UnifyClash ty1 ty2 t1 t2]
              err e                                   = emptyFO {foErrL = e}
              comp tf1 ta1 tf2 ta2 mkComp
                   = foldr1  (\fo1 fo2 -> if foHasErrs fo1 then fo1 else fo2)
                             [ffo,afo,res rt]
                   where  ffo  = f tf1 tf2
                          afo  = f ta1 ta2
                          rt   = mkComp (foTy ffo) (foTy afo)
  \end{code}}
\end{frame}

\begin{frame}
  \frametitle{Before you know it... EH99, zoomed in on app-case}
  
  \scriptsize{
  \begin{code}
  f fi  t1@(Ty_App (Ty_App (Ty_Con c1) tpr1) tr1)
        t2@(Ty_App (Ty_App (Ty_Con c2) tpr2) tr2)
          | hsnIsArrow c1 && c1 == c2 && not (fioPredAsTy (fiFIOpts fi)) && isJust mbfp
      = fromJust mbfp
      where  (u',u1,u2,u3)    = mkNewLevUID3 (fiUniq fi)
             prfPredScope     = fePredScope (fiEnv fi)
             mbfp             = fVarPred2 fP (fi {fiUniq = u'}) tpr1 tpr2
             mberr            = Just (errClash fi t1 t2)
             fP fi tpr1@(Ty_Pred _)              tpr2@(Ty_Pred _)
                  =  if foHasErrs pfo
                     then Nothing
                     else Just  ( foUpdTy ([foTy pfo] `mkArrow` foTy fo)
                                $ foUpdLRCoe (mkIdLRCoeWith n (CMetaVal_Dict Nothing))
                                $ foUpdLRTCoe (C.mkIdLRCoeWith n (C.MetaVal_Dict Nothing) (C.tyErr ("fitsIn.fP.mkIdLRCoeWith.1: " ++ show n)))
                                $ fo)
                  where  pfo   = fVar f (fi {fiFIOpts = predFIOpts}) tpr2 tpr1
                         n     = uidHNm u2
                         fo    = fVar ff (fofi pfo fi) tr1 tr2
             fP fi tpr1@(Ty_Pred pr1)            (Ty_Impls (Impls_Tail iv2 ipo2))
                  =  Just (foUpdImplExplCoe iv2
                                            (Impls_Cons iv2 pr1 (mkPrIdCHR u2) range ipo2 im2)
                                            tpr1
                                            (mkIdLRCoeWith n (CMetaVal_Dict Nothing))
                                            (C.mkIdLRCoeWith n (C.MetaVal_Dict Nothing) (C.tyErr ("fitsIn.fP.mkIdLRCoeWith.2: " ++ show n)))
                                            fo)
                  where  im2   = Impls_Tail u1 ipo2
                         n     = uidHNm u2
                         fo    = fVar ff fi tr1 ([Ty_Impls im2] `mkArrow` tr2)
  \end{code}}
\end{frame}

\begin{frame}
  \frametitle{Could we describe it as...}
  
  \begin{center}
  \footnotesize{
  \begin{mathpar}
    \inferrule*
      { \inferrule*
          {}
          {|Int == Int ^^ & emptyset|}
        \\
        \inferrule*
          {
            \inferrule*
              {}
              {|Bool == Bool ^^ & emptyset|}
            \\
            \inferrule*
              {}
              {|Char == Char ^^ & emptyset|}
          }
          {|Bool -> Char == Bool -> Char ^^ & emptyset|}
      }
      {| Int -> Bool -> Char == Int -> Bool -> Char ^^ & emptyset|}
  \end{mathpar}}
  \end{center}
  \pause
  \begin{itemize}
  \item Dynamic construction of derivation tree
  \item Attribution of derivation tree
  \end{itemize}
\end{frame}

\section{Background}

\intermission{Background}

\begin{frame}
  \frametitle{Attribute Grammars}
  
  \begin{itemize}
  \item Context-free grammar
    \begin{itemize}
    \item Nonterminals
    \item Productions
    \end{itemize}
  \item Attributes
    \begin{itemize}
    \item Parameters of nonterminals
    \item Inherited attributes
    \item Synthesized attributes
    \end{itemize}
  \item Rules
    \begin{itemize}
    \item Equations between attributes per production
    \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Traversing AST}
  
  \begin{itemize}
  \item We use AGs to generate a traversal on an AST
        \comment{and does something useful}
  \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[syn]            (n1syn2) [right of=n1syn1] [label={[rotate=90,xshift=4.5mm,yshift=-2.5mm]above:|errs|}] {};
    
    \node[inh,leftfirst] (n2inh1) [left of=n2] {};
    \node[syn,rightfirst] (n2syn1) [right of=n2] {};
    \node[syn] (n2syn2) [right of=n2syn1] {};
    
    \node[inh,leftfirst] (n3inh1) [left of=n3] {};
    \node[syn,rightfirst] (n3syn1) [right of=n3] {};
    \node[syn] (n3syn2) [right of=n3syn1] {};
    
    \node[inh,leftfirst] (n4inh1) [left of=n4] {};
    \node[syn,rightfirst] (n4syn1) [right of=n4] {};
    \node[syn] (n4syn2) [right of=n4syn1] {};
    
    \node[inh,leftfirst] (n5inh1) [left of=n5] {};
    \node[syn,rightfirst] (n5syn1) [right of=n5] {};
    \node[syn] (n5syn2) [right of=n5syn1 ] {};
    
    \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] (n1syn2) to (n2syn2);
    \draw[arr] (n1syn2) to (n3syn2);
    \draw[arr] (n3syn2) to (n4syn2);
    \draw[arr] (n3syn2) to (n5syn2);
    
    \draw[arr] (n2syn1.south) to [out=-90,in=-90] (n2inh1.south);
    \draw[arr] (n2syn2.south) to [out=-90,in=-90] (n2inh1.south);
    \draw[arr] (n4syn1.south) to [out=-90,in=-90] (n4inh1.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}
  \frametitle{AG Programming Model}
  
  \begin{itemize}
  \item Focus on AST instead of grammar.
  \item AG describes algorithm that decorates AST.
  \comment{decoration = attaching attributes to nodes in the AST}
  \end{itemize}
  
  \begin{code}
  data Expr
    | App  ^^ ^^  fun :: Expr  ^^  arg :: Expr
    | Var  ^^ ^^  nm :: Ident
  \end{code}
  \vspace{-6mm}
  \uncover<2->{
  \begin{code}
  attr Expr  inh  env  :: Env
             syn  ty   :: Ty
  \end{code}}
  \vspace{-6mm}
  \uncover<3->{
  \begin{code}
  sem Expr
    | App  ^^ ^^  fun.env  = this.env
                  arg.env  = this.env
    | Var         this.ty  = lookup loc.nm this.env 
  \end{code}}
  
  \begin{textblock}{7}(7.5,-8.5)
  \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}
    , tr/.style={isosceles triangle,rotate=90, 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=30mm, level distance=15mm]
      child {
        node[tr, xshift=-3mm](n2){|Expr|}
      }
      child {
        node[tr, xshift=-3mm](n3){|Expr|}
      };
    \uncover<2->{
    \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] {};
    }
    
    \uncover<3->{
    \draw[arr] (n2inh1) to (n1inh1);
    \draw[arr] (n3inh1) to (n1inh1);
    }
    
  \end{tikzpicture}
  \end{textblock}
\end{frame}

%if False
\begin{frame}
  \frametitle{AG Program}

  An AG program consists of:

  \begin{itemize}
  \item Declaration of the structure of the AST
  \item Declaration of attributes of the AST
    \begin{itemize}
    \item Each node has three sets of attributes:
          inherited, synthesized, local
    \item Inherited and synthesized attributes can be referred to by the parent
    \comment{Nodes that belong to the same nonterminal have the ``same'' inherited and synthesized attributes.}
    \end{itemize}
  \item Small algorithms for each node:
    \begin{itemize}
    \item We call them ``rules''
    \item Computes the values of attributes based on the values of other attributes
    \item These must define the synthesized attributes of the node itself, and the inherited attributes of the direct children
    \item These may read from the inherited attributes of the node itself, and the synthesized attributes of the direct children
    \end{itemize}
  \end{itemize}
\end{frame}
%endif

\begin{frame}
  \frametitle{Compilation}
  
  \begin{textblock}{7}(2,-4)
  \begin{tikzpicture}
    [ nd/.style={rectangle, minimum size=14mm, very thick, draw=black!50, top color=white, bottom color=black!20}
    , obj/.style={circle, minimum size=10mm, very thick, draw=black!50, top color=white, bottom color=black!20}
    , annot/.style={font=\scriptsize}
    ]
    \node[nd](ag){@.ag@};
    \node[nd,right of=ag, xshift=30mm](hs){@.hs@};
    \draw[->, thick] (ag) to node[auto]{generate} (hs);

    %% \node[obj, right of=hs, xshift=15mm](txt){@text@};
    \node[obj, right of=hs, xshift=15mm](ast){@ast@};
    \node[obj, below of=ast, yshift=-14mm](astattr){@ast+attrs@};
    \node[below of=astattr, yshift=-10mm](dots){\ldots};
    
    %% \draw[->,thick] (txt) to node[auto]{parse} (ast);
    \draw[->,thick] (ast) to node[auto]{decorate} (astattr);
    \draw[->,thick] (astattr) to node[auto](int){inspect} (dots);
    
    \node[rectangle,thick,dotted,draw=black,fit=(ast)(astattr)(dots)(int)](cde){};
    \draw[-,thick,dotted] (hs) to (cde);
    
    \node[annot,above of=ast]{behavior of generated code};
  \end{tikzpicture}
  \end{textblock}

  \begin{itemize}
  \item Automatic generation of trivial rules
  \item Circularity checking
  \item Efficient evaluation order
  \end{itemize}
\end{frame}

%if False
\begin{frame}
  \frametitle{Semantic trees}

  \begin{itemize}
  \item Parser constructs a fixed AST
  \item AG programming model: decorating the AST
  \item Semantic tree: AST that is being decorated
        \begin{itemize}
        \item (extensional) tree data structure with table per node
        \item (intentional) \emph{function} from inherited to synthesized
        \end{itemize}
  \end{itemize}

  \vspace{1em}
  In this talk:
  \begin{itemize}
  \item No AST: the AST as inherited attribute
  \item Dynamically construct the semantic tree
  \item Closely related to HOAGs
    \begin{itemize}
    \item Statically determined, context-dependent types and number of attributes
    \end{itemize}
    \comment{but not the same: contexts}
  \end{itemize}
\end{frame}
%endif

\section{Problem}

\intermission{Problem}

\begin{frame}
  \frametitle{Unification}
  
  \begin{center}
    \begin{tikzpicture}
      [ nd/.style={circle, minimum size=6mm, very thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\scriptsize}
      , match/.style={ultra thick,draw=red!50!black!30}
      ]
    \node[nd](n1){|->|}
      [sibling distance=20mm, level distance=15mm]
      child {
        node[nd](n2){|v1|}
      }
      child {
        [sibling distance=10mm]
        node[nd](n3){|->|}
          child {
            node[nd](n4){|int|}
          }
          child {
            node[nd](n5){|->|}
              child {
                node[nd](n6){|int|}
              }
              child {
                node[nd](n7){|v2|}
              }
          }
      };

    \node[nd](m1) [right of=n1, xshift=48mm] {|->|}
      [sibling distance=20mm,level distance=15mm]
      child {
        [sibling distance=10mm]
        node[nd](m2){|->|}
          child {
            node[nd](m4){|int|}
          }
          child {
            node[nd](m5){|int|}
          }
      }
      child {
        [sibling distance=10mm]
        node[nd](m3){|->|}
          child {
            node[nd](m6){|v1|}
          }
          child {
            node[nd](m7){|v2|}
          }
      };
    
    \pause
    \draw[->,match,out=40,in=140] (n2) to node[auto]{bind} (m2);
    \pause
    \node[nd, at=(m6.center)](m8){|->|}
      [sibling distance=10mm]
      child {
        node[nd](m9){|int|}
      }
      child {
        node[nd](m10){|int|}
      };
      \node[nd, at=(n2.center)](n10){|->|}
        [sibling distance=10mm]
        child {
          node[nd](n11){|int|}
        }
        child {
          node[nd](n12){|int|}
        };
    \draw[->,match,dotted] (m6) to node[auto,swap]{update} (m2);
    \pause
    \draw[match,out=40,in=140] (n4) to node[auto]{match} node[auto,swap]{err: different!} (m6);
    \pause
    \draw[<-,match,out=-90,in=-90] (n5) to node[auto]{bind} node[auto,swap]{err: cyclic!} (m7);
    \end{tikzpicture}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Unification with AGs?}
  
  \begin{itemize}
  \item Unification in UHC has many inputs and outputs:
    type env, variance env, subst, type, errors, context, pred env, ...
  \item ... and a rich type language
  \item Large amount of boilerplate (mostly trivial copying)
  \item Caching, memoization
  \item AGs to the rescue?
    \comment{Integration,Dealing with inputs and outputs}
  \end{itemize}
  \pause
  \vspace{1cm}
  Challenges:
  \begin{itemize}
  \item Simultaneous traversal of two ASTs
  \item ASTs depend on substitution, which changes during the
        computation
  \end{itemize}
\end{frame}

\section{Idea}

\intermission{Idea}

\begin{frame}
  \frametitle{Construct virtual tree representing the traversal}
  
  \begin{itemize}
  \item AG evaluation: we already have a tree, then decorate it
  \item Now: build and decorate the tree at the same time
  \end{itemize}
  
  \begin{center}
  \begin{tikzpicture}
    [ nd/.style={rectangle, minimum size=14mm, very thick, draw=black!50, top color=white, bottom color=black!20}
    , obj/.style={circle, minimum size=10mm, very thick, draw=black!50, top color=white, bottom color=black!20}
    , annot/.style={font=\scriptsize}
    ]
    
    \node[obj](virtual){@virtual+attr@};
    \node[obj, left of=virtual, yshift=30mm](ast1){@ast1@}
      edge[->] node[auto,swap]{consumed} (virtual);
    \node[obj, right of=virtual, yshift=30mm](ast2){@ast2@}
      edge[->] node[auto]{consumed} (virtual);
    \node[annot, right of=virtual, xshift=40mm]{tree representing traversal of @ast1@ and @ast2@};
    
    \node[below of=virtual, yshift=-20mm](dots){$\ldots$};
    \draw[->] (virtual) to node[auto]{inspect} (dots);
  \end{tikzpicture}
\end{center}
\end{frame}

\begin{frame}
  \frametitle{Virtual Constructors: clauses}
  
  \begin{itemize}
  \item Each virtual constructor is a separate function
    \begin{itemize}
    \item Function has access to parameters of parent
    \item Function constructs virtual subtrees
    \item Function may inspect values of attributes
    \item Function may fail
    \end{itemize}
  \item These function make up the \emph{clauses} of the actual function
  \item Evaluation: take the results of the first clause that succeeds
  \end{itemize}
  
  \begin{code}
  unify =  ^^             unify_arrows
           ^^  `mappend`  unify_var
           ^^  `mappend`  unify_const
           ^^  `mappend`  unify_mismatch
  ^^
  unify_arrows    = ...
  unify_var       = ...
  unify_const     = ...
  unify_mismatch  = ...
  \end{code}
\end{frame}

\intermission{Scenario 1: Growing the tree}

\begin{frame}
  \frametitle{Growing the tree}
  
  \begin{tikzpicture}
    [ nd/.style={circle, minimum size=6mm, very thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\scriptsize}
    , match/.style={-,ultra thick,draw=red!50!black!30}
    , attr/.style={rectangle, minimum size=1.5mm, node distance=3.5mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\scriptsize}
    , inh/.style={attr}
    , syn/.style={attr}
    , leftfirst/.style={xshift=-3mm}
    , rightfirst/.style={xshift=3mm}
    , sibling distance=20mm
    , attrlbl/.style={font=\scriptsize,yshift=-10mm}
    , annot/.style={font=\scriptsize,yshift=5mm}
    ]
  
  \node[nd](l1){|->|}
    child {
      node[nd](l2){|int|}
    }
    child {
      node[nd](l3){|v1|}
    };
  
  \node[nd,right of=l1, xshift=70mm](r1){|->|}
    child {
      node[nd](r2){|int|}
    }
    child {
      node[nd](r3){|int|}
    };
   
  \uncover<1>{
    \node[above of=l1,yshift=-3mm]{|input ty1|};
    \node[above of=r1,yshift=-3mm]{|input ty2|};
  }
  \pause
  \node[nd,right of=l1, xshift=30mm](s1){|==|};
  \node[inh,leftfirst,left of=s1](s1t1){};
  \node[inh,left of=s1t1](s1t2){};
  \node[inh,left of=s1t2](s1s){};
  \node[attrlbl,above of=s1t1]{|ty1|};
  \node[attrlbl,above of=s1t2]{|ty2|};
  \node[attrlbl,above of=s1s]{|subst|};
  \uncover<2>{
  \node[above of=s1,yshift=-3mm]{|root|};}
  \pause
  \draw[->,dotted] (s1t1) to [in=135,out=45] (r1);
  \draw[->,dotted] (s1t2) to [in=45,out=135] (l1);
  \node[annot,below of=s1]{|->|};
  \pause
  \node[nd,below of=s1,yshift=-20mm,xshift=-15mm](s2){|==|}
    edge (s1);
  \node[inh,leftfirst,left of=s2](s2t1){};
  \node[inh,left of=s2t1](s2t2){};
  \node[inh,left of=s2t2](s2s){};
  \node[annot,below of=s2]{|const|};
  \pause
  \draw[->,dotted] (s2t1) to [in=-135,out=45] (r2);
  \draw[->,dotted] (s2t2) to [in=-45,out=135] (l2);
  \node[syn,rightfirst,right of=s2](s2s'){};
  \node[attrlbl,above of=s2s']{|subst|};
  \pause
  \node[nd,below of=s1,yshift=-20mm,xshift=15mm](s3){|==|}
    edge (s1);
  \node[inh,leftfirst,left of=s3](s3t1){};
  \node[inh,left of=s3t1](s3t2){};
  \node[inh,left of=s3t2](s3s){};
  \node[annot,below of=s3]{|var|};
  \pause
  \draw[->,thick] (s3s) to [in=90,out=90] (s2s');
  \draw[->,dotted] (s3t1) to [in=-135,out=45] (r3);
  \draw[->,dotted] (s3t2) to [in=-45,out=135] (l3);
  \pause
  \node[nd,below of=s3,yshift=-10mm](ftv){|fv|}
    edge (s3);
  \node[inh,leftfirst,left of=ftv](ftvt){};
  \node[inh,left of=ftvt](ftvs){};
  \pause
  \draw[->,dotted] (ftvt) to [in=-135,out=45] (r3);
  \node[attrlbl,above of=ftvt]{|ty|};
  \node[attrlbl,above of=ftvs]{|subst|};
  \draw[->,thick] (ftvs) to (s3s);
  \node[annot,below of=ftv]{|const|};
  \pause
  \node[syn,rightfirst,right of=ftv](ftvv){};
  \node[attrlbl,above of=ftvv]{$\emptyset$};
  \pause
  \node[syn,rightfirst,right of=s3](s3s'){};
  \node[attrlbl,above of=s3s']{|subst|};
  \node[syn,rightfirst,right of=s1](s1s'){};
  \draw[->,thick] (s1s') to (s3s');
  \end{tikzpicture}
\end{frame}

\intermission{Scenario 2: Context dependent attribution}

\begin{frame}
  \frametitle{Context dependent attribution}
  
  \begin{tikzpicture}
    [ nd/.style={circle, minimum size=6mm, very thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\scriptsize}
    , ndx/.style={circle, minimum size=6mm, very thick, draw=red!50!black!50, top color=white, bottom color=red!50!black!20,font=\scriptsize}
    , match/.style={-,ultra thick,draw=red!50!black!30}
    , attr/.style={rectangle, minimum size=1.5mm, node distance=3.5mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\scriptsize}
    , inh/.style={attr}
    , syn/.style={attr}
    , leftfirst/.style={xshift=-3mm}
    , rightfirst/.style={xshift=3mm}
    , sibling distance=20mm
    , attrlbl/.style={font=\scriptsize,yshift=-10mm}
    ]
  
  \node[nd](l1){|->|}
    child {
      node[nd](l2){|int|}
    }
    child {
      node[nd](l3){|int|}
    };
  
  \node[nd,right of=l1, xshift=70mm](r1){|->|}
    child {
      node[nd](r2){|bool|}
    }
    child {
      node[nd](r3){|int|}
    };
  \pause
  \node[nd,right of=l1, xshift=30mm](s1){|==|};
  \node[inh,leftfirst,left of=s1](s1t1){};
  \node[inh,left of=s1t1](s1t2){};
  \node[inh,left of=s1t2](s1s){};
  \node[attrlbl,above of=s1t1]{|ty1|};
  \node[attrlbl,above of=s1t2]{|ty2|};
  \node[attrlbl,above of=s1s]{|subst|};
  \draw[->,dotted] (s1t1) to [in=135,out=45] (r1);
  \draw[->,dotted] (s1t2) to [in=45,out=135] (l1);
  \pause
  \node[nd,below of=s1,yshift=-20mm,xshift=-15mm](s2){|==|}
    edge (s1);
  \node[inh,leftfirst,left of=s2](s2t1){};
  \node[inh,left of=s2t1](s2t2){};
  \node[inh,left of=s2t2](s2s){};
  \draw[->,dotted] (s2t1) to [in=-135,out=45] (r2);
  \draw[->,dotted] (s2t2) to [in=-45,out=135] (l2);
  \pause
  \node[ndx,at=(s2)] {X};
  \pause
  \node[syn,rightfirst,right of=s2](s2e){};
  \node[attrlbl,above of=s2e]{|e|};
  \node[below of=s2e]{errors instead of an improved substitution};
  \end{tikzpicture}
\end{frame}




%if False

\begin{frame}
  \frametitle{Problem: traverse multiple ASTs}
  
  \begin{itemize}
  \item Example: unification
  \item Traverse common spine
  \end{itemize}
  
  \begin{center}
  %% Visualize a traversal over multiple trees
  \begin{tikzpicture}
    [ nd/.style={circle, minimum size=6mm, very thick, draw=blue!50!black!50, top color=white, bottom color=blue!50!black!20,font=\scriptsize}
    , attr/.style={rectangle, minimum size=1.5mm, node distance=3.5mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\scriptsize}
    , inh/.style={attr}
    , syn/.style={attr}
    , leftfirst/.style={xshift=-3mm}
    , rightfirst/.style={xshift=3mm}
    , arr/.style={->,dashed}
    ]
  \node[nd](n1){|->|}
    [sibling distance=10mm, level distance=15mm]
    child {
      node[nd](n2){|v1|}
    }
    child {
      node[nd](n3){|->|}
        child {
          node[nd](n4){|int|}
        }
        child {
          node[nd](n5){|->|}
            child {
              node[nd](n6){|int|}
            }
            child {
              node[nd](n7){|int|}
            }
        }
    };
  
  \node[nd](k1) [right of=n1, xshift=23mm] {|arr|}
    [sibling distance=23mm, level distance=15mm]
    child {
      node[nd](k2){|var|}
    }
    child {
      node[nd](k3){|arr|}
        child {
          node[nd](k4){|cst|}
        }
        child {
          node[nd](k5){|var|}
        }
    };
  
  \node[nd](m1) [right of=k1, xshift=48mm] {|->|}
    [sibling distance=20mm,level distance=15mm]
    child {
      [sibling distance=10mm]
      node[nd](m2){|->|}
        child {
          node[nd](m4){|int|}
        }
        child {
          node[nd](m5){|int|}
        }
    }
    child {
      [sibling distance=10mm]
      node[nd](m3){|->|}
        child {
          node[nd](m6){|bool|}
        }
        child {
          node[nd](m7){|v2|}
        }
    };
  
    \node[inh,leftfirst]  (k1inh1) [left of=k1]      [label={[rotate=90,xshift=5mm,yshift=-2.5mm]above:|subst|}] {};
    \node[syn,rightfirst] (k1syn1) [right of=k1]     [label={[rotate=90,xshift=4mm,yshift=-2.5mm]above:|errs|}] {};
    \node[syn]            (k1syn2) [right of=k1syn1] [label={[rotate=90,xshift=5mm,yshift=-2.5mm]above:|subst|}] {};
    
    \node[inh,leftfirst]  (k2inh1) [left of=k2]      {};
    \node[syn,rightfirst] (k2syn1) [right of=k2]     {};
    \node[syn]            (k2syn2) [right of=k2syn1] {};
    
    \node[inh,leftfirst]  (k3inh1) [left of=k3]      {};
    \node[syn,rightfirst] (k3syn1) [right of=k3]     {};
    \node[syn]            (k3syn2) [right of=k3syn1] {};
    
    \node[inh,leftfirst]  (k4inh1) [left of=k4]      {};
    \node[syn,rightfirst] (k4syn1) [right of=k4]     {};
    \node[syn]            (k4syn2) [right of=k4syn1] {};
    
    \node[inh,leftfirst]  (k5inh1) [left of=k5]      {};
    \node[syn,rightfirst] (k5syn1) [right of=k5]     {};
    \node[syn]            (k5syn2) [right of=k5syn1] {};
    
    \draw[arr] (k2syn2.south) to [out=-90,in=-90] (k2inh1.south);
    \draw[arr] (k4syn2.south) to [out=-90,in=-90] (k4inh1.south);
    \draw[arr] (k5syn2.south) to [out=-90,in=-90] (k5inh1.south);
    \draw[arr] (k2syn2.north) to [out=90,in=90]   (k3inh1.north);
    \draw[arr] (k4syn2.north) to [out=90,in=90]   (k5inh1.north);
    \draw[arr] (k2inh1)       to                  (k1inh1);
    \draw[arr] (k4inh1)       to                  (k3inh1);
    \draw[arr] (k5syn2)       to                  (k3syn2);
    \draw[arr] (k3syn2)       to                  (k1syn2);
  \end{tikzpicture}
  
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Solution: compute semantic trees}
  
  \begin{itemize}
  \item \emph{Compute} an attributed tree that represents the \emph{derivation} of unification
  \item Unification is a relation defined by one or more \emph{clauses}
  \item Actual ASTs are inherited attributes
  \item Define an \emph{interface}, define \emph{clauses}
  \end{itemize}
  
  \begin{center}
  %% non-terminal picture
  \begin{tikzpicture}
    [ nd/.style={circle, minimum size=10mm, 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}
    , inh2/.style={attr,node distance=7mm}
    , syn/.style={attr}
    , leftfirst/.style={xshift=-4mm}
    , rightfirst/.style={xshift=4mm}
    , arr/.style={->,dashed}
    , visit/.style={-,solid,ultra thick,blue!70!black!20}
    ]
    \node[nd](n1){|==|};
    \node[inh,leftfirst]  (n1inh3) [left of=n1]      [label={[rotate=90,xshift=4mm,yshift=-2.5mm]above:|inhs|}] {};
    \node[inh]            (n1inh2) [left of=n1inh3]  [label={[rotate=90,xshift=4mm,yshift=-2.5mm]above:|ast2|}] {};
    \node[inh]            (n1inh1) [left of=n1inh2]  [label={[rotate=90,xshift=4mm,yshift=-2.5mm]above:|ast1|}] {};
    \node[syn,rightfirst] (n1syn1) [right of=n1]     [label={[rotate=90,xshift=4mm,yshift=-2.5mm]above:|syns|}] {};
    
    \draw[visit] (n1inh1.south west) to [out=-90,in=-90] node[yshift=-2mm]{visit 1} (n1inh2.south east);
    \draw[visit] (n1inh3.south west) to [out=-90,in=-90] node[yshift=2mm]{visit 2} (n1syn1.south east);
    
    \node[nd, right of=n1, xshift=50mm](k1){|==|}
      [sibling distance=45mm,level distance=15mm]
      child {
        node[nd](k2){|==|}
      }
      child {
        node[nd](k3){|==|}
      };
  
    \node[inh2,leftfirst]  (k1inh1) [left of=k1]      {|inh|};
    \node[inh2,left]       (k1inh2) [left of=k1inh1,xshift=-5mm]  {|c -> d|};
    \node[inh2,left]       (k1inh3) [left of=k1inh2,xshift=-5mm]  {|a -> b|};
    
    \node[inh2,leftfirst]  (k2inh1) [left of=k2]      {|inh|};
    \node[inh2,left]       (k2inh2) [left of=k2inh1]  {|c|};
    \node[inh2,left]       (k2inh3) [left of=k2inh2]  {|a|};
    
    \node[inh2,leftfirst]  (k3inh1) [left of=k3]      {|inh|};
    \node[inh2,left]       (k3inh2) [left of=k3inh1]  {|d|};
    \node[inh2,left]       (k3inh3) [left of=k3inh2]  {|b|};
    
    \node[above of=n1,yshift=5mm](itflabel){interface};
    \node[right of=itflabel,xshift=40mm]{clause};

  \end{tikzpicture}
  \end{center}
\end{frame}

\section{Solution}

\intermission{Solution}

\begin{frame}
  \frametitle{Problem + Idea, revisited}
  
  \begin{itemize}
  \item AGs describe an algorithmic semantics for a \emph{relation}, i.e. typing relation
  \item Parameters of the relation: inherited atributes + 1 AST + synthesized attributes
  \end{itemize}
  
  \begin{itemize}
  \item Goal: deal with relations between multiple ASTs
  \end{itemize}
  
  \begin{itemize}
  \item Idea: \emph{Compute} semantic trees
  \item \comment{How do we compute it?}
        Compute the semantic tree in multiple visits, such that we can use results
        computed in a previous visit to structure the semantic tree.
        \begin{itemize}
        \item For unification: choose clauses based on both the two type ASTs and the
              latest substitution
        \comment{(In this paper) We restricted ourselves to a linear sequence of visits}
        \end{itemize}
  \item For each visit, clause: compute attributes, define children, visit children
  \end{itemize}
\end{frame}


\begin{frame}
  \frametitle{Closer investigation: visit functions}
  
  AG Compiler:
  \begin{itemize}
  \item Analysis of AG code: \emph{plan}
  \item Compilation of a plan to \emph{visit functions}
  \end{itemize}
  
  Plan:
  \begin{itemize}
  \item For each nonterminal: divide the computation of attributes over a linear sequence of visits
  \item For each production: sequence of computation step for each visit
    \begin{itemize}
    \item compute an attribute
    \item visit a child
    \end{itemize}
  \end{itemize}
  
  Visit functions:
  \begin{itemize}
  \item Function that takes some inherited attributes, finds a matching clause,
        computes some synthesized attributes and a continuation
        visit-function for the remainder of the visits.
        \comment{the computed continuation is a closure that remembers all the results that have been computed
          in a previous visit.}
  \end{itemize}
\end{frame}
%endif

\section{Implementation}

\intermission{Some Aspects of the Implementation}

\begin{frame}
  \frametitle{Simplification}
  
  \begin{itemize}
  \item Assumption: simplified context dependent attribution
  \item Success and failure contexts only
  \item No values for synthesized attributes upon failure
  \item A visit to a subtree must result into success otherwise the clause fails
  \item Selection of clauses: pick the first one that succeeds
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Attributed Trees as Functions of Attributes - type}
  
  \begin{code}
  itf Unify
    inh  ty1   :: Ty
    inh  ty2   :: Ty
    inh  subst :: Subst
    syn  subst :: Subst
    syn  errs  :: Errs
  \end{code}
  \pause
  \begin{code}
  type I_Unify = Ty -> Ty -> Subst -> Maybe (Subst, Errs)
  \end{code}
\end{frame}
  
\begin{frame}
  \frametitle{Attributed Trees as Functions of Attributes - body}
  
  \begin{code}
  unify :: I_Unify
  unify = unify_arr `mappend` ...
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Attributed Trees as Functions of Attributes - clauses}

  \begin{code}
  unify_arr
    =  ^^ sem :: Unify
       ^^ ^^  match (Ty_Arr loc.a loc.b) = this.ty1
              match (Ty_Arr loc.c loc.d) = this.ty2
              child left : Unify = unify
              left.ty1 = loc.a
              left.ty2 = loc.b
              this.errs = left.errs ++ right.errs
  \end{code}
  \pause
  \small{
  \begin{code}
  unify_arr ty1 ty2 inSubst =
      case ty1 of        ^^  case ty2 of
        (Ty_Arr a b)     ^^    (Ty_Arr c d)
      
      (subst1, errs1) = unify a c
      (subst2, errs2) = unify b d
          
      outSubst = ... inSubst
      outErrs  = ...

      -> Just (outSubst, outErrs)
      -> Nothing
  \end{code}}
\end{frame}

\begin{frame}
  \frametitle{Pattern Matching and Evaluation Order}
  
  \begin{code}
  unify_arr ty1 ty2 inSubst =
    case ty1 of
      (Ty_Arr a b)
    case ty2 of
      (Ty_Arr c d)
  \end{code}
  
  \begin{itemize}
  \item Clause selection based on pattern matches on attributes
  \item The order of the pattern matches influences (lazy) evaluation
  \item Dependency analysis
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Multi-visit}
  
  Scenario:
  \begin{itemize}
  \item Select a clause based on some inherited attributes, i.e. the var-clause for unification
  \item Compute some attributes, i.e. free variables
  \item Refine clause selection based on other attributes, i.e. occur-check
  \item Compute more attributes, i.e. errors on failure, new substitution on success
  \end{itemize}
  
  Or variations on this theme
\end{frame}

\begin{frame}
  \frametitle{Implementation based on Visit Functions}
  
  A visit function is:
  \begin{itemize}
  \item   Function that takes some inherited attributes, finds a matching clause,
          computes some synthesized attributes and a continuation
          visit-function for the remainder of the visits.
          \comment{the computed continuation is a closure that remembers all the results that have been computed
            in a previous visit.}
  \item Originally intended as functional backend for AGs
  \end{itemize}
  
  \begin{itemize}
  \item Consider the ASTs as additional inherited attributes
  \item Visit function pattern matches on inherited attribute to find a clause
  \item Call recursively, etc. to visit children
  \end{itemize}
  
  \begin{itemize}
  \item We need a front-end for visit functions!
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Front-end}
  
  \begin{code}
  itf Check                      ^^^    itf Analyze
  ^^  inh   ty1, ty2  :: Ty      ^^^    ^^  inh  finalSubst :: Subst
  ^^  syn   subst     :: Subst   ^^^    ^^  syn  errs :: Ty
  ^^  tail :: Analyze

  unify =  sem :: Check
             match (Arr a b) = this.ty1
             match (Arr c d) = this.ty2
             
             child left = unify  ^^^  visit left : Check
             left.ty1 = a             left.ty2 = c
             
             this.subst = left.subst `union` right.subst
             
             tail sem :: Analyze
                    visit left : Analyze
                    left.finalSubst = this.finalSubst
                    this.errs = left.errs ++ right.errs
        `mappend` sem :: Check ...
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Comparison to AGs}
  
  Similar:
  \begin{itemize}
  \item Model with attributes and rules
  \item Conveniences: trivial rule insertion, sanity checks, AG optimizations
  \end{itemize}
  
  \vspace{1cm}
  
  To be done explicitly what you get normally for free with AGs:
  \begin{itemize}
  \item Manually select clauses
  \item Partition attributes over multiple visits
  \item Explicitly indicate what function to use for the children 
  \end{itemize}
  
  \vspace{1em}
  
  The usual dependency analysis for AGs can be used to augment a partial specification
  of visit function to a full specification.
\end{frame}


%if False

\begin{frame}
  \frametitle{Super! However...}
  
  Consider unification.
  
  \begin{code}
  data Ty  | Con  String 
           | Arr  Ty Ty
  
  unify :: Ty -> Ty -> Subst
  unify (Con nm1) (Con nm2)
    | nm1 == nm2 = emptysubst
  unify (Arr t1 t2) (Arr t3 t4)
    = unify t1 t3 `union` unify t2 t4
  unify _ _ = error "unification failure"
  \end{code}
  
  \begin{itemize}
  \item In practice: very complex recursive function
  \comment{subsitution, errors, compilation flags, context-information}
  \item Can we describe this function with an AG?
  \item No: traverses two ASTs at the same time
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Why would we?}
  
  The traversal over the type ASTs behaves as an attribute grammar.
  Environment information is passed top-down
  A substitution is computed bottom-up
  
  In Haskell, unification functions are typically written with
  reader/writer/state monads.
  ``But this is ugly''
  However, we know that these resemble AGs.
\end{frame}

\begin{frame}
  %% Simple representation of attribute grammars
  %% AG = fold (catamorphism) + algebra
  %% fold is generated
  %%
  %% We change this to: explicit description of fold
  %%   but in terms of not only the AST but also attributes!
\end{frame}

%endif

\section{Conclusion}

\begin{frame}
  \frametitle{Current Work}
  
  \begin{itemize}
  \item Fun with Higher-Order Attribute Grammars
    \begin{code}
    data Tree ...
    data View ...
    sem Tree
      | Node  inst.view : T_View
              inst.view = sem_View_Node' (...)
              
              inst.inh = ...
              ... = inst.syn
    \end{code}
  \item Nested Attribute Grammars
    \begin{code}
    sem Tree
      | Node  lhs.view =  sem View 
                            -- own inh/syn attrs
                            -- + attrs of outer sem
              -- own attrs + attrs of view
    \end{code}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Conclusion}

  \begin{itemize}
  \item Problem: AGs not suitable for traversals over multiple ASTs
  \item Solution: decorate a virtual tree that represents the traversal itself
  \end{itemize}
  
  Use AGs for the implementation of:
  \begin{itemize}
  \item Type rules that are not syntax directed (but e.g. type directed)
  \item Bi-directional type rules
  \item Search algorithms with attributed search trees
  \item Constraint solving
  \item Actually, any Haskell function
  \end{itemize}

%if False
  \begin{itemize}
  \item Visit functions specify:
    \begin{itemize}
    \item Statically: structure of a multi-visit tree representation of a traversal
      \comment{typically resembles the structure of the AST or a tupling of ASTs}
      \comment{extra: allows us to change the traversal based on attributes of an earlier traversal}
      \comment{extra: allows us to establish invariants on the order of evaluation}
    \item Algorithmically: how to traverse the ASTs, based on
      the structure of the ASTs
      \comment{go left here, go right there}
      \comment{compare these two two values, etc.}
    \item Declaratively: attributes of the traversal based on
      other attributes.
    \end{itemize}
  \end{itemize}
%endif
  
  \begin{itemize}
  \item Intended to improve the code of the UHC type checker
  \item Implemented as a preprocessor for Haskell
  \item UHC project: @http://www.cs.uu.nl/~ariem/@
  \end{itemize}
\end{frame}

\end{document}