\documentclass[authoryear]{sigplanconf}

%include lhs2TeX.fmt
%include polycode.fmt

\usepackage{stmaryrd}
\usepackage{float}
\usepackage{graphicx}
\usepackage{pgf}
\usepackage{tikz}
\usepackage{mathpartir}
\usepackage{url}
\usepackage{txfonts}
\usetikzlibrary{arrows,positioning}
\floatstyle{boxed}
\restylefloat{figure}
\setlength{\fboxsep}{1.4pt}

%format emptyset = "\emptyset"
%format ^^^^ = "\hspace{1em}"
%format ^^^ = "\;"
%format sig = "\mathbf{sig}"
%format inh = "\mathbf{inh}"
%format syn = "\mathbf{syn}"
%format sem = "\mathbf{sem}"
%format tail = "\mathbf{tail}"
%format clause = "\mathbf{clause}"
%format match  = "\mathbf{match}"
%format child  = "\mathbf{child}"
%format forall (xs) (q) = "\mathbf{forall}\;" xs ".\;" q
%format (overline (x)) = "\overline{" x "}"
%format partial = "\mathbf{partial}"
%% %format lhs = "\mathbf{lhs}"
%% %format loc = "\mathbf{loc}"
%format alt = "\mathbf{alt}"
%format none = "\mathbf{none}"
%format strict = "\mathbf{strict}"
%format . = "."

%format alpha = "\alpha"
%format beta = "\beta"

%format (attr f a) = f "." a
%format (lhsattr a) = lhs "." a
%format (locattr a) = loc "." a
%format (sub (k) (x)) = "{" k "}_{" x "}"
%format (sup (k) (x)) = "{" k "}^{" x "}"
%format (tau (x)) = "\tau_{" x "}"
%format (In (k) (x))  = k "I" x
%format (Out (k) (x)) = k "O" x
%format (InLhs (x))  = "lhsI" x
%format (OutLhs (x)) = "lhsO" x

%format a1
%format a2
%format k1
%format k2
%format S1
%format S2
%format S3
%format S4
%format s1
%format s2
%format b1
%format t1
%format t2
%format t3
%format t4
%format x1
%format x2
%format i1
%format i2
%format v1
%format v2
%format u1
%format u2
%format u3
%format subst1
%format subst2
%format subst3
%format tauS' = "\tau_{" S' "}"

%format rulerfront  = "{\mbox{\scshape ruler-front}}"
%format rulercore   = "{\mbox{\scshape ruler-core}}"
%format shadow      = "{\mbox{\scshape schadow}}"

\renewcommand{\hscodestyle}{\small}

\begin{document}

