Each chapter has its own related work section. In this section we consider work that is
related to the thesis as a whole.

\subsection{Circular AGs and Exposure of Intermediate States}
Evaluation algorithms for circular
AGs~\citep{DBLP:journals/toplas/Jones90,DBLP:journals/scp/MagnussonH07}
provide an alternative way to extend the AG evaluation algorithm.
For circular AGs, the algorithm is parametrized with an initial value for cyclic
attributes, which are called gate attributes by \citet{Walz:1989:EAG:76225}.
The algorithm describes a repeated attribute evaluation to compute a fixpoint for the
cyclic attributes. When used in the context of this thesis,
such attributes thus expose intermediate states of the derivation
tree during evaluation.

Fixpoint iteration is one of many evaluation strategies (Section~\ref{intro.sect.inference}).
For example, several type systems use an algorithm that describes the exploration of
multiple candidate derivation trees (Chapter~\tref{chapt.breadthfirst}).
Moreover, to expose the intermediate states of the derivation tree as an attribute,
attributes at various locations of the tree have to be explicitly stored into and obtained
from this attribute\footnote{Such an attribute models a heap in a similar way as a substitution
models memory.}, which is cumbersome and destroys
modularity. Our extensions generalize over fixpoint iteration and many other common techniques
employed by inference algorithms.


\subsection{Inference Rules}

\citet{Glesner98usingmany-sorted} shows a mapping from syntax directed
inference rules to AGs. Similar to Ruler, relations defined by syntax directed rules are
mapped to nonterminals, syntax directed rules to productions, and judgments of such relations
to children of a production. Judgments of rules that are not syntax directed are mapped to
an AG rule that employs a hull algorithm to construct a derivation tree.
Only one of the rules may be applicable at a given time, and the domain of the parameters
of the relation must be finite.
While suitable for type checking, this approach does not suffice for type inference, as multiple
rules may be applicable, and it may be necessary to postpone solving the judgment when insufficient
type information is available.

Typol~\citep{DESPEYROUX:1988:INRIA-00070072:1} is another language for the specification
of inference rules with a mapping to Prolog. \citet{ATTALI:1994:INRIA-00077110:1} show
how to identify a subclass of Typol that can be mapped to an efficient AG implementation.
Since this class consists effectively of syntax directed rules, this approach is too
restrictive for the implementation of type inference.

\subsection{Proof Assistants}
Proof assistants such as Isabelle/HOL~\citep{DBLP:conf/tphol/WenzelPN08},
Twelf~\citep{DBLP:conf/tphol/Schurmann09}, and
Sparkle~\citep{Mol:2001:TPF:647980.743393} and
Coq~\citep{DBLP:journals/corr/abs-cs-0603118} can be used to formalize
a type system and inference algorithm, and prove various consistency
properties between specification and implementation. Typically, the
formalized inference algorithm can be extracted to code in some target
language.
Such an approach is possible for small type systems as encountered in
theory, but does not scale up when dealing with practical, full-blown type
systems of large languages\footnote{
  As demonstrated by \citet{DBLP:journals/jfp/Faxen02}, a type system for
  Haskell'98 is already large and complex.
}.

In Coq, but also in other dependently typed languages
such as Agda~\citep{DBLP:conf/tldi/Norell09},
Epigram~\citep{DBLP:conf/afp/McBride04}, and
IDRIS~\citep{Brady:2011:ISP:1929529.1929536}, properties of type
system can be expressed as types of the inference algorithm.
To do so, the inference algorithm needs to be implemented,
and structured so that it can be complemented with proofs of
properties, such as type soundness.
In this thesis, we consider type systems for which the
first task is already difficult, and the second task infeasible
in practice. Thus, such approaches are out of the scope of this
thesis. However, we consider dependently typed languages in
Chapter~\tref{chapt.dependent-ags}.

Closer to the goals expressed in this thesis are the
languages Ott (Section~\ref{sect.intro.ott}) and
TinkerType (Section~\ref{sect.intro.tinkertype}).

%% OTT?  http://moscova.inria.fr/~zappa/readings/wmm10.pdf
%% SassyLF? http://www.cs.cmu.edu/~aldrich/SASyLF/fdpe08.pdf
\subsection{Ott}
\label{sect.intro.ott}

