\documentclass{beamer}

%include lhs2TeX.fmt
%include polycode.fmt

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

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

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

\author{Arie Middelkoop}
\title{Iterative Type Inferencing with 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{GPCE '10}

%format :- = "\vdash{}"
%format epsilon = "\epsilon{}"
%format . = "."
%format ^^^^ = "\hspace{6mm}"
%format ^^^ = "\hspace{3mm}"
%format (emph (x)) = "\emph{" x "}"
%format pause = "\pause{}"
%format (many (x)) = "\overline{" x "}"

%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 t1
%format t2
%format t3
%format t4
%format C1
%format C2
%format C3

\newcommand\kw[1]{\ensuremath{\mathbf{#1}}}

\begin{document}

\frontmatter

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

\mainmatter

\begin{frame}
  \frametitle{Software Engineering}

  \begin{itemize}
  \item Research: Abstract over \emph{patterns} in Attribute Grammar (\emph{AG})
        descriptions of \emph{type inference algorithms}
  \item Patterns related to \emph{Choice}   % relations vs functions
  \item \emph{Iteration} in a \emph{multi-visit AG}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Attribute Grammar: Functions on Attributes}
  
  \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=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);
    
    \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);
    
    \pause
    
    \draw[arr] (n2syn1.south) to [out=-90,in=-90] (n2inh1.south);
    \draw[arr] (n4syn1.south) to [out=-90,in=-90] (n4inh1.south);
    \draw[arr] (n2syn2.south) to [out=-90,in=-90] (n2inh1.south);
    \draw[arr] (n4syn2.south) to [out=-90,in=-90] (n4inh1.south);
    \draw[arr] (n5syn1.south) to [out=-90,in=-90] (n5inh1.south);
    \draw[arr] (n5syn2.south) to [out=-90,in=-90] (n5inh1.south);
  \end{tikzpicture}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{AG Properties}
  
  \begin{itemize}
  \item Evaluation order unspecified: derived automatically
        \begin{itemize}
        \item Attribute functions may be written in \emph{arbitrary order}
        \item \emph{Composition} via concatenation
        \end{itemize}
  \item \emph{Visits} implicit
        \begin{itemize}
        \item Sometimes advantagous to have these explicit
        \end{itemize}
  \item Code completion patterns
        \begin{itemize}
        \item Insert \emph{trivial missing functions} for attributes
        \item Offers abstractions similar to reader/write/state monads,
              without affecting evaluation order
        \end{itemize}
  \item Static guarantees
  \end{itemize}
  
\end{frame}

\begin{frame}
  \frametitle{Rationale for Multi-visit AGs}
  
  \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=\footnotesize}
    , attr/.style={rectangle, minimum size=1mm, node distance=4mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\footnotesize}
    , inh/.style={attr}
    , syn/.style={attr}
    , syn1/.style={syn, xshift=1mm}
    , syn2/.style={syn, xshift=4mm}
    , syn3/.style={syn, xshift=1mm, yshift=-3mm}
    , arr/.style={->,dashed, very thick}
    ]
    
    \node[nd](n1){}
      [sibling distance=14mm, level distance=12mm]
      child {
        node[nd](n2){}
      }
      child {
        node[nd](n3){}
          child {
            node[nd](n4){}
          }
          child {
            node[nd](n5){}
          }
      };
    \node[above of=n1]{Name Analysis};
    
    \node[nd, right of=n1, xshift=22mm](m1){}
      [sibling distance=14mm, level distance=12mm]
      child {
        node[nd](m2){}
      }
      child {
        node[nd](m3){}
          child {
            node[nd](m4){}
              child {
                node[nd](m6){}
              }
              child {
                node[nd](m7){}
              }
          }
          child {
            node[nd](m5){}
          }
      };
    \node[above of=m1]{Type Inference};

    \node[nd, right of=m1, xshift=22mm](k1){}
      [sibling distance=14mm, level distance=12mm]
      child {
        node[nd](k2){}
      }
      child {
        node[nd](k3){}
          child {
            node[nd](k4){}
              child {
                node[nd](k6){}
              }
              child {
                node[nd](k7){}
              }
          }
          child {
            node[nd](k5){}
          }
      };
    \node[above of=k1]{Code Generation};
    
    %% Add attributes
    \node[syn1, right of=n1]{};
    \node[syn1, right of=n2]{};
    \node[syn1, right of=n3]{};
    \node[syn1, right of=n4]{};
    \node[syn1, right of=n5]{};
    
    \node[syn1, right of=m1]{};
    \node[syn1, right of=m2]{};
    \node[syn1, right of=m3]{};
    \node[syn1, right of=m4]{};
    \node[syn1, right of=m5]{};
    \node[syn2, right of=m1]{};
    \node[syn2, right of=m2]{};
    \node[syn2, right of=m3]{};
    \node[syn2, right of=m4]{};
    \node[syn2, right of=m5]{};
    \node[syn1, right of=m6]{};
    \node[syn1, right of=m7]{};
    
    \node[syn1, right of=k1]{};
    \node[syn1, right of=k2]{};
    \node[syn1, right of=k3]{};
    \node[syn1, right of=k4]{};
    \node[syn1, right of=k5]{};
    \node[syn3, right of=k1]{};
    \node[syn3, right of=k2]{};
    \node[syn3, right of=k3]{};
    \node[syn3, right of=k4]{};
    \node[syn3, right of=k5]{};
    \node[syn2, right of=k1]{};
    \node[syn2, right of=k2]{};
    \node[syn2, right of=k3]{};
    \node[syn2, right of=k4]{};
    \node[syn2, right of=k5]{};
    \node[syn1, right of=k6]{};
    \node[syn1, right of=k7]{};
    \node[syn2, right of=k6]{};
    \node[syn2, right of=k7]{};

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