\conferenceinfo{GPCE'10,} {October 10--13, 2010, Eindhoven, The Netherlands.}
\CopyrightYear{2010}
\copyrightdata{978-1-4503-0154-1/10/10}

\titlebanner{Submitted to GPCE 2010}        % These are ignored unless
\preprintfooter{|rulerfront|: attribute grammar language with explicit visits, first class derivations, and iterations.}   % 'preprint' option specified.

\title{Iterative Type Inference with Attribute Grammars}

\authorinfo{Arie Middelkoop \and Atze Dijkstra \and S. Doaitse Swierstra}
           {Universiteit Utrecht}
           {\{ariem,atze,doaitse\}@@cs.uu.nl}

\maketitle

\begin{abstract}
  Type inference is the process of constructing a
  typing derivation while gradually discovering type information.
  During this process, inference algorithms typically make subtle decisions
  based on the derivation constructed so far.

  Because a typing derivation is a decorated tree we aim to use attribute
  grammars as the main implementation tool.
  Unfortunately, we can neither express iteration, nor express decisions
  based on intermediate derivations in such grammars.

  We present the language |rulerfront|, a conservative extension to ordered
  attribute grammars, that deals with the aforementioned problems. We show why
  this extension is suitable for the description of constraint-based inference
  algorithms.
\end{abstract}

\category{F.3.1}{Logics and Meanings of Programs}{Specifying and Verifying and Reasoning about Programs}
\terms{Algorithms, Languages}

\section{Introduction}
\label{sect.visit.intro}

  Attribute grammars (AGs) are traditionally used to specify the static semantics of programming
  languages~\cite{DBLP:journals/mst/Knuth68}.
  Moreover, when semantic rules of an AG are written in a general
  purpose programming language, the AG can be compiled into
  an (efficient) multi-visit tree walk algorithms that implements the
  specification~\cite{DBLP:conf/popl/KennedyW76,DBLP:journals/acta/Kastens80}.

  We implemented a large portion of the Utrecht Haskell Compiler
  (UHC)~\cite{DBLP:conf/afp/DijkstraS04,DBLP:journals/entcs/FokkerS09}
  with attribute grammars using the UUAG system~\cite{uuagc}.
  Haskell~\cite{DBLP:journals/sigplan/HudakPWBFFGHHJKNPP92} is
  a purely functional programming language, with an elaborate and expressive type system.
  We also compile our
  attribute grammars to Haskell. The ideas presented in this paper, however,
  are not restricted to any particular language.

  Attribute grammars offer us two general benefits.
  \citet{DBLP:conf/haskell/DijkstraFS09} give a detailed description why these
  advantages are important for the UHC project.
  Firstly, the evaluation order of semantic rules is determined
  automatically, unrelated to the order of appearance.
  Rules may be written separately from each other, and grouped by
  aspect~\cite{DBLP:conf/icfp/VieraSS09,DBLP:conf/gpce/Saraiva02}.
  Secondly, semantic rules for idiomatic tree traversals (such as: topdown,
  bottom-up, and in-order) can be
  inferred automatically, thus allowing for concise specifications.

  Two main components of UHC's type inferencer, polymorphic unification and
  context reduction, would benefit from an AG-based implementation.
  However, we implemented them directly in Haskell, because it is not
  straightforward to express them as an attribute grammar.
  
  These two components exhibit two challenges to attribute grammars.
  Firstly, the grammar needs to produce typing derivations. The structure
  of such a derivation depends on what is known about types, and this
  information gradually becomes available during inferencing,
  e.g. due to unifications.
  This requires a mixture of tree construction and
  attribute evaluation, which are normally separate tasks if one takes an AG view.
  Secondly, construction of a subtree needs to be postponed when it depends on
  a type that is not known yet. Later, after we constructed more of the
  tree, this type may become known and the postponed construction can continue,
  or it becomes never known and we need to default it to some type.

  An evaluator for an attribute grammar starts from a given tree (usually constructed by the parser),
  and has a fixed algorithm
  to evaluate attributes. We present an AG extension to open up these
  algorithms to deal with the above challenges, without loosing the
  advantages that AGs offer.
  More precisely, our contributions are:
  \begin{itemize}
  \item We present the language |rulerfront|, a conservative extension
        of ordered attribute grammars.
        It has three concepts to deal with the above challenges.
        \begin{itemize}
        \item We exploit the notion of visits to the tree. In each
              visit some attributes are computed.
              Visits can be done iteratively. The number of iterations
              can be specified based on the values of attributes.
        \item Productions are chosen based on the values of attributes.
              A production can be chosen per visit.
        \item (Attributed) Derivation trees are first class values. They can be passed around
              in attributes, and inspected by visiting them.
        \end{itemize}
        In Section~\ref{sect.semantics}, we define a denotational
        semantics via a translation to Haskell.
  \item We present |rulerfront| by example in Section~\ref{sect:casestudy}.
        The example illustrates the challenges and motivates the need for the
        above concepts, but is necessarily dense.
        In related work~\cite{Middelkoop10wgt,Middelkoop10ifl},
        we give more gentle introductions to variations on this theme.
  
  \item An implementation of |rulerfront| including several examples
        is available at:
        \url{https://subversion.cs.uu.nl/repos/project.ruler.systems/ruler-core/}.
        The implementation supports both greedy and ondemand evaluation of
        attributes.
  \item We compare our approach with other attribute grammar approaches (Section~\ref{sect.visit.relatedwork})
        as a further motivation for the need for |rulerfront|'s extensions.
  \end{itemize}

\section{Motivation}
\label{sect:casestudy}

  In this section, we show how to implement a small compiler for
  an example language we named |shadow|, written with attribute
  grammars using |rulerfront|. The implementation of |shadow|
  poses exactly those challenges mentioned in the previous
  section, while being small enough to fit in this paper.

  We assume that the reader is familiar with attribute grammars~\cite{DBLP:journals/mst/Knuth68}
  and their terminology, as well as type systems and their implementation.
  For a more gentle introduction to both subjects including |rulerfront|, consider
  \cite{Middelkoop10wgt,Middelkoop10ifl}.

  \subsection{Example to implement: the language |shadow|}
  
  %format (sup x u) = "{" x "}^{" u "}"
  %format ty = "\tau"
  %format env = "\Gamma"
  %format :- = "\vdash"
  %format ~> = "\leadsto"
  %format . = "."
  %format ty1
  %format ty2
  
  We take for |shadow| the simply-typed lambda calculus, with two small modifications: we annotate
  bindings with annotations (i.e. |\(sup x u).|), and an identifier may refer to a \emph{shadowed} binding.
  For example, in the term |\(sup x u1). \(sup x u2). f x|, the expression |x| normally refers to the binding
  annotated with |u2|. However, if the expression cannot be typed with that binding, we allow |x| to refer to
  the shadowed binding annotated with |u1| instead, if this interpretation would be well-typed\footnote{
    |shadow| is an example language that we take as a given.
    It can be used to model typed disambiguation of duplicately imported identifiers from modules.
    However, its design rationale is out of the scope of this section.
  }. The interpretation of this expression is thus by default |\u1 . \u2 . f u2|, but under some conditions (defined
  more precisely later) it may be |\u1 . \u2 . f u1|.

  We write a compiler (i.e. a function |compile :: Env -> ExprS -> ExprT|) that takes a |shadow| expression (of type |ExprS|),
  type checks it with respect to the environment |Env|, and maps it to an expression (of type |ExprT|) in the simply-typed lambda calculus.
  \begin{code}
    -- concrete syntax and its abstract syntax in Haskell
  (sub e S)  ::=  x  |  (sub e S) (sub e S) |  ^^^^  data ExprS =  VarS Ident | AppS ExprS ExprS
                  \(sup x u). (sub e S)        ^^^^             |  LamS Ident Ident ExprS
  (sub e T)  ::=  u  |  (sub e T) (sub e T) |  ^^^^  data ExprT =  VarT Ident | AppT ExprT ExprT
                  \u. (sub e T)                ^^^^             |   LamT Ident ExprT
  ty         ::=  alpha | Int | ty -> ty       ^^^^  data Ty = TyVar Var | TyInt | TyArr Ty Ty
  \end{code}
  Before delving into the actual implementation, we first give a specification of the type system,
  together with translation rules.
  %format innermost = "\mbox{innermost}"
  %format ofall = "\mbox{of all}"
  \begin{mathpar}
    \fbox{|env :- (sub e S) : ty ~> (sub e T)|}\\
    \inferrule*[right=var]
      {|innermost (sup x u) ofall:|\\\\|(sup x u) : ty `elem` env|}
      {|env :- x : ty ~> u|}

    \inferrule*[right=app]
      {|env :- f : ty1 -> ty2 ~> f'|\\\\
       |env :- a : ty1 ~> a'|
      }
      {|env :- f a : ty2 ~> f' a'|}

    \inferrule*[right=lam]
      {|env, sup x u : ty1 :- e : ty2 ~> e'|}
      {|env :- \sup x u . e : ty1 -> ty2 ~> \u.e'|}
  \end{mathpar}
  Each lambda is assumed to be annotated with a unique |u|.
  Rule \TirName{var} is rather informal\footnote{
  Actually, the specification itself is incomplete and informal. We stress that
  our goal is not to
  rigorously discuss and prove properties about |shadow|. Instead, we show |rulerfront|
  and its concepts. The translation for |shadow| acts as illustration.
  }. Of all the bindings for |x| with the
  right type |ty|, the innermost one is to be chosen. Its annotation |u| is
  used as name in the translation. The rule \TirName{app} is standard.
  In rule \TirName{lam}, the type of a binding is appended to the environment.
  The annotation of the binding is used as the name of the binding in the translation.
  
  Given an (empty) environment, a |shadow| expression, and optionally a type,
  we can manually construct a derivation tree using these translation rules. 
  The lookup of a binding poses a challenge due to context sensitivity.
  For example, for |\(sup x u1). \(sup x u2). f x|,
  the choice between translations |\u1 . \u2 . f u1| and |\u1 . \u2 . f u2| depends
  on what the program, where this expression occurs in, states about the type of |f| and
  the type of the entire expression by itself. When the context imposes insufficient
  restrictions to find a unique solution, the \TirName{var} states that we should default to the
  innermost possibility\footnote {
    The reader may observe that this example has a strong connection to context reduction in Haskell.
    The challenge is that we deal with type-directed inference rules, which may be overlapping or
    whose selection may remain ambiguous.
  }. 

  \subsection{Relation to attribute grammars}
  
  We focus on writing an implementation for the above translation rules with
  attribute grammars using |rulerfront|.
  For each relation in the above specification, we introduce a nonterminal in
  the |rulerfront| code. The parameters of the relations become attributes
  of these nonterminals, thus also the expression part which is normally implicit
  in an AG based description. Derivation rules become productions, and their contents
  we map to semantic rules.
  The productions contain no terminals:
  only the values of attributes determine the structure of the derivation tree.
  Thus, the attribute grammar defines the language of derivation trees
  for the translation rules.
  Note that this differs from the normal AG approach, \emph{where a single specific
  parameter of the relations fully determines the shape of the derivation tree}.

  Operationally, the algorithm which constructs derivation trees picks a
  production, recursively builds the derivations for the children of the
  production, computes attributes, and if there is a mismatch between the
  value of an attribute and what is expected of it,
  backtracks to the next production.
  
  We necessarily treat productions a bit differently in order to capture the
  gradual process of type inference.
  Final decisions about what productions are chosen to make up the
  derivation tree cannot be made until sufficient information is available.
  Therefore, we construct the derivation tree in one or more
  sequential passes called visits.
  As key feature of |rulerfront|, \emph{a nonterminal has productions per visit}.
  To make the distinction clearer,
  we call these clauses.
  During the construction of
  the part of a derivation for a visit, we try to apply the available clauses to build the portion
  of the derivation tree for that visit. When successful, we finalize the
  choice for that clause (similar to the cut in Prolog). The next visit
  can thus assume that those parts of the derivation tree constructed in previous
  visits is final. Moreover, we often wish to repeat a visit when
  type information was discovered that sheds new light upon decisions
  taken earlier during the visit.
  The upcoming example code shows this behavior several times.

  In a normal AG, for each non-terminal in the tree, we have exactly one production.
  In our new model we can at each next visit choose again how to refine the production.
  So, we can regard our approach as having our productions organized as the leafs of a tree
  of clauses, and at each next visit we refine the choice a bit by going down one of the paths in the tree.
  Once we have payed all visits and made all choices we know the production precisely.

  %format itf = "\mathbf{itf}"
  A |rulerfront| program is a Haskell program augmented with attribute
  grammar code.
  We generate vanilla Haskell code from such a program.
  For each
  nonterminal in a |rulerfront| program we generate a Haskell coroutine, encoded using continuations.
  The following is a sketch of |rulerfront| program (we explain
  the various forms of syntax later):
  \begin{code}
  module MyCompiler where
  data ExprS = ...   -- Haskell data declaration
  itf TransExpr ...  -- |rulerfront| nonterm and attr declaration
  itf TransExpr ...  -- additional attr declarations for nonterm
  ones = 1 : ones    -- Haskell binding
  translate = sem transExpr :: TransExpr  -- embedded nonterminal
                ... rules ...             -- (|rulerfront|)
  sem transExpr ... rules ...  -- additional rules for nonterm
  sem transExpr ... rules ...  -- even more rules
  \end{code}
  The idea is that we define a nonterminal (introduce it, give clauses and
  rules) inside a Haskell expression using a sem-block. Additional clauses
  and rules can be given in separate toplevel sem-blocks.
  
  The coroutines we generate from nonterminals are known as visit functions~\cite{DBLP:conf/ifip2-4/SwierstraA98}.
  Instantiation of a coroutine corresponds to the construction of
  the root node of a derivation tree.
  An invocation of such a coroutine corresponds to a visit in our attribute
  grammar description. Inputs to and outputs from the visits of the
  coroutine represent inherited and synthesized attributes respectively.
  Clauses are mapped to function alternatives of the coroutine.
  The internal state of the coroutine represents the
  derivation tree. This state contains instances of coroutines that
  represent the children.
  In Section~\ref{sect.semantics} we precisely show the translation to
  Haskell.

  %format (many x) = "\overline{" x "}"
  %format (opt x) = "{" x "_?}"
  %format itf     = "\mathbf{itf}"
  %format ty      = "ty"
  %format env     = "env"
  %format inh     = "\mathbf{inh}"
  %format syn     = "\mathbf{syn}"
  %format chn     = "\mathbf{chn}"
  %format visit   = "\mathbf{visit}"
  %format visitstar = "\mathbf{visit\star}"
  %format visitbang = "\mathbf{visit!}"
  %format star    = "\mathbf{\star}"
  %format clause  = "\mathbf{clause}"
  %format default = "\mathbf{default}"
  %format self    = "\mathbf{self}"
  %format rename  = "\mathbf{rename}"
  %format forall  = "\mathbf{forall}"
  %format hides   = "\mathbf{hides}"
  %format attach  = "\mathbf{attach}"
  %format detach  = "\mathbf{detach}"
  %format sep     = ";\;\;"
  %format iterate = "\mathbf{iterate}"
  %format invoke = "\mathbf{invoke}"
  
  \subsection{Typing expressions}
  
  Figure~\ref{fig.example.derivation}
  gives a rudimentary sketch of a derivation tree and some of the nonterminals we introduce.
  Nonterminal |compile| is
  the root. It has a child of nonterminal |transExpr|, and clauses for the various
  forms of syntax of |shadow|. In locating a variable definition in the environment, three nonterminals play a role.
  |lookup| has a list of children formed by |lkMany| nonterminals. These are
  |lookupLam| children, representing a choice for a binding (the dotted line points to that
  binding). At the end of inference, at most one of these choices remains.

  \begin{figure}[htb]
  \begin{tikzpicture}
    [ grow=up
    , nd/.style={circle, minimum size=2mm, node distance=4mm, very thick, draw=black!50, top color=white, bottom color=black!20,font=\scriptsize}
    , lab/.style={xshift=-4mm, font=\scriptsize}
    , arr/.style={<-,dashed, very thick}
    , level distance=5mm
    , sibling distance=32mm
    ]
    \node(wrapper)[nd]{} % Compile.wrapper
      child {
        node(lam1)[nd]{} % Expr.lam
          child {
            node(lam2)[nd]{} % Expr.lam
              child {
                node(var)[nd]{} % Expr.var
                  child {
                    node(lookupTy)[nd]{} % Lookpup.lookupTy
                      child {
                        node(cons1)[nd]{} % LookupMany.cons
                          child {
                            node(lookupLam1)[nd]{} % LookupOne.lookupLam
                          }
                          child {
                            node(cons2)[nd]{} % LookupMany.cons
                              child {
                                node(lookupLam2)[nd]{} % LookupOne.lookupLam
                              }
                              child {
                                node(nil)[nd]{} % LookupMany.nil
                              }
                          }
                      }
                  }
              }
          }
      };
      
      \node[lab, left of=wrapper]{|compile.wrapper|};
      \node[lab, left of=lam1]{|transExpr.exprLam|};
      \node[lab, left of=lam2]{|transExpr.exprLam|};
      \node[lab, left of=var]{|transExpr.exprVar|};
      \node[lab, left of=lookupTy]{|lookup.lookupTy|};
      \node[lab, left of=cons1]{|lkMany.lkCons|};
      \node[lab, left of=cons2]{|lkMany.lkCons|};
      \node[lab, left of=nil]{|lkMany.lkNil|};
      \node[lab, left of=lookupLam1]{|lookupLam.lookupLam|};
      \node[lab, left of=lookupLam2]{|lookupLam.lookupLam|};

      \draw[arr](lookupLam1) to [in=0,out=0] node[auto,lab,xshift=2mm]{|u2|} (lam2);
      \draw[arr](lookupLam2) to [in=0,out=0] node[auto,lab]{|u1|} (lam1);
  \end{tikzpicture}
  \caption{Sketch of derivation tree for |\(sup x u1) . \(sup x u2) . x|}
  \label{fig.example.derivation}
  \end{figure}

  We declare a type |TransExpr| for the nonterminal |transExpr|, which describes
  the interface (|itf|) of a nonterminal.
  The interface declares the visits and attributes of a nonterminal.
  \begin{code}
  itf TransExpr            -- type of a nonterminal
    inh env :: Env         -- inherited attr (belongs to some visit)
    visit dispatch         -- declares a visit
      inh expr :: ExprS    -- inherited attr (belongs to visit |dispatch|)

  type Env = Map Ident [LookupOne]  -- shown later
  \end{code}
  In this case, a nonterminal with the interface |TransExpr| has
  a single visit named |dispatch|, and two inherited attributes.
  The attribute |expr| contains the expression to translate.
  Later we will define more attributes and visits on |TransExpr|.

  The visits are automatically totally ordered if this can be done,
  based on value-dependencies between attributes derived from all
  clauses in the code.
  Attribute |expr| is declared explicitly for visit |dispatch| (note
  the indenting). The |env| attribute is not: we automatically determine
  the earliest visit is can be allocated to.

  From the above interface, we generate
  a Haskell type for the coroutines that we generate for
  nonterminals with this interface, as well as functions to
  invoke the coroutines and access or provide values for
  attributes from the Haskell code.
  
  We introduce a nonterminal |transExpr| with interface
  |TransExpr| using a sem-block, embedded in Haskell code.
  We translate this sem-block to a vanilla Haskell coroutine
  expression.
  \begin{code}
  -- embedded toplevel Haskell code:
  translate = sem transExpr :: TransExpr
  \end{code}
  We bind it to the
  Haskell name |translate|, such that we can refer to it
  from the Haskell code.
  The nonterminal name |transExpr| is global to the entire
  program. The Haskell name |translate| follows
  Haskell's scoping rules.
  
  If we visit a |transExpr|-node for the first time, we have to see what kind of expression we have at hand.
  We do so by defining a number of alternative ways to deal with the node by introducing a couple of named clauses.
  For each of the clause we subsequently introduce further sem-rules to detail what has to be done.
  Unlike most of the other code that we give in this section, the
  order of appearance does matter for clauses, because operationally
  they are tried in that order.
  \begin{code}
  sem transExpr  -- nonterminal with clauses
    clause  exprVar  of dispatch  -- as the name of the first
    clause  exprApp  of dispatch  -- visit we typically
    clause  exprLam  of dispatch  -- use |dispatch|

  sem exprVar    -- clause with rules (or clause of next visit)
    -- semantic rule (i.e. to match against attributes)
    -- semantic rule (i.e. to define a child)
    -- perhaps clause of next visit (in scope of this clause)
  \end{code}
  Clauses provide a means of scoping. For example, we typically
  declare clauses of the next visit in the scope of the father
  clause (i.e. clause taken at the previous visit).
  These inherit all the attributes and children
  in scope of that clause. Otherwise, they only inherit the common
  attributes and children. This enforces as well that the
  embedded clause takes place after the enclosing clause.
%%  A visit has often only one clause. This clause does not need to
%%  be declared. The rules can be written in the sem-block of the
%%  nonterminal instead or a clause of a previous visit.
  
  With a clause we associate a couple of semantic rules, all of
  which may fail and cause backtracking, may have an effect on the
  derivation tree we are constructing, or lead to a runtime error.
  \begin{itemize}
  \item
    \begin{code}
    match pattern = code            -- match-rule
    match (VarS loc.nm) = lhs.expr  -- example
    \end{code}
    The Haskell |pattern| must match the value of the right hand side. Evaluation
    of the rule requires the full pattern match to take place, or causes a backtrack
    to the next clause.

    Variables in the pattern refer to attributes, and have the form |childname.attrname|.
    The child name |lhs| is reserved to refer to the
    attributes of the current node. Furthermore, child name |loc| is a
    virtual child that conveniently stores local attributes, analogous to local variables.
    In the example, |lhs.expr| thus refers to the inherited attribute |expr| of the current
    node.
  \item
    \begin{code}
    pattern = code  -- assert-rule (not prefixed with a keyword)
    \end{code}
    Similar to the above, except that the match is expected to succeed. If not,
    evaluation aborts with a runtime error.
  \item
    \begin{code}
    child name :: I = code              -- child-rule
    child fun :: TransExpr = translate  -- example
    \end{code}
    In contrast to a conventional attribute grammar, we construct the
    tree during attribute evaluation. The rule above creates a child
    with the given |name|, described by a nonterminal with interface
    |I|, and defined by the coroutine |code|. For example, |code| could
    be the expression |translate|, or a more complex expression. Later we
    show an example where the code for a child is provided by an attribute.
    Evaluation of the child rule creates a fresh instance of this coroutine.
    This child will thus have its own set of attributes defined by |I|.
  \item
    \begin{code}
    default name [= f]  -- default rule
    \end{code}
    Provides a default definition for all synthesized attributes named |name|
    of the production and all inherited attributes of the children that are in scope.
    This default definition applies only to an attribute if no explicit definition is given.
    We come back to this rule later.
  \end{itemize}
  Later, we introduce more forms of rules.

  The evaluation order of rules is determined automatically based on
  their dependencies on attributes. Rules may refer to attributes defined by previous rules, including
  rules of clauses of previous visits.
  Similarly, attributes are mapped automatically
  to visits based on requirements by rules. Cyclic dependencies
  are considered to be a static error.
  The rules may be scheduled to a later visit, except for
  match-rules. These are scheduled in the visit
  of the clause they appear in.
  Visits to children are determined automatically based on dependencies of
  attributes of the children. If a visit to a child fails, which is the case
  when none of the children's clauses applies, the complete clause
  backtracks as well.

  The following is part of the clause for |exprVar|. It 
  states that the value of attribute |lhs.expr|
  must match the |VarS| constructor.
  \begin{code}
  sem exprVar  -- clause |exprVar| of nonterminal |transExpr|
    match (VarS loc.nm) = lhs.expr  -- if succesful, defines |loc.nm|
  \end{code}
  
  The names of inherited and synthesized attributes do not have to be distinct.
  Attribute variables in patterns refer to \emph{synthesized} attributes of |lhs|, or
  \emph{inherited} attributes of the children. Likewise, attribute variables in the right-hand side of a match
  refer to \emph{inherited} attributes of |lhs| or \emph{synthesized} attributes
  of the children.
  This ensures that attribute occurrences are uniquely identifyable.

  The following clause for |exprApp| demonstrates the use of child-rules. It introduces
  two children |f| and |a| with interface |TransExpr|, represented as instances of
  the |translate| coroutine.
  \begin{code}
  sem exprApp  -- clause |exprApp| of nonterminal |transExpr|
    match (AppS loc.f loc.a) = lhs.expr  -- is it an |AppS|?

    child f :: TransExpr  = translate    -- recurse on |f|
    child a :: TransExpr  = translate    -- recurse on |a|

    f.expr     = loc.f                   -- pass the
    a.expr     = loc.a                   -- expressions

    f.env      = lhs.env                 -- pass the
    a.env      = lhs.env                 -- environments
  \end{code}
  The last two lines express that the environment is passed down unchanged.
  We may omit these rules, and write the rule |default env| instead.
  When a child has an inherited attribute |env|, but no explicit rule
  has been given, and the production has |lhs.env|, then that
  value is automatically passed on.
  \begin{code}
  sem transExpr  -- for all clauses of |transExpr|
    default env
  \end{code}
  There are several variations of default-rules. We
  see later e.g. a default rule for synthesized attributes.

  We skip the clause |exprLam| for now, and consider types and type inference first.
  As usual with type inference, we introduce type variables for yet unknown types,
  and compute a substitution that binds types to these variables.
  \begin{code}
  itf TransExpr            -- extend interface of |TransExpr|
    syn ty      :: Ty      -- synthesized attr of some visit
    chn subst1  :: Subst   -- chained attr auto of some visit

  data Subst  -- left implicit: a mapping from variables to types
  \end{code}
  The chained attribute |subst1| stands for both an inherited and synthesized attribute
  with the same name. We can see this as a substitution that goes in, and comes out
  again updated with new type information that became available during the visit.
  We get automatic threading of the attribute through all children that have
  a chained attribute with this name, using the default-rule:
  \begin{code}
  sem transExpr ^^^^ default subst1
  \end{code}

  To deal with types and substitutions, we define several helper nonterminals.
  \begin{code}
  itf Lookup                 -- finds a pair |(nm,ty') `elem` ty|
    inh nm        :: Ident   -- such that |ty'| matches |ty|.
    inh ty        :: Ty
    inh env       :: Env

  itf Unify                  -- computes a substitution |s| such
    visit dispatch           -- that |s(ty1)| equals |s(ty2)|, if
      inh ty1      :: Ty     -- possible. Attributes for the
      inh ty2      :: Ty     -- substitution and errors added later.

  itf Fresh                  -- produces a fresh type
    syn ty        :: Ty
    chn subst     :: Subst

  lookup  = sem lookupTy  :: Lookup
  unify   = sem unifyTy   :: Unify
  fresh   = sem freshTy   :: Fresh
  \end{code}
  
  The implementation of |fresh| delegates to a library function
  |varFresh| on substitutions.
  \begin{code}
  sem freshTy
    (lhs.subst, loc.var) = varFresh lhs.subst
    lhs.ty = TyVar loc.var
  \end{code}
  We did not explicitly declare any visits for |freshTy|. In that case, it consists of
  a single anonymous visit. Similarly, when a visit does not have any declared clauses,
  it consists of a single anonymous clause.
  
  Interesting to note here is that we can wrap any Haskell function (including a data constructors)
  as a nonterminal, and represent an application of this function as child of the production.
  This is convenient in case of |fresh|, because we use default rules
  to automatically deal with the substitution attribute. Overdoing this, however, obscures the code.

  Both |fresh| and |lookup| are of use to refine the implementation of |exprVar|. With
  |fresh| we get a fresh variable to use as the type of the expression. Lookup then ensures
  that at some point this fresh type is constrained in the substitution to the type of
  a binding for the variable.
  \begin{code}
  sem exprVar  -- repeated sem-block: extends previous one
    child fr  :: Fresh   = fresh
    child lk  :: Lookup  = lookup
    lk.nm   = loc.nm  -- pass |loc.nm| to |lk| (|loc.nm| matched earlier)
    lk.ty   = fr.ty   -- pass the fresh type to |lk|
    lhs.ty  = fr.ty   -- also pass it up
  \end{code}
  The substitution we pass to child |fr|. The substitution that comes out, we pass up
  to the parent.
  \begin{code}
  sem exprVar
    sem exprVar ^^^^ rename subst := subst1 of fr

    fr.subst    = lhs.subst1  -- pass down
    lhs.subst1  = fr.subst    -- pass up
  \end{code}
  Recall that |subst1| is a chained attribute, hence there is an inherited
  |lhs.subst1|, and a synthesized |lhs.subst1|. These names are not ambiguous:
  the right hand side of the rule refers to the inherited attribute, the left
  hand side to the synthesized.
  With a rename-rule, we rename attributes of children to choose a more convenient name,
  for example to benefit from default-rules.
  The two explicit rules may actually be omitted, because of default-rule mentioned earlier.

  In the application clause, we use the |unify| nonterminal to
  express that various types should match.
  \begin{code}
  sem exprApp
    child fr  :: Fresh  = fresh
    child u   :: Unify  = unify

    u.ty1   = f.ty
    u.ty2   = TyArr a.ty fr.ty
    lhs.ty  = fr.ty

    rename subst := subst1 of fr  -- for default-rule
  \end{code}
  Rules for the substitution may be omitted. The default-rule threads
  it properly through the |fr| and |u| children, which (after renaming)
  both have a |subst1| chained attribute.
  
  \subsection{Unification}

  So far the example can be implemented with most attribute grammar
  systems that operate on a fixed abstract syntax
  tree~\cite{DBLP:conf/afp/DijkstraS04,DBLP:conf/flops/DijkstraS06}. In the above example, the
  choice of productions solemnly depends on the |expr| inherited
  attribute. The attribute grammar is directly
  based on the grammar of expressions.
  In the remainder of this section, we move beyond such systems.
  For unification, we allow a selection of production based on
  two inherited attributes: the attributes |ty1| and
  |ty2| of interface |Unify| defined above.

  The idea behind unification is to recursively compare these types.
  If one is a variable, then the other type is bound to that variable
  in the substitution.

  \begin{code}
  sem unifyTy
    clause matchEqVars  of dispatch  -- the same variables
    clause matchVarL    of dispatch  -- left a variable
    clause matchVarR    of dispatch  -- right a variable
    clause matchArr     of dispatch  -- both an arrow
    clause matchBase    of dispatch  -- both the same constant
    clause matchFail    of dispatch  -- failure
  \end{code}

  To implement these clauses, we need additional infrastructure
  to obtain the free variables of a type, and bind a type in the
  substitution. The actual implementations we omit, since these are similar
  to other examples in this section.
  \begin{code}
  itf Ftv  inh ty     :: Ty       -- determines free |vars| of |ty|
           inh subst  :: Subst    -- after applying the |subst|
           syn vars   :: [Var]

  itf Bind  inh var    :: Var     -- appends to |subst|:
            inh ty     :: Ty      -- |[var := ty]|
            chn subst  :: Subst

  ftv    = sem ftv    :: Ftv      -- impl. with |rulerfront|
  bind   = sem bind   :: Bind     -- wrapper around library fun
  \end{code}

  We define several additional attributes on the |Unify| nonterminal.
  For the synthesized attributes |success| and |errs|, we give
  a default definition of the form |default attr = f|.
  This function |f| gets as first parameter a list of values of
  attributes |attr| of the children that have this attribute.
  If the function is not given, we use the Haskell function |last| for |f|.
  \begin{code}
  itf Unify
    visit dispatch
      chn subst1   :: Subst
      syn success  :: Bool   -- |True| iff unification succeeds
      syn changes  :: Bool   -- |True| iff any variables were bound
    visit outcome
      inh subst2   :: Subst  -- take |subst2| more recent as
      syn errs     :: Errs   -- |subst1| for better error messages

  sem unifyTy
    default  success  = and     -- |and  [] = True|
    default  changes  = or      -- |or   [] = False|
    default  errors   = concat

    loc.ty1 = tyExpand lhs.subst1 lhs.ty1  -- apply subst one level
    loc.ty2 = tyExpand lhs.subst1 lhs.ty2  -- apply subst one level
  \end{code}
  The inherited types need to be compared with what is known in the
  substitution to ensure that we do not bind to a variable twice.
  Hence we introduce attributes |loc.ty1| and |loc.ty2| that are
  computed by applying the substitution to the two inherited types that are to be unified.
  Their values are shared among all clauses and
  are computed only once. We match on these values to select a clause.
  \begin{code}
  sem matchEqVars  -- applies if we get two equal vars
    match True  = same lhs.ty1 lhs.ty2 || same loc.ty1 loc.ty2
  
  -- embedded Haskell code:
  same (TyVar v1) (TyVar v2) | v1 == v2  = True
  same _                                 = False

  sem matchVarL  -- a yet unknown type left
    match (TyVar loc.var)  = loc.ty1
    loc.ty                 = loc.ty2

  sem matchVarR  -- a yet unknown type right
    match (TyVar loc.var)  = loc.ty2
    loc.ty                 = loc.ty1
  
  sem matchVarL matchVarR   -- common part of above
    child fr :: Ftv = ftv   -- determine free |fr.vars|
    fr.ty = loc.ty          -- of |loc.ty|

    child b :: Bind = bind  -- add substitution
    b.var  = loc.var        --  |[loc.var := loc.ty]|
    b.ty   = loc.ty

    rename subst := subst1 of fr b

    loc.occurs   = loc.var `elem` fr.vars  -- occur check
    lhs.subst1   = if loc.occurs then lhs.subst1 else b.subst1
    lhs.success  = not loc.occurs
    lhs.changes  = not loc.occurs

    lhs.errs =  if loc.occurs
                then  [CyclErr lhs.subst2 loc.var loc.ty]
                else  []

  sem matchArr  -- |t1 -> t2| left and |t3 -> t4| right
    match (TyArr t1 t2)  = loc.ty1
    match (TyArr t3 t4)  = loc.ty2

    child l :: Unify  = unify  -- recurse with argument types
    child r :: Unify  = unify  -- recurse with result types
    l.ty1 = t1 sep l.ty2 = t3 sep r.ty1 = t2 sep r.ty2 = t4

  sem matchBase  -- applies when e.g. both are |TyInt|
    match True = loc.ty1 == loc.ty2

  sem matchFail  -- mismatch between types
    lhs.success  = False
    lhs.errs     = [UnifyErr lhs.subst2 lhs.ty1 lhs.ty2]
  \end{code}
  The clauses of |unifyTy| are total, thus there is always one that applies,
  with |matchFail| as fallback. The visits to unification thus always
  succeed. Potential problems that arose during unification can be
  inspected through attributes |success| and |errs|.

  We now have the mechanisms available to deal with the case of a
  lambda expression. For the type of the binding, we introduce a
  fresh type |fr.ty|, and add this type together with the name to
  the environment.
  \begin{code}
  sem exprLam
    match (LamS loc.nm loc.u loc.b) = lhs.expr

    child b   :: TransExpr  = translate  -- recurse
    child fr  :: Fresh      = fresh
    rename subst := subst1 of fr

    b.expr  = loc.b
    b.env   = insertWith (++) loc.nm [loc.lk] env  -- append
    lhs.ty  = TyArr fr.ty b.ty  -- result type is |fr.ty -> b.ty|
    
    loc.lk  = sem lookupLam :: LookupOne  -- see below
  \end{code}
  Environments are treated a bit differently. Instead of
  transporting the information needed to construct the
  lookup-derivation tree in |exprVar|, we transport a
  coroutine |loc.lk| defined in |exprLam|. We define the
  nonterminal |lookupLam| belonging to |loc.lk|
  locally in |exprLam|, such that we access to the attributes of
  |exprLam|.
  \begin{code}
  itf LookupOne  -- interface of nested |lookupLam|
    visit dispatch   inh  ty :: Ty
  \end{code}
  The idea is that we instantiate this coroutine at the
  |exprVar|, then pass it the expected type of the expression, and determine if
  the expected type matches the inferred type of the
  binding.
  The rules for this nested nonterminal (shown later)
  have access to the
  local state (i.e. attributes) of the enclosing nonterminal.
  At the binding-site, we have information such as
  the type and annotation of the binding, which we need to
  construct the derivation.
  
  \subsection{Lookups in the environment}
  \label{sect.lookups}
  
  At |exprVar|, the goal is to prove that there is a binding in the
  environment with the right type. The overall idea is that we
  construct all possible derivations of bindings for an identifier,
  using the |lookupLam| nonterminal mentioned earlier.
  
  When there is only one possibility, we incorporate it in the
  substitution, and repeat the visits. The extra type information
  may rule out other derivations, and result in new type information,
  etc. Eventually a fixpoint is reached.
  Of all the remaining ambiguous derivations, we pick the
  deepest ones, and \emph{default} to those, by incorporating
  their changes into the substitution.
  We then repeat the process from the beginning, until no
  ambiguities remain.
  We run this process on the expression as a whole. In more complex
  examples that have a let-binding, this process could be repeated
  per binding group.
  In the purely functional |rulerfront| language, we encode this
  necessarily imperative process using repeated invocation of
  visits combined with a chained substitution.

  We show the implementation of the above algorithm in
  a step by step fashion. Recall Figure~\ref{fig.example.derivation}.
  Three nonterminals play an essential
  role: |Lookup| is invoked from the |exprVar| clause and
  delegates to |LookupMany| to create all derivations
  possible. To create one derivation, |LookupMany| creates
  |LookupOne| derivations, one for each nested nonterminal
  |lookupLam| that was put for that identifier into the
  environment at |exprLam|.
  \begin{code}
  sem lookupTy  -- invoked from |exprVar|
    child forest :: LookupMany = lookupMany
    forest.lks  = find [] lhs.nm lhs.env  -- all |LookupOne|s
    forest.ty   = lhs.ty  -- inherited attr of |Lookup|
  \end{code}
  The |lks| attribute is a list of coroutines. The coroutine
  lookupMany instantiates each of them, and passes on the |ty|
  attribute to each.
  \begin{code}
  itf LookupMany
    visit dispatch  inh lks  :: [LookupOne]
                    inh ty   :: Ty

  lookupMany = sem lkMany :: LookupMany  
  sem lkMany
    clause lkNil  of dispatch  -- when |lhs.lks| is empty
    clause lkCons of dispatch  -- when it has an elem

  sem lkNil
    match [] = lhs.lks  -- reached end of the list

  sem lkCons
    match (loc.hd : loc.tl)  = lhs.lks
    child hd :: LookupOne    = loc.hd      -- taken from list
    child tl :: LookupMany   = lookupMany  -- recurse
    tl.lks = loc.tl  -- remainder of the lookups
    default ty  -- pass downwards to |hd| and |tl|
  \end{code}
  
  If all the matching lookupsOnes are reduced to one,
  we pick that one and return its substitution.
  Otherwise, we return the substitution belonging to
  the innermost binding (which has highest |depth|).
  \begin{code}
  itf Lookup LookupOne LookupMany
    visit resolve  -- hunt for a derivation
      chn subst   :: Subst
      syn status  :: Status  -- outcome of the visit
      syn depth   :: Int     -- depth of the binding
    visit resolved  -- invoked afterward

  data Status = Fails | Succeeds { amb :: Bool, change :: Bool }
  isAmbiguous (Succeeds True _)  = True
  isAmbiguous _                  = False
  \end{code}
  Every visit is invoked at least once, unless it is declared
  to be hidden. We intend to invoke the |resolve| visit multiple
  times. We show later how this is done.

  The depth information is easily determined at the
  binding-site for lambda expressions, with an inherited
  attribute |depth|, starting with |0| at the top, and
  incrementing it with each lambda.
  \begin{code}
  itf TransExpr  inh depth  :: Int
  sem transExpr  default depth = 0
  sem exprLam    b.depth = 1 + lhs.depth
  \end{code}
  The default-rule for an inherited attribute optionally takes
  a Haskell expression (|0| in this case), which is only used
  when there is no parent attribute with the same name.

  The rules for |lookupLam| are relatively straightforward.
  \begin{code}
  sem lookupLam  -- defined inside |exprLam| above
    child m :: Unify = unify      -- try match of binding type
    rename subst1 := subst of m   -- to use-site type |lhs.ty|
    hide outcome of m  -- declare not to visit |outcome|

    m.ty1     = outer.fr.ty -- of enclosing |exprLam|
    m.ty2     = lhs.ty

    lhs.status = if m.success then Succeeds False m.changes else Fails
    lhs.depth  = outer.lhs.depth  -- of enclosing |exprLam|
  \end{code}
  With |hide|, we state not to invoke a visit and the visits
  that follow. Referencing to attributes of such a visit is considered
  a static error.

  The |lkCons| clause makes a choice. If one derivation remains, it delivers
  that one's substitution as result. Otherwise, it indicates that
  an ambiguous choice remains. The lookup with the highest depth
  is by construction at the beginning of the list.
  \begin{code}
  sem lkNil
    lhs.depth   = 0          -- lowest depth
    lhs.subst   = lhs.subst  -- no change to subst
    lhs.status  = Fails

  sem lkCons
    hd.subst  = lhs.subst  -- passed down to
    tl.subst  = lhs.subst  -- both
    
    (loc.pick, lhs.status, lhs.depth, lhs.subst)
      = case hd.status of
          Fails -> (False, tl.status, tl.depth, tl.subst)
          Success _ hdc ->
            let  status' = case tl.status of
                             Fails          -> hd.status
                             Success _ tlc  -> Success True (hdc || tlc)
            in (True, status', hd.depth, hd.subst)
  \end{code}
  
  When a visit is invoked again, we typically want to access some results
  of a previous invocation.
  To retain state between multiple invocations of a visits,
  we allow visits to take visit-local chained attributes. For
  example, an attribute |decided| for visit |resolve|.
  \begin{code}
  sem lookupTy ^^^^ visit.resolve.decided  = False  -- initial value
  \end{code}
  From inside the visit, we can match on these attributes to
  select a clause. Furthermore, there is an implicit default rule for them.
  \begin{code}
  sem lookupTy
    clause lkRunning of resolve     -- no final choice yet,
      match False = visit.decided   -- try again
      visit.decided = isAmbiguous lk.status
      default status depth subst    -- just pass on

    clause lkFinished of resolve  -- made final choice
      match True  = visit.decided
      lhs.status  = Success False False  -- no change
      lhs.depth   = 0
      default subst
  \end{code}

  %format langle = "\langle"
  %format rangle = "\rangle"
  Children created in a visit are discarded when the visit is repeated.
  The state of children created by a previous visit is properly maintained
  if their visits are also repeated.
  To prevent a created child from being discarded, it is possible to save
  a child in an attribute.
  Recall that children are derivations, which are instances of a coroutine, and
  these are first class values,
  The detach-rule can exactly be used for this purpose:
  |langle at = detach visitname of childname rangle| takes a child |childname| evaluated up
  to but not including visit |visitname|, and stores it in an attribute |at|.
  The attach-rule, |langle attach visitname of childname = code rangle|, takes such a
  child-value (defined by |code|) and attaches it to a child named |childname|.
  If |childname| already exists as child, the attach-rule overrules the visits starting
  from |visitname|.

  These |resolve| visits on |lookupTy| are invoked from |resolve|
  visits of |transExpr|. In map |deflMap|, we maintain the
  substitutions of ambiguous lookups per depth. These have not been
  incorporated in |subst2| yet. Applying the deepest of those, causes
  a defaulting to the corresponding bindings.
  \begin{code}
  itf TransExpr
    visitbang resolve
      chn  subst2   :: Subst
      syn  changes  :: Bool  -- True iff |subst2| was affected
      syn  deflMap  :: IntMap [Subst]  -- defaulting subst/depth
  \end{code}
  The bang at the resolve visit indicates that all attributes must
  be scheduled explicitly to this visit. No attribute is automatically
  assigned to this visit. This gives the visit a predictable interface,
  which is convenient when invoking the visit explicitly, as we do
  later.
  \begin{code}
  sem transExpr
    default changes  = or
    default deflMap  = unionsWith (++)
    default subst2
  \end{code}
  For ambiguous lookups in the |exprVar|, we add to |deflMap|.
  \begin{code}
  sem exprVar
    clause varLkAmb of resolve  -- put |lk.subst| in |deflMap|
      match (Success True _) = f.status
      lhs.deflMap = singleton lk.depth [lk.subst]
      lhs.subst2  = lhs.subst2  -- bypass |lk.subst|
    clause varLkOther of resolve  -- default rules only
  \end{code}

  To drive the iterations, we introduce a nonterminal |iterInner|, that
  invokes visit |resolve| one or more times. The iterate-rule
  |langle iterate visitname of childname = e rangle| denotes
  repeated invocation of |visitname| on |childname|. Code |e| defines the
  coroutine of a special nonterminal (|iterNext|, explained later) that computes
  the inherited attributes for the visit of the next iteration, out of the
  synthesized attributes of the previous. The iteration stops
  when this special nonterminal does not have an applicable
  clause.
  \begin{code}
  iterInner = sem iterInner :: ExprTrans
  sem iterInner
    child e :: ExprTrans = translate  -- |iterInner| is an extra node
    e.expr = lhs.expr                 -- on top of the derivation tree
    default ... -- omitted: same defaults as transExpr

    iterate resolve of e = next  -- until |e.changed| is |False|

    lhs.subst2  =  let  pairs   = toAscList e.deflMap ++ [(0, [e.subst2])]
                        substs  = head pairs  -- deepest substitutions
                   in foldl substMerge e.subst2 substs  -- apply them
    lhs.changes = not (null e.deflMap)
  \end{code}
  This special nonterminal has as interface the \emph{contravariant} interface
  of the visit |resolve| of |ExprTrans|, i.e. the inherited attributes
  turn to synthesized attributes, and vice versa. The triple instead of
  dual colons indicate this difference.
  \begin{code}
  next = sem iterNext ::: ExprTrans.resolve  -- one anonymous clause
           match True = lhs.changes  -- stops when there are no changes
           default subst2  -- pass prev |subst2| into the next iter
  \end{code}
  Finally, we introduce a nonterminal |wrapper|, which forms the root
  of the derivation tree and invokes the visits on the derivation
  for expressions, including again an iteration of the inner loop.
  \begin{code}
  itf Compile  inh expr   :: ExprS
               inh env    :: Env
               syn subst  :: Subst
               syn ty     :: Ty

  compile = sem wrapper :: Compile
  sem wrapper
    child e :: TransExpr = iterInner
    default env expr ty
    iterate resolve of e = next  -- repeat the inner loop
    lhs.subst = e.subst2
  \end{code}

  \subsection{Translation to target expression}
  
  The code so far computes the information needed to translate the
  source expression. The shape of the derivation is determined,
  and after iterations, |subst2| contains the substitution for the
  types. We wrap up with generating the target expression as
  attribute |trans| and collecting the errors.
  \begin{code}
    itf ExprTrans  visit generate
                     inh subst3  :: Subst
                     syn trans   :: ExprT
                     syn errs    :: Errs

    sem exprVar    lhs.trans = VarT lk.nm' -- |lk| delivers the name
    sem exprApp    lhs.trans = AppT f.trans a.trans
    sem exprLam    lhs.trans = LamT loc.u b.trans
    sem exprDeriv  default errs = concat

    itf Compile  syn trans :: ExprT
    sem wrapper  default trans
                 e.subst3 = e.subst2
  \end{code}

  The lookupTy nonterminal delivers the name for a variable.
  The alternatives were constructed in iterations of the
  |resolve| visits, and stored in the |loc.mbDeriv| attribute.
  We take it out and continue from there. From the derivations
  of nonterminal |lkMany|, we pick the name for the first one
  that has |loc.pick| equal to |True|.
  \begin{code}
  itf Lookup  visit resolved
                syn nm'   :: Ident
                syn errs  :: Errs

  sem lookupTy
    lhs.errs  = maybe [Err_unresolved lhs.nm] (const []) lk.mbNm
    lhs.nm'   = maybe lhs.nm id lk.mbNm

  itf LookupMany
    syn mbNm :: Maybe Ident

  sem lkNil   lhs.mbNm = Nothing
  sem lkCons  lhs.mbNm = if loc.pick then Just hd.nm' else tl.mbNm

  itf LookupOne  syn nm' :: Ident       -- use |u| as name
  sem lookupLam  lhs.nm' = outer.loc.u  -- defined in |exprLam|
  \end{code}

  What remains is to invoke the coroutine generated from the
  |compile| nonterminal, with a |ExprS| expressions, to get
  a type and an |ExprT| back. We omit these details.

  \subsection{Discussion}
  
  \paragraph{Performance.}
  Clauses introduce backtracking.
  In the worst case, this leads to a number of traversals exponential
  in the size of the (longest intermediate) tree.
  In practice, clause selection is often a function of some inherited
  attributes (i.e. deterministic), which only requires a constant
  number of traversals over the tree.
  For example, this is the case for |rulerfront| programs expressible in UUAG.
  We verified that programs generated from |rulerfront| are comparable to
  those generated from UUAG, both in time and memory.

%%  When iterating a visit, the programmer controls the number of repetitions
%%  made. We also showed in the example how to control which subtrees to visit.

  \paragraph{Expressiveness.}
  With attributes, we conveniently compute information in one part of the tree
  and transport it to another part, allowing context-dependent decisions to be
  made.
  The notion of visits gives us sufficient control to steer the inference process.

  On the other hand, it is not possible to simply plug a type system in
  |rulerfront| and automatically obtain an inference algorithm. We provide the
  building blocks to write inference algorithms for many type systems, but it
  is up to the programmer to ensure that the result is sound and complete.

  Soundness of a |rulerfront| program is typically easy to prove.
  Completeness, however, is a different issue. That largely depends on decisions
  made about unknown types. With |rulerfront|, we make explicit when choices are
  made, and when visits are repeated. We believe this helps reasoning about
  completeness.
  
    \paragraph{Constraint-based inference.}
    We establish the following relation to constraint-based inference.
    A detached derivation can be seen as a constraint, can be collected in
    an attribute and solved elsewhere.
    Solving constraints corresponds invoking visits (such as |resolve| in Section~\ref{sect.lookups})
    on the derivation, potentially multiple times.

    Solving a constraint may result in more constraints. We store these either in
    a node's state, or collect them in attributes.

    A constraint is typically parametrized with information from the context that
    created it. We provide access to this context via nested nonterminals, which
    have access to the attributes of their outer nonterminals.

%if False
  
  We can improve our approach by disconnecting clause selection from visits.
  Suppose that we specify not visit names in the interface but decision names.
  A decision is a sequence of visits.
  Visits are determined automatically, as well as their attribute allocation.
  Attributes may be constrained explicitly to decisions.
  Clauses are defined on decisions. A backtrack may happen to another clause
  within the same decision.
  This makes it a bit more flexible, without complicating matters too much, and
  does not require the programmer to manually list all visits.
  
  In the beginning of the section we gave a specification in term of type
  rules. What can we do to aid proving soundness and completeness of the
  implementation with respect to that specification?
  Visits represent choice points, hence we can formulate induction hypotheses
  per clause, and write down invariants on attributes of a visit, and make
  the invariant hard enough to prove properties about the resulting
  values of attributes after analysis.
  In that line of thought, dependent types for attributes may be of use to
  produce machine proofs.
  In another line of thought, we can do some steps to make the specification
  more resemble rules. For example, we can type set some of the code in a type rule style, when we have
  a formatting rule per nonterminal (atze's ruler paper). Furthermore, as written in a previous draft
  paper (ruler tutorial/aspect oriented bla), it is easy to write
  match/assert-rules using type-rule-like syntax.
  In general, it's nicer to write equations like attributes though.
  
  When implementing some form of constraint solving, one essential operation in the
  solver is a check if some constraint is already solved. This particular aspect does
  not play a role in the above example. Still, the approach seems suitable for this.
  We can store a partial derivation as first class value together with some meta
  information to identify it in a constraint store. Then take it out and instantiate
  it at multiple places, obtaining sharing of results of previous visits.
  
  Rules for nested nonterminals act as callbacks. They have access to the
  enclosing nonterminal. On the other hand, the enclosing nonterminal has
  no access to the state of the enclosed. Would this be desirable?
  Yes: citation to draft about nested attribute grammars, and presentation.
  Requires static enforcement of visit-order to keep the specification functional.
  
  The above example deals with non-determinism in rule selection. What about non-determinism in
  attributes? We use here the conventional unification and fresh variables to deal with
  those. We can maintain more complex information in the environment about attributes,
  such as constraints. In fact, we can model constraints using nested nonterminals.
  Solving them corresponds to an invocation of visit that improves a substitution.
  
  In fact, we can treat type variables differently. The pattern that we saw is that
  we introduce a variables, then apply an iterative
  process that discovers more information, until no more information is found, then
  a defaulting process starts. In a draft paper, we specified this process with a
  notion of \emph{defer} and \emph{fixate} on premises of a type rule.
  The idea is: we associate a callback (a.k.a. constraint) with a type variable.
  If more is known about the variable, the callback triggers and updates substitution
  or grows a portion of the tree. Otherwise, it triggers a defaulting procedure.
  We made steps towards facilitating the implementation of this pattern.
%endif
  
  
\section{Semantics}
\label{sect.semantics}
  
  %format << = "\llbracket"
  %format >> = "\rrbracket"
  %format ~> = "\leadsto"
  %format (semcl (i) (v) (ys) (z)) = << z >> "_{" i,v,ys "}"
  %format (semt (i) (z)) = << z >> "_{" i "}"
  %format (semtc (i) (ks) (z)) = << z >> "_{" i,ks "}"
  %format (semb (z)) = << z >>
  
  We define |rulercore|, a small core language for Attribute Grammars.  
  We translate a |rulerfront| program in two steps to Haskell. We first 
  desugar |rulerfront| to |rulercore|, then translate the latter to Haskell.
  The separately defined attributes of |rulerfront| are grouped together in
  |rulercore|, visits are ordered, attributes allocated to visits, 
  covariant interfaces translated to normal interfaces, rules
  ordered based on their attribute dependencies, and rules augmented with
  default rules. We omit description of this step, as it is similar to
  the frontend of UUAG~\cite{uuagc}, and of a variation on |rulercore|~\cite{Middelkoop10wgt}.
  Instead, we focus on the translation to Haskell, which precisely defines the
  semantics of |rulercore|, and thus forms the underlying semantics for
  |rulerfront|.
  %% I that is not sufficient, download the UUAG repository and
  %% try to understand the Transform.ag and Order.ag files, because
  %% that contains all there is to know aobut this.
  
  \subsection{Syntax}
  
  %format hty = "\tau"
  The |rulercore| language is Haskell extended with additional syntax
  for toplevel interface declarations, semantic expressions, and attribute
  occurrence expressions. The following grammar lists these syntax extensions.
  \begin{code}
    i  ::=  itf I (many v)                                  -- interface decl, with visits |v|
    v  ::=  visit x inh (many a1) syn (many a2)             -- visit decl, with atributes |a1| and |a2|
    a  ::=  x :: hty                                        -- attribute decl, with Haskell type |hty|

    s  ::=  sem x :: I t                                    -- semantics expr, defines nonterm |x|
    t  ::=  () |  visit x1 chn (many x2) (many r) (many c)  -- visit def, with common rules |r|
    c  ::=  clause x (many r) t                             -- clause definition, with next visit |t|

    r  ::=  p <- e                                          -- assert-rule, evaluates monadic |e|
       |    match p <- e                                    -- match-rule, backtracking variant
       |    invoke x of c <- e                              -- invoke-rule, invokes |x| on |c|, while |e|
       |    attach x of c :: I <- e                         -- attach-rule, attaches a part. eval. child
       |    p = detach x of c                               -- detach-rule, stores a child in an attr

    o  ::=  x.x                                             -- expression, attribute occurrence

    x, I, p, e  -- identifiers, patterns, expressions respectively
  \end{code}
  There are some differences in comparison with the examples of the previous
  section.
  Invocations of visits to children are made explicit through the
  invoke-rule, which also represents the iterate-rule.
  Similarly, the attach rule also takes care of introducing children.
  A visit definition declares number of visit-local chained attributes |many y|,
  and has a number of rules to be evaluated prior to the evaluation of
  clauses. A clause defines the next visit, if any.
  
  The order of appearance of rules determines the evaluation
  order, which allows them to be monadic. Non-monadic expressions are lifted
  with |return|.
  The monad may be any backtracking-monad, such as |Either String|, |Logic|,
  and |IO|. We take |IO| as example.
  
  \subsection{Example}
  
  %format sumCons2
  %format sumNil2
  %format noIterationS = noIteration "_" S
  The following example demonstrates how to to compute
  sum of a list of integers in two visits in |rulercore|.
  \begin{code}
  itf S  visit v1  inh l :: [Int]  syn emptyset  -- decompose list |l| down
         visit v2  inh emptyset    syn s :: Int  -- compute sum |s| up

  sum' =  sem sum :: S
    visit v1 chn emptyset emptyset
      clause sumNil                              -- when list is empty
        match [] <- return lhs.l                 -- match |[] = l|

        visit v2 chn emptyset emptyset           -- no visit-local attrs
          clause sumNil2
            lhs.s <- return 0                    -- empty list, zero sum
            ()                                   -- no next visit
      clause sumCons                             -- when list non-empty
        match (loc.x : loc.xs) <- return lhs.l   -- match |(x:xs) = l|
        attach v1 of tl :: S <- return sum       -- recursive call
        tl.l <- return loc.xs                    -- |l| param of call
        invoke v1 of tl <- noIterationS          -- visit it to pass |l|

        visit v2 chn emptyset emptyset
          clause sumCons2
            invoke v2 of tl <- noIterationS      -- visit it to get the sum
            lhs.s <- return (loc.x + tl.x)       -- sum of |hd| and the |tl|    
            ()                                   -- no next visit
  \end{code}
  
  We translate a |rulerfront| nonterminal to a coroutine, in the
  form of continuations. From
  the interface, we generate a type signature for these coroutines.
  \begin{code}
  type S        = S_v1
  newtype S_v1  = S_v1 ([Int] -> IO ((), (S_v1, S_v2)))
  newtype S_v2  = S_v2 (IO (Int, (S_v2, ())))
  \end{code}
  Inherited attributes become parameters, and synthesized attributes
  are returned as a tuple of results. Each visit also returns two
  continuations. The first continuation represents the current
  visit itself (which may be re-invoked with updated internal state),
  the second continuation represents the next visit (if any).
  
  The coroutine |nt_sum| has |S| as type.
  Attributes are encoded as a variable |childIattr| or |childOattr|,
  depending on whether the attribute is an input or output of the
  clause.
  Clause selection relies on backtracking in the monad. When a
  match-statement doesn't match, a failure is generated in the
  monad, which we |catch| to switch to the next clause.
  %format vis_v1
  %format vis_v2
  %format S_v1
  %format S_v2
  %format lhsIl = lhs "_{" I "}" l
  %format lhsOs = lhs "_{" O "}" s
  %format tlOl  = tl "_{" O "}" l
  %format tlIs  = tl "_{" I "}" s
  %format locLx = loc "_{" L "}" x
  %format locLxs = loc "_{" L "}" xs

  \begin{code}
  sum' = S_v1 vis_v1 where
    vis_v1 lhsIl = (                     -- first clause of visit |v1|
        do  []  <- return lhsIl          -- match on |lhs.l|
            let  r  = S_v1 vis_v1        -- repetition cont.
                 k  = S_v2 vis_v2 where  -- next visit cont.
                   vis_v2 = (                      -- clause of visit |v2|
                       do  lhsOs <- return 0       -- |lhs.s| computation
                           let  r  = S_v2 vis_v2   -- repetition
                                k  = ()            -- no next visit
                           return (lhsOs, (r,k))   -- deliver result |v2|
                     ) `catch` (\_ -> undefined)   -- no other clause for |v2|
            return ((), (r,k))    -- deliver result of visit |v1|
      ) `catch` ( \_ ->           -- second clause (when first clause fails)
        do  (locLx : locLxs)  <- return lhsIl      -- match on |lhs.l|
            tlOl              <- return locLxs     -- inherited attr |tl.l|
            (S_v1 vis_tl_v1)  <- return sum'       -- attach child |tl|
            ((), (_,S_v2 vis_tl_v2)) <- vis_tl_v1 tlOl  -- first visit on |tl|
            let  r  = S_v1 vis_v1                      -- repetition cont.
                 k  = S_v2 vis_v2 where                -- next visit cont.
                   vis_v2 = (                          -- clause of visit |v2|
                       do  (tlIs, (_,_)) <- vis_tl_v2  -- second visit on |tl|
                           lhsOs <- return (locLx + tlIs)    -- |lhs.s|
                           let  r  = S_v2 vis_v2       -- repetition
                                k  = ()                -- no next visit
                           return (lhsOs, (r,k))       -- deliver result |v2|
                     ) `catch` (\_ -> undefined)   -- no other clause for |v2|
            return ((), (r,k)) )  -- deliver result of visit |v1|
  \end{code}
  The above code is slightly simplified. Below, we show the general translation.

  \subsection{Translation}
  
  We use the following naming conventions from |rulerfront| names to Haskell names.
  \begin{code}
  outp "loc"  x  = "locL" x        ^^^^ inp "loc"  x  = "locI" x
  outp "lhs"  x  = "lhsI" x        ^^^^ inp "lhs"  x  = "lhsS" x
  outp c      x  = c "S" x         ^^^^ inp c      x  = c "I" x
  outp y         = "visitS" y      ^^^^ inp        y  = "visitI" y
  vis c x  = "vis_" c "_" x        ^^^^ nt x     = "nt_" x
  vis x    = "vis_" x              ^^^^ ity I x  = I "_" x
  s I x  ^^^^ ^^^^ i I x  -- respectively, inh and syn attrs of |x| of |I|
  \end{code}
  
  From an interface declaration, we generate the types for the coroutines.
%%  We need these types are needed to give a non-cyclic type to the coroutines.
%%  Also, the extra type information causes more informative error messages
%%  when rules contain type errors.
  \begin{code}
  semb (itf I (many v))                       ~>  type ^^^ (semb I) = (semb (ity I x'))  ; many (semt I v)             -- |x'| next visit,
  semt I (visit x inh (many a) syn (many b))  ~>  newtype ^^^ (semb (ity I x)) =                                       -- otherwise |()|
    (semb (ity I x)) (semb (many a) -> IO (semb (many b), (semb (ity I x), semb (ity I x'))))
  \end{code}
  From these interfaces, we actually also generate wrappers to interface with the coroutines
  from Haskell code. The translations for them bear a close resemblance to 
  the translation of the attach and invoke rules below.
  
  The clauses of a visit are translated to a function |(semb (vis x))| that tries the clauses one by one.
  This function takes as parameters the coroutines (|semb chlds|) of the children in scope prior to
  invoking the visit, the
  visit-local attributes |many y|, and the inherited attributes.
  \begin{code}
  semb (sem x :: I t)                                  ~>  let ^^^ (semb (nt x)) = semt I t in semb (nt x)

  semt I (())                                          ~>  ()
  semt I (visit x chn (many y) (many r) (many c))      ~>
    let ^^^  (semb (vis x)) (semb chlds) (semb (inp (many y))) (semb (inp lhs (i I x)))
         = catch (do {semb (many r); semcl I x (many y) (many c)}) undefined  ^^^ in (semb (ity I x)) (semb (vis x))
  \end{code}
  The clauses themselves translate to a sequence of statements, consisting of the translated statements of the
  semantic rules, and the construction of the two continuations. We partially parametrize both continuations
  with the updated children.
  \begin{code}
  semcl I v (many y) []                                ~>  error "no clause applies"
  semcl I v (many y) (clause x (overline r) t : cs)    ~>  
    catch  (do  { semb (many r) ; let { semb (inp x (many y) = outp (many y)) }
                ; let  { r  = (semb (ity I x)) (semb (vis x) (semb chlds) (semb (outp x (many y))))
                       ; k  = (semtc I chlds t) }
                ; return (semb (outp lhs (s I x)), (r,k)) })
           (\_ -> semcl I v (many y) cs)
  
  semtc I ks (())                                      ~>  ()
  semtc I ks (visit x chn (many y) (many r) (many c))  ~>  (semt I (visit x chn (many y) (many r) (many c))) (semb ks) (semb (outp x (many y)))
  \end{code}
  
  Semantic rules translate to monadic statements. For the assert-rule, we match in a let-statement,
  to ensure that a pattern match failure is considered a runtime error, instead of cause backtracking in the monad.
  \begin{code}
  semb (match p <- e)             ~>  semb p <- semb e
  semb (p <- e)                   ~>  x <- semb e; let { semb p = x}    ^^^^ -- |x| fresh
  semb (attach x of c :: I <- e)  ~>  ((semb (ity I x)) (semb (vis c x))) <- semb e
  semb (p = detach x of c)        ~>  let { semb p = (semb (ity I x)) (semb (vis c x)) }
  \end{code}
  
  Invoke invokes a visit |x| (named |f| in the translation) on child |c| once, then repeats invoking it,
  as long as |e| (named |g|) succeeds in feeding it new input.
  %format Ic = I "_{" c "}"
  \begin{code}
  semb (invoke x of c <- e)  ~>  
    (semb (inp c (s Ic x)), (_, k))
      <-   let  iter f (semb (outp c (i Ic x))) = do
                  {  ((semb (coIty Ic x)) g) <- semb e
                  ;  z@(semb (inp c (s Ic x)), ( semb (ity Ic x) f',_))
                       <- f (semb (outp c (i Ic x)))
                  ;  catch  (  do  {  (semb (outp c (i Ic x)), _) <- g (semb (inp c (s Ic x)))
                                   ;  iter f' (semb (outp c (i Ic x))) })
                            (\_ -> return z) }
           in iter (semb (vis c x)) (outp c (i Ic x))
    ; let ((semb (ity Ic x')) (semb (vis c x'))) = k  -- |x'| is next visit, or line omitted
  \end{code}

  Finally, we add bangs around patterns to enforce evaluation, and replace attribute occurrences with
  their Haskell names.
  \begin{code}
  semb (C (many p))  ~> !(C (many (semb p))) 
  semb ((p,..,q))    ~> !(semb p,..., semb q)
  semb (c.x)         ~> !(semb (inp c x))

  semb e             ~> e [ c.x := semb (outp c x) ]
  \end{code}

  The translation exhibits a number of properties. If the |rulerfront| or |rulercore| program is
  well typed, then so is the generated Haskell program, and vice versa. Further investigation requires
  a discussion of |rulerfront|'s type system, which we omit for reasons of space.
  Furthermore, the translation is not limited to Haskell. A translation similar to above can be given
  for any language that supports closures.

  %% perhaps, should also mention that the io monad is used only for the implementation. The
  %% ag program itself is still purely functional, unless side effect is wanted.
  %% perhaps mention too that this can be nicier encoded with a combination of the LogicT monad
  %% and the Control.Coroutine monads, athough they cannot be combined in their present states.


\section{Related Work}
\label{sect.visit.relatedwork}

  Attribute grammars as defined by Knuth~\cite{DBLP:journals/mst/Knuth68} are extensions of
  context free grammars.
  Typically, the tree is the parse tree determined a priori by a parser.
  For typing relations that are not syntax directed,
  the derivation tree is not known beforehand, which conflicts with the attribute grammar
  model.
  
  \paragraph{Tree manipulations.}
  There are many extensions to attribute grammars to facilitate changing the tree during
  attribute evaluation.
  Silver~\cite{DBLP:journals/entcs/WykBGK08}, JastAdd~\cite{DBLP:conf/oopsla/EkmanH07} and
  UUAG~\cite{uuagc} support higher-order attribute grammars~\cite{DBLP:conf/pldi/VogtSK89}.
  These grammars allow the tree to be extended with subtrees computed from attributes, and subsequently
  decorated. The responsibility of selecting a production of a higher-order child lies with the
  parent of that child, and the choice is final.
  In |rulerfront|, a child itself selects a clause to make a choice, and a choice can be made
  per visit.
  
  JastAdd and Aster~\cite{DBLP:conf/cc/KatsSV09}, support conditional rewrite rules, which allows rigorous
  changes to be made to the tree. Coordination between rewriting and attribute evaluation
  is tricky due to mutual influence, especially if the transformations are not confluent.
  To limit interplay, JastAdd's rewriting of a tree is limited to the first access of that
  tree, and choices finalized.

  Many type inference algorithms, especially for type and effect systems, iteratively
  traverse the tree. Some algorithms
  construct additional subtrees during this process.
  Circular Attribute Grammars~\cite{DBLP:journals/toplas/Jones90}, supported by JastAdd and Aster,
  iteratively compute circular attributes until a fixpoint is reached.
  UUAG and Silver can deal with circularity via lazy evaluation with streams.
  CAGs, however, do not support changes to the tree during these iterations.
  Stratego's rewrite mechanism that underlies Aster, however, is more general and can change
  the tree.
  In |rulerfront|, a visit may be iterated several times. Each node in the derivation
  tree can maintain a per-visit state to keep track of newly constructed parts of
  the tree.

  \paragraph{Non-deterministic trees.}
  The attribute grammar systems above have in common that they massage a tree until it
  has the right form. Alternatively, a tree can be constructed non-deterministically,
  using e.g. logic programming languages.
  The grammar produces only the empty string, and the semantic rules disambiguate the
  choice of productions.
  \citet{DBLP:journals/ibmrd/Arbab86} showed how to translate attribute grammars to Prolog.
  However, this approach does not allow the inspection of partial |LookupOne|
  derivations of Section~\ref{sect.lookups}, nor the defaulting, to be implemented
  easily.
  With |rulerfront|, we offer non-deterministic construction of the tree per
  visit. The notion of a visit provides an intuitive alternative for the
  |cut| operator.

  Prolog-like approaches also offer unification mechanisms to deal
  with non-determinism in attribute computations. In contrast, we
  require the programmer to either program unifications and substitutions manually,
  or use a logic monad combined with a unification in the translation of Section~\ref{sect.semantics}.

%%  Arguably, some manual intervention is required, for example to implement
%%  the defaulting mechanism in Section~\ref{sect.lookups}. In this example,
%%  substitutions of ambiguous lookup-derivations were not directly
%%  incorporated in the main substitution.
%%  A memoization facility to cache the results of children, however, has to be
%%  written explicitly in |rulerfront|.

  \citet{DBLP:journals/jacm/EngelfrietF89} shows the expressiveness of classes of attribute grammars.
  Unsurprisingly, deterministic AG evaluators have lower computational complexity bounds compared to
  non-deterministic ones. With |rulerfront|, we target
  heavy compilers (i.e. UHC), that processes large abstract syntax trees, thus we need the control
  on the non-determinism that visits offer.

  \paragraph{Related attribute grammar techniques.}

  Several attribute grammar techniques are important to our work.
  \citet{DBLP:journals/acta/Kastens80} introduces ordered attribute
  grammars. In OAGs, the evaluation order of attribute
  computations as well as attribute lifetime can be determined statically,
  allowing severe optimizations.
%%  Underlying to our work is the concept of |k|-visit attribute grammars~\cite{DBLP:journals/mst/RiisS81}.
%%  Related is \citet{DBLP:conf/popl/KennedyW76}.

  \citet{DBLP:journals/toplas/Boyland96} introduces conditional attribute grammars.
  In such a grammar, semantic rules may be guarded. Our clauses-per-visit model
  provides an easier yet less flexible alternative.

  \citet[chap. 3]{Saraiva99} describes multiple traversal functions
  (or visit functions~\cite{DBLP:conf/ifip2-4/SwierstraA98}).
  These visit functions are one-shot continuations, or
  coroutines without looping. We improved upon this mechanism to
  support iterative invocation of visits, thus encoding coroutines
  with loops.

\section{Conclusion}
\label{sect.visit.conclusion}

  We presented |rulerfront|, a conservative extension of ordered
  attribute grammars, intended to describe algorithms for type
  inferencing, evaluators and code generators.
  We explained this language by example in
  Section~\ref{sect:casestudy} and described its semantics
  in Section~\ref{sect.semantics}. It has three distinct features.

  Firstly, in contrast to most attribute grammar systems, construction of a
  derivation tree and the evaluation of its attributes is intertwined
  in |rulerfront|. This allows us to define a grammar for the language
  of derivations of some typing relations, instead of being limited to
  the grammar of expressions or types.

  Secondly, we use the notion of explicit visits to capture the
  gradual, side effectful nature of type inference. Each visit
  corresponds to a state transition of the derivation tree
  under construction. These visits may be repeated to form
  fixpoint iterations.

  Thirdly, many inference algorithms reason about what part of the
  derivation is known, or is still pending, e.g. by means of
  constraints. In |rulerfront|, derivation trees are first class
  and can be inspected by visiting them, which facilitates such
  reasoning in terms of attributed trees.

  As future work, we started a project to describe UHC's type inference
  algorithm as attribute grammar with |rulerfront|. With |rulerfront|,
  we can express unification and context reduction, which paves the
  way for a full description of UHC's inference algorithm with attribute
  grammars.

\acks
This work was supported by Microsoft Research through its European PhD Scholarship Programme.

  \bibliographystyle{abbrvnat}
  \begin{thebibliography}{23}
  \providecommand{\natexlab}[1]{#1}
  \providecommand{\url}[1]{\texttt{#1}}
  \expandafter\ifx\csname urlstyle\endcsname\relax
    \providecommand{\doi}[1]{doi: #1}\else
    \providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi

  \bibitem[Arbab(1986)]{DBLP:journals/ibmrd/Arbab86}
  B.~Arbab.
  \newblock {Compiling Circular Attribute Grammars Into Prolog}.
  \newblock \emph{IBM Journal of Research and Development}, 30\penalty0
    (3):\penalty0 294--309, 1986.

  \bibitem[Boyland(1996)]{DBLP:journals/toplas/Boyland96}
  J.~T. Boyland.
  \newblock {Conditional Attribute Grammars}.
  \newblock \emph{ACM Transactions on Programming Languages and Systems},
    18\penalty0 (1):\penalty0 73--108, 1996.

  \bibitem[Dijkstra and Swierstra(2004)]{DBLP:conf/afp/DijkstraS04}
  A.~Dijkstra and S.~D. Swierstra.
  \newblock {Typing Haskell with an Attribute Grammar}.
  \newblock In \emph{AFP}, pages 1--72, 2004.

  \bibitem[Dijkstra and Swierstra(2006)]{DBLP:conf/flops/DijkstraS06}
  A.~Dijkstra and S.~D. Swierstra.
  \newblock {Ruler: Programming Type Rules}.
  \newblock In \emph{FLOPS}, pages 30--46, 2006.

  \bibitem[Dijkstra et~al.(2009)Dijkstra, Fokker, and
    Swierstra]{DBLP:conf/haskell/DijkstraFS09}
  A.~Dijkstra, J.~Fokker, and S.~D. Swierstra.
  \newblock {The Architecture of the Utrecht Haskell Compiler}.
  \newblock In \emph{Haskell}, pages 93--104, 2009.

  \bibitem[Ekman and Hedin(2007)]{DBLP:conf/oopsla/EkmanH07}
  T.~Ekman and G.~Hedin.
  \newblock {The JastAdd Extensible Java Compiler}.
  \newblock In \emph{OOPSLA}, pages 1--18, 2007.

  \bibitem[Engelfriet and Fil{\'e}(1989)]{DBLP:journals/jacm/EngelfrietF89}
  J.~Engelfriet and G.~Fil{\'e}.
  \newblock {Passes, sweeps, and visits in attribute grammars}.
  \newblock \emph{Journal of the ACM}, 36\penalty0 (4):\penalty0 841--869, 1989.

  \bibitem[Fokker and Swierstra(2009)]{DBLP:journals/entcs/FokkerS09}
  J.~Fokker and S.~D. Swierstra.
  \newblock {Abstract Interpretation of Functional Programs using an Attribute
    Grammar System}.
  \newblock \emph{ENTCS}, 238\penalty0 (5):\penalty0 117--133, 2009.

  \bibitem[Hudak et~al.(1992)Hudak, Jones, Wadler, Boutel, Fairbairn, Fasel,
    Guzm{\'a}n, Hammond, Hughes, Johnsson, Kieburtz, Nikhil, Partain, and
    Peterson]{DBLP:journals/sigplan/HudakPWBFFGHHJKNPP92}
  P.~Hudak, S.~L.~P. Jones, P.~Wadler, B.~Boutel, J.~Fairbairn, J.~H. Fasel,
    M.~M. Guzm{\'a}n, K.~Hammond, J.~Hughes, T.~Johnsson, R.~B. Kieburtz, R.~S.
    Nikhil, W.~Partain, and J.~Peterson.
  \newblock {Report on the Programming Language Haskell, A Non-strict, Purely
    Functional Language}.
  \newblock \emph{SIGPLAN Notices}, 27\penalty0 (5):\penalty0 1--, 1992.

  \bibitem[Jones(1990)]{DBLP:journals/toplas/Jones90}
  L.~G. Jones.
  \newblock {Efficient Evaluation of Circular Attribute Grammars}.
  \newblock \emph{ACM Transactions on Programming Languages and Systems},
    12\penalty0 (3):\penalty0 429--462, 1990.

  \bibitem[Kastens(1980)]{DBLP:journals/acta/Kastens80}
  U.~Kastens.
  \newblock {Ordered Attributed Grammars}.
  \newblock \emph{Acta Informatica}, 13:\penalty0 229--256, 1980.

  \bibitem[Kats et~al.(2009)Kats, Sloane, and Visser]{DBLP:conf/cc/KatsSV09}
  L.~C.~L. Kats, A.~M. Sloane, and E.~Visser.
  \newblock {Decorated Attribute Grammars: Attribute Evaluation Meets Strategic
    Programming}.
  \newblock In \emph{CC}, pages 142--157, 2009.

  \bibitem[Kennedy and Warren(1976)]{DBLP:conf/popl/KennedyW76}
  K.~Kennedy and S.~K. Warren.
  \newblock {Automatic Generation of Efficient Evaluators for Attribute
    Grammars}.
  \newblock In \emph{POPL}, pages 32--49, 1976.

  \bibitem[Knuth(1968)]{DBLP:journals/mst/Knuth68}
  D.~E. Knuth.
  \newblock {Semantics of Context-Free Languages}.
  \newblock \emph{Mathematical Systems Theory}, 2\penalty0 (2):\penalty0
    127--145, 1968.

  \bibitem[Middelkoop et~al.(2010{\natexlab{a}})Middelkoop, Dijkstra, and
    Swierstra]{Middelkoop10ifl}
  A.~Middelkoop, A.~Dijkstra, and S.~D. Swierstra.
  \newblock {Towards Dependently Typed Attribute Grammars}.
  \newblock \url{http://people.cs.uu.nl/ariem/ifl10-depend.pdf},
    2010{\natexlab{a}}.

  \bibitem[Middelkoop et~al.(2010{\natexlab{b}})Middelkoop, Dijkstra, and
    Swierstra]{Middelkoop10wgt}
  A.~Middelkoop, A.~Dijkstra, and S.~D. Swierstra.
  \newblock {Iterative Type Inference with Attribute Grammars}.
  \newblock \url{http://people.cs.uu.nl/ariem/wgt10-journal.pdf},
    2010{\natexlab{b}}.

  \bibitem[Saraiva(2002)]{DBLP:conf/gpce/Saraiva02}
  J.~Saraiva.
  \newblock {Component-Based Programming for Higher-Order Attribute Grammars}.
  \newblock In \emph{GPCE}, pages 268--282, 2002.

  \bibitem[Saraiva and Swierstra(1999)]{Saraiva99}
  J.~A. B.~V. Saraiva and S.~D. Swierstra.
  \newblock {Purely Functional Implementation of Attribute Grammars}.
  \newblock Technical report, Universiteit Utrecht, 1999.

  \bibitem[Swierstra and Alcocer(1998)]{DBLP:conf/ifip2-4/SwierstraA98}
  S.~D. Swierstra and P.~R.~A. Alcocer.
  \newblock Attribute grammars in the functional style.
  \newblock In \emph{Systems Implementation 2000}, pages 180--193, 1998.

  \bibitem[{Universiteit Utrecht}(1998)]{uuagc}
  {Universiteit Utrecht}.
  \newblock {Universiteit Utrecht Attribute Grammar System}.
  \newblock \url{http://www.cs.uu.nl/wiki/HUT/AttributeGrammarSystem}, 1998.

  \bibitem[v.~Wyk et~al.(2008)v.~Wyk, Bodin, Gao, and
    Krishnan]{DBLP:journals/entcs/WykBGK08}
  E.~v.~Wyk, D.~Bodin, J.~Gao, and L.~Krishnan.
  \newblock {Silver: an Extensible Attribute Grammar System}.
  \newblock \emph{ENTCS}, 203\penalty0 (2):\penalty0 103--116, 2008.

  \bibitem[Viera et~al.(2009)Viera, Swierstra, and
    Swierstra]{DBLP:conf/icfp/VieraSS09}
  M.~Viera, S.~D. Swierstra, and W.~Swierstra.
  \newblock {Attribute Grammars Fly First-class: how to do Aspect Oriented
    Programming in Haskell}.
  \newblock In \emph{ICFP}, pages 245--256, 2009.

  \bibitem[Vogt et~al.(1989)Vogt, Swierstra, and Kuiper]{DBLP:conf/pldi/VogtSK89}
  H.~Vogt, S.~D. Swierstra, and M.~F. Kuiper.
  \newblock {Higher-Order Attribute Grammars}.
  \newblock In \emph{PLDI}, pages 131--145, 1989.

  \end{thebibliography}

%%  \bibliography{references}

\end{document}