Ott~\citep{DBLP:conf/icfp/SewellNOPRSS07} and SASyLF~\citep{Aldrich:2008:SEP:1411260.1411266}
are meta languages in which formal semantics such as type systems can be formalized.
Similar to Ruler~\citep{DBLP:conf/flops/DijkstraS06}, these languages provide special syntax
for inference rules, and require the rules to be well-formed. In contrast to Ruler, the purpose
of these languages is to aid the construction of proofs. From an Ott-description, boilerplate
code for several proof assistants (e.g., Coq) can be generated. This boilerplate code consists
of parsers for concrete syntax, abstract syntax, and substitution lemmas.

\paragraph{Concrete and Abstract Syntax.}
The following is specification of a grammar for a variant of the lambda calculus
with tuples in Ott\footnote{
  For presentation purposes, the examples use a slightly different notation than provided by Ott.
}. Such a grammar consists of three types of symbols:
meta variables, nonterminals and terminals. Meta
variables are nonterminals that can be substituted and alpha-renamed. Nonterminals
are introduced by the grammar. The remaining symbols that occur in the grammar are
considered terminals.
Occurrences of a nonterminal may take a subscript to distinguish multiple
occurrences of the same nonterminal from each other.
\begin{verbatim}
metavar x
grammar  e ::=                  :: Expr
           |    x               :: Var
           |    \ p . e         :: Lam :: bind b(p) in e
           |    e1 e2           :: App
           |    ( e )           :: _

         p ::=                  :: Pat
           |    x               :: Var :: b = {x}
           |    (p1, ..., p.n)  :: Tup :: b = b(p1) ... b(p.n)
\end{verbatim}
The grammar specifies a concrete syntax to the left of the
double colon, and the constructor for the abstract syntax to
the right. The production for parentheses is considered a
meta-production and is not reflected in the abstract syntax.

An important concept of Ott is \emph{binding}. After the
second double colon, \emph{binders} for meta variables
can be specified, as well as their scope.
The expression @b(p)@ represents the set of meta variables
defined by the synthesized attribute @b@ of @p@. Zero or more
synthesized attributes may be specified for a nonterminal.
The binder @bind b(p) in e@ for the lambda production
denotes that the meta variables @b(p)@ are bound at this
lambda, and are in scope of |e|.
Lemmas for substitution and alpha equivalence, as well
as a definition of free variables are derived from
the binder annotations.
The underlying mechanism ensures through alpha renaming
that meta variables are not accidentally captured by
substitutions.

Ott has a notion of list forms, which is convenient syntax to
represent the common overbar notation that is used grammars and type
rules. Triple dots can be used to construct list patterns, list
expressions, and lists of judgments. For example @b(p1) ... b(p.n)@
is a list expression, where @n@ is an index variable.
Also, list comprehensions and projections of list items can be used.

\paragraph{Inference Rules.}
Judgements can refer to relations defined in Ott via type rules, or
to externally defined functions and relations in the target language.
For example, to model a call-by-value operational semantics, the
following code fragment represents beta reduction.
\begin{center}
\begin{verbatim}
defn  e1 --> e2 :: reduce

                  isValue e2
  ---------------------------------------- :: call-by-value beta
           (\x.e1) e2  -->  {e2/x} e1
\end{verbatim}
\end{center}
The @defn@ line specifies the syntax of the @reduce@
judgments, and is followed by the inference rules for
that relation.
The premise judgments occur above the horizontal line and
conclusion judgments below. The infrastructure for the
substitution @e2/x@ is derived from the binder specification
of @e1@.
The inference rules are translated to axioms in the target
language for the reduction relation.

\paragraph{Discussion.}
Approaches such as Ott aid formal reasoning about type
systems, and thus pursuit a different goal than the derivation
of type-inference implementations from specifications.
On the other hand, Ott and Ruler share the common goal of
formalizing type systems and specifying properties.
Certain concepts are also beneficial to AGs. Binding and
scoping is very common, so the concept of binding may be
very useful for AGs as an abstraction for name
analysis. Similarly, list forms would benefit AGs when
using higher-order children (Section~\ref{intro.sect.higherorder}).


\newcommand\TinkerType{TinkerType}
\newcommand\TinkerTypeAssembler{TinkerType Assembler}