\begin{frame}
  \frametitle{Fit The Pieces Together}
  
  \begin{center}
  \begin{tikzpicture}
    [ attr/.style={rectangle, minimum size=1mm, node distance=4mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\footnotesize}
    , attr1/.style={attr,xshift=1mm}
    , attr2/.style={attr,xshift=4mm}
    , attr3/.style={attr,xshift=7mm}
    , attr4/.style={attr,xshift=10mm}
    , attr5/.style={attr,xshift=13mm}
    , attr6/.style={attr,xshift=16mm}
    , attr7/.style={attr,xshift=19mm}
    , attr8/.style={attr,xshift=22mm}
    , attr9/.style={attr,xshift=25mm}
    , attr10/.style={attr,xshift=28mm}
    , attr11/.style={attr,xshift=31mm}
    , attr12/.style={attr,xshift=34mm}
    ]
    
    %% row1
    \node[](ref){};
    \node[left of=ref,attr1]{};
    \node[left of=ref,attr2]{};
    \node[left of=ref,attr3]{};
    \node[left of=ref,attr4]{};
    \node[left of=ref,attr5]{};
    \node[left of=ref,attr6]{};
    \node[left of=ref,attr7]{};
    \node[left of=ref,attr8]{};
    \node[left of=ref,attr9]{};
    %% \node[left of=ref,attr10]{};
    %% \node[left of=ref,attr11]{};
    \node[left of=ref,attr12]{};
    
    \node[yshift=3mm,left of=ref,attr1]{};
    \node[yshift=3mm,left of=ref,attr2]{};
    \node[yshift=3mm,left of=ref,attr3]{};
    \node[yshift=3mm,left of=ref,attr4]{};
    \node[yshift=3mm,left of=ref,attr5]{};
    \node[yshift=3mm,left of=ref,attr6]{};
    \node[yshift=3mm,left of=ref,attr7]{};
    \node[yshift=3mm,left of=ref,attr8]{};
    \node[yshift=3mm,left of=ref,attr9]{};
    %% \node[yshift=3mm,left of=ref,attr10]{};
    %% \node[yshift=3mm,left of=ref,attr11]{};
    \node[yshift=3mm,left of=ref,attr12]{};
    
    \node[yshift=6mm,left of=ref,attr1]{};
    \node[yshift=6mm,left of=ref,attr2]{};
    \node[yshift=6mm,left of=ref,attr3]{};
    \node[yshift=6mm,left of=ref,attr4]{};
    \node[yshift=6mm,left of=ref,attr5]{};
    \node[yshift=6mm,left of=ref,attr6]{};
    \node[yshift=6mm,left of=ref,attr7]{};
    \node[yshift=6mm,left of=ref,attr8]{};
    \node[yshift=6mm,left of=ref,attr9]{};
    %% \node[yshift=6mm,left of=ref,attr10]{};
    %% \node[yshift=6mm,left of=ref,attr11]{};
    \node[yshift=6mm,left of=ref,attr12]{};
    
    \node[yshift=9mm,left of=ref,attr1]{};
    \node[yshift=9mm,left of=ref,attr2]{};
    \node[yshift=9mm,left of=ref,attr3]{};
    \node[yshift=9mm,left of=ref,attr4]{};
    \node[yshift=9mm,left of=ref,attr5]{};
    \node[yshift=9mm,left of=ref,attr6]{};
    \node[yshift=9mm,left of=ref,attr7]{};
    \node[yshift=9mm,left of=ref,attr8]{};
    \node[yshift=9mm,left of=ref,attr9]{};
    %% \node[yshift=9mm,left of=ref,attr10]{};
    %% \node[yshift=9mm,left of=ref,attr11]{};
    \node[yshift=9mm,left of=ref,attr12]{};
    
    \node[xshift=25mm,yshift=20mm,attr]{};
    \node[xshift=28mm,yshift=20mm,attr]{};
    \node[xshift=28mm,yshift=23mm,attr]{};
    \node[xshift=28mm,yshift=26mm,attr]{};
  \end{tikzpicture}
  \end{center}
