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

%format t1
%format t2
%format t3
%format t4
%format C1
%format C2
%format C3

  \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}
  
  \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}
  
  \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}
  
  \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}
  
  \begin{code}
  data Expr = VarE String | AppE Expr Expr
  data Type = Arr Type Type | Con String
  type Env  = Map String Type
  \end{code}
  
  \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}
  \begin{mathpar}
    \inferrule*[right=App]
      { |g :- f : tf | \\
        |g :- a : ta | \\ 
        |g :- tf <= (ta -> r)| \\
      }
      { |g :- f a : r| }
  \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 -> r
  \end{code}
  
  
  \begin{mathpar}
    \inferrule*[right=Refl]
      {}
      { |t <= t| }
  \end{mathpar}
  \begin{code}
  Refl :  U    ->  epsilon   ^^^^  lhs.l (emph(==)) lhs.r
          lhs
  \end{code}
  \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}

  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}

  \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}

  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}

  \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}

  \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}