%format x0
%format y0
%format z0
%format x1
%format y1
%format z1
%format x2

\chapter{Conclusion}
\label{chapt.conclusion}

  This thesis presented several extensions to attribute grammars. With these
  extensions, complex type inference algorithms can be expressed.
  When viewed from a high level perspective, this thesis explored notation
  that allows units of evaluation in
  an AG to be made explicit, to be annotated, and to be controlled.
  More concretely, we regard type inference as the simultaneous construction
  of a derivation tree and the evaluation of the tree's attributes.
  In an inference algorithm, attribute evaluation and tree construction take turns.
  The construction of a derivation tree thus introduces the notion of phasing.
  Certain attributes must be evaluated to decide on the structure of the
  tree. We provided several examples, in particular in Chapter~\tref{chapt.iterative}.

  %if False
  For example, to describe some inference algorithm,
  as a first phase of type inference of an expression,
  we may collect all constraints on type variables that are introduced in that
  expression. As a second phase, we generalize over those type variables
  that we discovered to be unconstrained in the first phase.
  %endif

  With our extensions, we organize the evaluation of attributes in
  phases, which makes
  explicit in what state the tree is before and after the evaluation of a
  phase. We showed how to exploit this additional information
  to encode fixpoint computations and search algorithms.
  Although we focussed on type inference, our extensions are actually making
  it possible to describe complex tree walking automata.

  \section{Addressed Challenges}
  We briefly restate the challenges as mentioned in the instruction.
  A declarative specification of a type system is used for formal reasoning
  and explanation. An inference algorithm describes how to infer admissible
  types for a program. The former is therefore an implementation of the latter.
  To show that an inference algorithm is indeed an implementation, it is desirable
  to have a proof that it is consistent with the type system.

  As discussed in Section~\ref{intro.sect.motivation},
  it is a non-trivial exercise to construct an inference algorithm
  for languages such as Haskell (with extensions), which integrate several
  cross-cutting type systems. In this setting, a formal specification (if it exists at all)
  and the implementation are complex,
  which makes it hard to keep both consistent, let alone proof that this is the case.
  Moreover, such an implementation changes continuously to support
  more language features or to use different implementation techniques,
  thus it is likely to be inconsistent.
  The apparent inconsistency leaves a big gap between theory and
  practice. With this thesis, we worked towards a solution where the
  gap is closed by specifying a formal type systems that contain sufficient
  algorithmic details to be executable.

  A question that arose is what execution model to associate with type rules.
  Despite the absence of a general inference
  algorithm that fits any type system (Section~\ref{intro.sect.inference}), most
  inference algorithms are a complex composition of standard inference
  techniques. An executable specification thus describes how to tailor these
  algorithms to the type system.
  In this thesis, we zoomed in on the description of such underlying algorithms.

  Previous work on the language Ruler posed an initial solution.
  Ruler is a language in which syntax-directed,
  algorithmic type rules can be described, which in combination with some additional
  annotations can be translated automatically to AGs (Section~\ref{intro.sect.ruler}).
  Type rules coincide with productions, and metavariables with attributes.
  The inference algorithm is thus expressed as the evaluation of AGs.

  For a declaratively specified type system, type inference for
  declarative aspects boils down to inferring the structure of the derivation tree
  and inferring instantiations for non-functionally constrained meta variables.
  Higher-order AGs withstanding, AGs assume an apriori fixed tree, and require
  functional definitions for attributes. Therefore, an inference algorithm for
  declarative type rules cannot be obtained via a straightforward translation to
  attribute grammars.
  We addressed this issue in this thesis by extending the AG language to
  cater for several inference strategies, and mechanism to combine these strategies.

  %%\paragraph{Solutions.}
  \section{Solutions}

  As initial setting, we showed that we can model an AG on type derivation trees
  instead of parse trees. To deal with non-functional attributes such as types, we
  used a conventional unification-based strategy with an additional threaded substitution
  attribute (Section~\tref{intro.sect.ag.dhm}),
  and expressed unifications in the AG in a declarative manner using
  higher-order children (Section~\tref{sect.intro.hochildrencopyrules}). The substitution
  in combination with placeholders in types
  makes the relations on types functional. Moreover, the implementation of
  the higher-order child expresses the standard unification algorithm, and the
  threading of the substitution its algorithmic coordination, since the
  threading defines the relative order of the unifications and other operations
  that depend on the substitution.
  To this setting, we made various improvements which we describe in the remainder
  of this section.

  The explicit threading of the substitution is a tedious job.
  Alternatively, we can regard unification as an operation with side effects that
  affects the substitution. In Chapter~\tref{chapt.side-effect}, we showed how
  to make the visit order explicit and use this order to declaratively specify
  the relative order of the operations with side effects in addition to the
  usual order constraints induced by attribute dependencies.
  To retain the desired referential transparency of attributes in the
  programming model, side effects may only be used in the construction of
  higher-order children.
  In particular, this approach allows AGs to be integrated
  in a compiler that uses inference monads.

  The relative order of operations that provide fresh placeholders and
  perform unification is largely irrelevant.
  In Chapter~\tref{chapt.warren}, we presented
  commutable rules for threaded attributes to both model side effects
  and to relax the order induced by attribute dependencies.
  In Chapter~\rref{chapt.warren}, we abstracted from visits to phases, where a
  phase corresponds to one or more inferred visits, and allowed us to
  decouple the actual AG evaluation algorithm.
  Visits provide a fine-grained model to describe aspects of the evaluation
  of AGs, whereas with phases we can specify properties of larger chunks of
  evaluation.
  We also showed how to encode the Kennedy-Warren AG evaluation algorithm
  in a strongly-typed functional language.