\end{frame}

\begin{frame}
  \frametitle{Type Rules to AG}
  
  \begin{code}
  g :- e : t        -- expression type rules
  t1 <= t2          -- subtyping rules
  \end{code}
  
  \begin{code}
    itf E   inh g : Env, e : Expr
            syn t : Type
    itf U   inh l : Type, r : Type
  \end{code}
  \pause
  \begin{code}
  data Expr = VarE String | AppE Expr Expr
  data Type = Arr Type Type | Con String
  type Env  = Map String Type
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Choice Issue}
  
  \begin{mathpar}
    \inferrule*[right=Var]
      { |(x,t) `elem` g| }
      { |g :- x : t| }
  \end{mathpar}
  \begin{code}
  Var :   E    ->  epsilon     ^^^^  (VarE x) = lhs.e
          lhs                        lhs.t = lookup x lhs.g
  \end{code}
  \pause
  \begin{mathpar}
    \inferrule*[right=App]
      { |g :- f : tf | \\
        |g :- a : ta | \\ 
        |g :- tf <= (ta -> s)| \\
      }
      { |g :- f a : s| }
  \end{mathpar}
  \begin{code}
  App :  E    ->    E  ^^^  E  ^^^  U   ^^^^  (AppE f.e a.e) = lhs.e
         lhs  ^^^   f       a       u         f.g = lhs.g,  ^^^ a.g = lhs.g
                                              u.l = f.t,    ^^^ u.r = a.t `Arr` (emph s)
                                              lhs.t = s
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Potential Consequences of Choice}
  
  \begin{mathpar}
    \inferrule*[right=Refl]
      {}
      { |t <= t| }
  \end{mathpar}
  \begin{code}
  Refl :  U    ->  epsilon   ^^^^  lhs.l (emph(==)) lhs.r
          lhs
  \end{code}
  \pause
  \begin{mathpar}
    \inferrule*[right=Arr]
      { |t3 <= t1| \\
        |t2 <= t4|
      }
      { |(t1 -> t2) <= (t3 -> t4)| }
  \end{mathpar}
  \begin{code}
  Arr :  U    ->  U  ^^^  U  ^^^^  (emph (Arr q.l p.l))  = lhs.l
         lhs      p       q        (emph (Arr p.r q.r))  = lhs.r
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Choice: What Type To Choose?}
  
  Two strategies to \emph{guess} a type:
  \begin{itemize}
  \item Active: try all possibilties, backtrack if this does not work out later
        \begin{itemize}
        \item Infrequently employed in inference algorithms
        \item Reasons: efficiency, error messages, principal typing
        \end{itemize}
  \item Passive: fill in a place holder, delay the choice until the value
        is fixed later by unifications
        \begin{itemize}
        \item Placeholders for inhs attrs used as syns,
              unification for syn attrs treated as inhs
        \item Employed by all unification-based algorithms
        \item Delayed judgments: encoded as \emph{constraints}
        \item \emph{Iteratively}: fixpoint iteration
        \item \emph{Defaulting:} By absence of any demands on the place holder, actively assign a \emph{default} value
        \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{The Curse of Constraints}
  
  \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=\footnotesize}
    , attr/.style={rectangle, minimum size=1mm, node distance=4mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\footnotesize}
    , inh/.style={attr}
    , syn/.style={attr}
    , syn1/.style={syn, xshift=1mm}
    , syn2/.style={syn, xshift=4mm}
    , syn3/.style={syn, xshift=1mm, yshift=-3mm}
    , arr/.style={->,dashed, very thick}
    ]
    
    \node[nd](n1){}
      [sibling distance=14mm, level distance=8mm]
      child {
        node[nd](n2){}
      }
      child {
        node[nd](n3){}
          child {
            node[nd](n4){}
          }
          child {
            node[nd](n5){}
          }
      };
    \node[above of=n1]{Fat tree};
    
    \node[right of=n1, xshift=30mm](m1){|[ C1, C2, ... ]|};
    \node[above of=m1]{Flat set of constraints};

    \node[syn1, right of=n1]{};
    \node[syn1, right of=n2]{};
    \node[syn1, right of=n3]{};
    \node[syn1, right of=n4]{};
    \node[syn1, right of=n5]{};
    
    \node[right of=n1, xshift=-2mm](x){};
    \draw[arr] (x) to [out=-40,in=-150] (m1);
    \draw[arr] (m1) to [out=150,in=40] (x);
  \end{tikzpicture}
  \end{center}
  \begin{itemize}
  \item Advantage: constraints are first-class values, and can for example
             occur in types.

  \item Decoupling of judgments requires bidirectional transport of information:
        \begin{itemize}
        \item context-information for error messages
        \item constructed proofs e.g. needed for code gen
        \end{itemize}
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{AG-only solution}
  
  Goal:
  \begin{itemize}
  \item Delayable judgements
  \item Fixpoint iteration
  \end{itemize}
  
  Non-solution:
  \begin{itemize}
  \item Encode substitution as cyclic attributes?
  \item Defaulting is a \emph{side-effectful} operation
  \item lack of control where to iterate
  \end{itemize}
  
  Proposed solution:
  \begin{itemize}
  \item Explicitly iterate \emph{visits}
  \item Detachable visits
  \item Visit-local attributes
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{AG With Explicit Visits}
  
  \begin{code}
  itf Infer
    visit Analyze
      inh e      : Expr
      inh g      : Env
      syn errs1  : Errs
    visit Process
      inh subst  : Subst
      syn subst  : Subst
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Notation For Rules}
  
  \begin{code}
  -- rules
  r  ::=  p = e              -- conventional AG-rule
     |    match p = e        -- backtracking variation
     |    child c : I = e    -- (higher-order) child
  \end{code}
  \begin{code}
  e  -- right-hand side
  c  -- child name
  I  -- interface name
  \end{code}

  \begin{code}
  -- patterns
  p  ::=  c.x                -- attribute reference
     |    C (many p)         -- constructor match
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Notation For Productions}
  
  \begin{code}
  nonterm_Expr :: Sem Infer
  nonterm_Expr =
    sem : Infer
      clause e.var
        match (Expr_Var loc.x) = lhs.e
        ...
      clause e.app
        match (Expr_App loc.fe loc.ae) = lhs.e
        child f : Infer = nonterm_Expr
        child a : Infer = nonterm_Expr
        f.e  = loc.fe
        a.e  = loc.ae
        ...
  \end{code}
  %% Automatic ordering of rules