%% \section{\TinkerType}
  \subsection{\TinkerType}
  \label{sect.intro.tinkertype}

  \TinkerType{}~\citep{DBLP:journals/jfp/LevinP03} is a language for the modular description of whole families of
  formal systems, with a focus on type systems and operational semantics. A type
  system is described in two ways. A system is described intensionally as a set of {\it features}.
  These features are names for abstract properties of a type system. A system is described intentionally as a
  set of {\it clauses}. In TinkerType, a clause is a denotation of a type rule in the form of \LaTeX{} text
  or ML code.

  %% \subsection{Overview}
  \paragraph{Overview.}
  A \TinkerType{} description consists of a number of elements: features,
  dependencies between features, clauses, a clause refinement relation, and
  feature constraint formulas. With the latter two elements, clause
  refinement and feature constraints, a partial consistency between type systems
  can be expressed.

  Distinct type systems have different clauses. However, type systems with
  similar features tend to have similar clauses. The relation between clauses
  is exploited by \TinkerType. A \TinkerType{} description therefore contains
  a whole repository of named clauses that are tagged with a number of feature names.
  Clauses with different feature sets can have the same name.
  Given a number of features, a type system is then assembled by the
  \TinkerTypeAssembler{} by selecting the
  clauses that support these features best, which are the clauses where the
  provided feature set is a subset of the requested feature set. Duplicately
  tagged clauses are filtered out. The clause with the largest feature set is retained.

  A dependency relation must be specified between features. A type system
  is fully defined by the transitive closure of the dependency relation on the
  set of features of the type system. Some combinations of features give an
  unsound type system, or the inference algorithm is incomplete.
  Certain combinations of features
  can be declared as deficient using feature constraint formulas. These are propositional
  formulas over features that must be satisfied with the features mapped to
  truth-values based on their presence in the type system. The dependency
  relation between features is one form of such a feature constraint formula,
  in the form of an implication.

  %%\subsection{Code Assembly}
  \paragraph{Code Assembly.}
  The code repository consists of {\it components}, which represents several
  clauses and support code. For example, the following fragment~\citep{DBLP:journals/jfp/LevinP03}
  contains ML code that deals with the type checking of conditional and boolean
  expressions.
  \begin{verbatim}
  component bool, typing {
    parsing { ... }
    ast { ... }
    core {
      typeof {
        header {# let rec typeof gam t = match t with #}
        separator {#| #}

        T-If
          {#TmIf(e1,e2,e3) ->
            if equiv gam (typeof gam e1} TyBool
            then let res = typeof gam e2 in
              if equiv res (typeof gam e3)
              then res
              else error "branches differ in type"
            else error "guard is not a boolean"#}
  } } }
  \end{verbatim}
  The level of granularity of features is actually per component instead of per
  clause. A component consists of several sections related to parsing, abstract
  syntax tree representation, and the actual typing relations with their
  clauses.

  The assembling process is essentially based on concatenating and substituting
  strings.
  The components that match the
  requested features are merged, and the produced code consists of the @header@
  followed by the clauses in verbatim, which are separated by the @separator@.

  Consider a component with subtyping @sub@ as additional feature:
  \begin{verbatim}
  component bool, typing, sub {
    core {
      typeof {
        T-If
          {#TmIf(e1,e2,e3) ->
            if [[subtype]] gam (typeof gam e1} TyBool
            then [[join (typeof gam e2) (typeof gam e3)]]
            else error "guard is not a boolean"#}
  } } }
  \end{verbatim}
  In another component with feature @sub@, the functions @subtype@ and @join@ are
  defined, which can thus be used in the above component.

  The refinement relation between clauses is expressed by means of double bracket
  annotations in the source code. The fragments inside the double brackets are
  considered new, the fragments outside the double brackets must occur verbatim in the
  refined clause.

  \paragraph{Discussion.}
  \TinkerType{} is modular in the sense that all clauses can be written
  separately, and the system enforces that clauses are designed with reuse of
  concepts in mind. A clause can only be
  reused verbatim. In practice, additional material needs to be added to a
  clause, for example, due to extra judgments or due to extra parameters to the
  judgments when supporting extra features. This leads to code duplication in
  the clauses with the usual engineering problems as a consequence. The static
  checks on clause refinement, however, are likely to catch errors resulting from
  incomplete code modifications, and encourage writing clauses as increments of
  each other.

  As discussed above, some forms of consistency are expressed between clauses of
  different type systems, which is enforced by means of consistency checks that point
  to errors in the code. To make these checks effective, there must be a lot
  of overlap between clauses, and thus an extensive set of features with a
  fine granularity. Consistency is not expressed between clauses of the same type
  system. There is no guarantee that the collection of clauses results in compilable
  ML code or \LaTeX{} text, nor that the ML code is in any way related to the
  \LaTeX{} text.

\subsection{Overview of Recent Attribute Grammar Systems}
\label{intro.ag.recent}

  An in-depth exploration of AG systems is out of the scope of this thesis.
  We give some of the distinguishing features of current AG systems.
  Most current AG systems support a wide range of features including
  higher-order attributes~\citep{DBLP:conf/pldi/VogtSK89}
  and collection attributes~\citep{10.1109/SCAM.2007.13}.

  The Lrc~\citep{springerlink:10.1007/BFb0026440} is one of the few current
  AG systems that is based on ordered attribute evaluation. Its distinguishing
  feature is incremental evaluation.
  It has been used as vehicle for research in parallel evaluation and
  the generation of interactive programming environments.
  Lrc generates Haskell and C code, although it is not actively
  maintained anymore.

  UUAG~\citep{uuagc} can be regarded as a simplified reimplementation of
  Lrc, starting originally by piggybacking heavily Haskells lazy evaluation.
  Currently, UUAG supports ordered and
  demand-driven evaluation. Features such as incremental and parallel evaluation
  are being investigated, as well as first-class attribute grammars~\citep{DBLP:conf/icfp/VieraSS09}.

  The AG systems that we consider below are based on demand-driven attribute evaluation.
  These systems support reference attributes~\citep{DBLP:journals/scp/MagnussonH07}
  which allow attributes to be defined and accessed from non-local nodes.
  Data-flow analyses with circular attributes are an application of reference attributes~\citep{Farrow:1986:AGF:12276.13320}.

  Silver~\citep{DBLP:journals/entcs/WykBGK08} supports forwarding~\citep{forwarding} as
  distinguishing feature. Forwarding is a convenient notation for
  desugaring with higher-order children (Section~\ref{intro.sect.higherorder}) in combination with specialized
  copy rules (Section~\ref{intro.sect.copyrules}).
  With first-class AGs, \citet{DBLP:conf/icfp/VieraSS09} implement a more advanced form of
  forwarding.

  Silver also supports the specification of a (control-flow) graph structure on top of the
  AST~\citep{VanWyk:2007:UVD:1279007.1279138}. A production may specify CTL formula which are checked against the graph structure.
  This way, control-flow analyses can be implemented conveniently in attribute grammars (see also \citet{ariem-ext-graph}).

  JastAdd~\citep{DBLP:conf/oopsla/EkmanH07} has rewrite rules as distinguishing feature.
  Rewrite rules are applied to a tree upon the first access through demand-driven
  evaluation and can conditionally depend on attribute values.

  %% \paragraph{Eli}


%if False
\section{Door Attribute Grammars}

  A Door Attribute Grammar~\citep{DBLP:conf/cc/Hedin94} provides programming model
  for remote attributes. It introduces a different kind
  of AST node, called a \emph{door node}. These nodes do not have children, and
  carry not syntactic content. Their sole purpose is to serve as interface to
  attributes of a door node defined elsewhere in the AST. Only the equations of
  a door object may deference attributes of a remote node.

  The door nodes restrict programmers to deal with remote attributes separately
  from conventional attributes. This makes explicit what data is exchanged
  between remote locations, and how this data is derived from local data of
  these locations.

  Like any mechanism for remote attributes, door nodes provides a convenient
  mechanism to deal with symbol tables. Instead of storing concrete data in
  a symbol table, only a reference to the door node is stored. Data defined
  at a declaration site can then easily be accessed at a definition site.

  The author gives an algorithm for Door Attribute Grammars. This algorithm
  maintains a runtime dependency graph between attributes.
  Door nodes gives rise to dependencies to other
  door nodes. During evaluation of equations of door nodes, more dependencies
  arise when remote attributes are dereferenced. Attributes are evaluated on
  demand, in such a way that dependencies are evaluated first. The behavior in
  case of cyclic dependencies is not specified.
%endif