%%  Since this chapter described how to generalize visits to phases, we
%%  described the remainder of the thesis in terms of visits without
%%  loss of generality.

  We exploited the notion of a visit to express typical inference algorithms.
  In Chapter~\tref{chapt.iterative}, we presented how to express fixpoint iteration
  by iterating visits. An invocation of a visit on a subtree specifies how
  to compute the visit's inherited attributes from its synthesized attributes
  of the previous iteration. In contrast to conventional fixpoint evaluators
  for AGs, the notion of visits allows us to compute stop
  conditions as synthesized attribute, and have visit-local chained
  attributes that retain computed values of previous visits.

  When an attribute contains an unconstrained placeholder,
  residuation is a strategy that defers a dependent computation until the placeholder
  is sufficiently constrained.
  In Chapter~\tref{chapt.iterative}, we presented an example that implements the residuation
  strategy by decoupling a child at one location in the tree and provide input at another
  location in the tree.
  This mechanism also provides
  an integration with constraints (Section~\tref{sect.iter.discussion}).
  %% loc.sem1 <- detach x.v
  %% register loc.sem1
  %% lookup loc.sem2
  %% attach x.(v+1) <- loc.sem2
  %% Explicit interface allows us to invoke the visit from e.g. Haskell.

  In Chapter~\tref{chapt.iterative}, we also presented how to infer the derivation tree as a
  function of the inherited attributes. In a case study~\citep{ariem-ext-gadt}, we illustrated
  the need for search strategies to infer the structure of derivation trees
  when the structure of the derivation tree is not functionally defined.
  Chapter~\tref{chapt.breadthfirst} showed how to encode such search strategies.

  Finally, our work provides solutions in other contexts than type inference.
  We illustrated this in the extended edition of this thesis~\citep{ariem-ext-graph},
  where we applied our work to graphs.
  Since many analyses in compilers are based on control-flow or data-flow graphs,
  we showed how to associate a semantics with each node of such a graph with
  an AG, while explicitly specify visits to these nodes with a traversal algorithm.
  Moreover, this approach allows the encoding of reference attributes in an ordered AG.

  In Chapter~\tref{chapt.dependent-ags}, we applied our work to dependently-typed
  languages. With dependently-typed attributes, invariants between attributes can be expressed,
  and proven to hold, which allows formal reasoning with attribute grammars.
  Moreover, the type attributes provide a mechanism for the universal and existential quantification
  of the type of a semantic functions.

  %%\paragraph{Advantages and disadvantages.}
  \section{Remarks}
  We put great effort in ensuring that our extensions retain the ease of composition
  as offered by AGs so that attributes and rules can still be defined in an aspect-wise and
  order-independent fashion.
  Also, our ideas are conservative extensions of AGs. A conventional AG can be expressed
  straightforwardly, which allows features of RulerCore to be retrofitted on an implementation
  using conventional AGs.

  However, to exploit the visit order, we need to specify in which order the children are
  visited.
  For conventional AGs, the traversal over the AST and order of evaluation
  of rules does not need to be specified, which has the advantage that it is no concern
  for the programmer.
  This is only a small price to pay. Such orders are declaratively specified
  (Chapter~\tref{chapt.side-effect}), and only where needed.
  %% Moreover, mistakes in the visit order are likely to be caught by the depedency
  %% analysis.

  %%\paragraph{Implementations.}
  \section{Implementations}
  We implemented several prototypes to experiment with the extensions presented in this thesis.
  We validated that our extensions have reasonably efficient implementations. In particular, the
  ideas are implementable in Haskell.
  Our prototypes depend on language features such as lazy evaluation,
  monads and GADTs. However, the underlying ideas themselves are implementable
  in mainstream languages and other AG systems.

  To our attribute grammar system UUAG, we added higher-order children
  (Section~\ref{intro.sect.higherorder})
  and stepwise evaluation (Chapter~\tref{chapt.breadthfirst}).
  In essence, we added only features that do not conflict with the
  conventional notion of AGs.
  Also, we implemented several features to support the use of AGs in large
  compiler implementations. In particular, we organized the code generated by UUAG
  such that separate compilation, debugging, and profiling is possible.

  In the tool @ruler-core@, we implemented the programming
  model with explicit visits (Chapter~\tref{chapt.side-effect}).
  We experimented with clauses, fixpoint iteration, and other features
  that benefit from the notion of a visit (Chapter~\tref{chapt.iterative}).
  As further case study, @ruler-core@ was used in a master project to implement the
  inference algorithm of the HML type system~\citep{DBLP:conf/popl/Leijen09}.

  In the tool @ruler-interpreter@ we implemented the operational semantics
  as outlined in Chapter~\tref{chapt.warren}. The interpreter provides
  custom judgment syntax, aspect-weaving of type rules, and a built-in
  efficient unification mechanism.
  The simplicity of an interpreter facilitated rapid prototyping with
  some of RulerCore's features.

  %%\paragraph{Future work.}
  \section{Future Work}
  We implemented and validated our ideas with several prototype
  implementations. We provided powerful building blocks for the
  description of inference algorithms with AGs, and the description
  of patterns that often occur in these contexts.
  However, to fully exploit our techniques, an integrated implementation of all
  extensions is needed.

  The features that we implemented in UUAG
  were used to improve the UHC implementation.
  Moreover, we used UHC as motivation to investigate AG
  extensions using RulerCore for prototyping purposes.
  We claim that we provide sufficient expressive power to
  implement unification and context reduction more concisely
  in UHC, but to actually do so remains as future work.

  We provide the algorithmic underpinning of inference
  algorithms for AGs. This takes us one step closer to
  our ultimate goal to derive type inference algorithms
  from type system specifications.
  However, the remaining challenges
  as mentioned in Section~\ref{intro.sect.overview}
  need to be addressed as well, such as special syntax
  and first-class abstractions for AGs.
  Moreover, visits are a prominent component in our
  current work. A direction of future work is to
  \emph{infer} properties of visits from a more abstract
  specification.

  A question that remains open is how we can
  formally prove and ensure properties of the
  implementations that we generate. We address this
  topic briefly in Chapter~\tref{chapt.dependent-ags}.
  A direction of future work is to generate boilerplate
  code to support typical proofs.

  This thesis provides a core language for
  inference algorithm descriptions, which paves the
  way for high-level abstractions of inference
  algorithms, thus facilitates more complex
  language implementations, and ultimately leads
  to software of higher quality.