\end{frame}

\begin{frame}
  \frametitle{Explicit Invocation}
  
  \begin{code}
  invoke x of c   -- execute visit |x| of child |c|
  \end{code}
  
  \begin{code}
  clause e.app
    ...
    f.g = lhs.g
    a.g = lhs.g
    invoke infer of f
    invoke infer of a
  \end{code}
  
  %% Normally inferred automatically
\end{frame}

\begin{frame}
  \frametitle{Iterated Invoctation}
  
  \begin{code}
  invoke infer of a = repeat
  \end{code}
  
  \begin{code}
  repeat :: CoSem Expr Process
  repeat =
    cosem : Expr Process
      clause e.repeat
        match True = isChanged lhs.subst
        lhs.subst = lhs.subst
  \end{code}
\end{frame}

\begin{frame}
  \frametitle{Advantages}
  
  \begin{itemize}
  \item Keeps the dependency-graph cycle-free
  \item Pointpoint where to iterate, and under what conditions
  \item Construct parts of the tree while iterating
  \item Store \emph{visit-local} attributes to save
        information about an iteration
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Conclusion}
  
  \begin{itemize}
  \item AGs are a useful language to describe type inferencing algorithms
  \item Type inferencing is not syntax-directed
  \item Type inferencing requires choice/guessing/unknowns
  \item Iterative inferencing algorithms can be described with multi-visit AGs
  \end{itemize}
  
  More material:
  \url{http://www.cs.uu.nl/~ariem/thesis.pdf} (under construction...)
\end{frame}

\end{document}