%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 terminator = "\Box" %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 rulerback = "{\mbox{\scshape ruler-back}}" %format shadow = "{\mbox{\scshape shadow}}" Type inference on a program is the gradual process of constructing a \emph{typing derivation}, which is a proof that relates the program to a type. During this process, inference algorithms analyze the intermediate states of the typing derivation to direct the construction of the proof. Since a typing derivation is a decorated tree, we aim to use attribute grammars to implement type inference. In their present form, it is hard to express type inference in attribute grammars, because attributes are defined in terms of the final state of the decorated tree. We present the language RulerCore, a conservative extension to ordered, higher-order attribute grammars, that permits both the structure and attributes of the tree to be defined based on intermediate states of the tree. We show that both iteration-based and constraint-based inference algorithms can be expressed straightforwardly in RulerCore. \section{Introduction} \label{iter.sect.visit.intro} Attribute grammars (AGs) are traditionally used to specify the static semantics of programming languages~\citep{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 algorithm that implements the specification~\citep{DBLP:conf/popl/KennedyW76,DBLP:journals/acta/Kastens80}. We implemented a substantial part of the Utrecht Haskell Compiler (UHC)~\citep{DBLP:conf/afp/DijkstraS04,DBLP:journals/entcs/FokkerS09} with attribute grammars using the UUAG system~\citep{uuagc}. Haskell~\citep{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 \thiswork{}, however, are not restricted to any particular language. Attribute grammars benefit the implementation of a compiler for several reasons. 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, which makes attribute grammars highly composable~\citep{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. These advantages play an important role in the UHC project~\citep{uhc}. Two essential components of UHC's type inferencer, polymorphic unification and context reduction, would benefit from an AG-based implementation. For example, when polymorphic unification is defined as an AG, many of its required attributes can be automatically provided by the AGs of expressions and declarations. However, we implemented these components directly in Haskell, because it is not obvious how to express these as an attribute grammar. These two components present 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 inference, typically as a result of unifications. This requires a mixture of tree construction and attribute evaluation, which are normally separate tasks if one takes an AG view. Secondly, the construction of a proof of a subgoal may need to be postponed when it depends on a type that is not known yet. After more of the structure of the proof is determined, the 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 evaluates the attributes using a fixed algorithm. We present AG extensions to customize the algorithms, without loosing the advantages that AGs offer. More precisely, our contributions are: \begin{itemize} \item We present the language RulerCore, 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, as we explained in Chapter~\rref{chapt.side-effect}. Visits can be done iteratively. The number of iterations can be specified based on the values of attributes. \item We define abstract grammars on the structure of typing derivations. Productions are chosen based on the values of attributes. Moreover, we present \emph{clauses}, which allows the choice of a production to be refined per visit. \item Derivation trees are first class values in RulerCore. They can be passed around as attributes, and can be inspected by visiting them. \end{itemize} In Section~\ref{iter.sect.semantics}, we define a denotational semantics for RulerCore via a translation to Haskell. \item In Chapter~\tref{chapt.side-effect}, we gave an introduction to RulerCore. In this chapter, we show how RulerCore can be used to express type inference. Section~\ref{iter.sect:casestudy} presents an extensive example that motivates the design of RulerCore. \item An implementation of RulerCore is available at: \url{https://svn.science.uu.nl/repos/project.ruler.papers/archive/ruler-core-1.0.tar.gz}. It includes several examples. The implementation supports both statically ordered and demand driven evaluation of attributes. \item We compare our approach with other attribute grammar approaches (Section~\ref{iter.sect.visit.relatedwork}) as a further motivation for the need for RulerCore's extensions. \end{itemize} \section{Motivation} \label{iter.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 RulerCore. The implementation of |shadow| poses exactly those challenges mentioned in the previous section, while being small enough to fit in \thiswork{}. %if False We assume that the reader is familiar with attribute grammars~\citep{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 \citep{Middelkoop10wgt,Middelkoop10ifl}. %endif \subsection{Example: the Shadow-language} %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 a unique label |u| (i.e. |\(sup x u).|), and allow identifiers to refer to \emph{shadowed} bindings. 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{ The language |shadow| can be used to model typed disambiguation of duplicately imported identifiers from modules. However, |shadow| is only an example. 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 further below) it may be |\u1 . \u2 . f u1|. The compiler for |shadow| takes an 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. It is realized as a function |compile :: Env -> ExprS -> ExprT|: \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 identifier |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 RulerCore 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 { This example has a strong connection to context reduction in Haskell. The inference rules are type-directed. Such rules may be overlapping, and the choice of which rule to apply in a typing derivation may be ambiguous. }. \subsection{Relation to Attribute Grammars} We focus on writing an implementation for the above translation rules with attribute grammars using RulerCore. For each relation in the above specification, we introduce a nonterminal in the RulerCore 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 do not contain terminals: only the values of attributes determine the structure of the derivation tree. Thus, the grammar defines the language of derivation trees for the translation rules. Note that this differs from the standard AG approach, where a single specific parameter of the relations fully determines the shape of the derivation tree. Operationally, the algorithm, which specifies the construction of the derivation tree, 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 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 RulerCore, the grammar may contain productions per visit of a nonterminal. To make the distinction clearer, we call these productions \emph{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 conventional AG, each node in the AST is associated with exactly one production. In RulerCore, however, we may at each visit \emph{refine} the production that is associated with the node. 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 specialize the choice by going down one of the paths in the tree. Paths in this tree determine actual productions. %format itf = "\mathbf{itf}" A RulerCore program is a Haskell program augmented with attribute grammar code. We generate plain Haskell code from such a program. For each production of RulerCore we generate a coroutine in Haskell. These coroutines are encoded as continuations. The following is a code snippet of a RulerCore program. We explain the syntax further below: \begin{code} module MyCompiler where data ExprS = ... -- Haskell data declaration itf TransExpr ... -- RulerCore nonterminal and attribute declaration itf TransExpr ... -- additional attribute declarations for nonterminal ones = 1 : ones -- Haskell binding translate = sem transExpr :: TransExpr -- embedded production ... rules ... -- rules of RulerCore sem transExpr ... rules ... -- additional rules for production sem transExpr ... rules ... -- even more rules \end{code} With an itf-block, we define a nonterminal and its attributes. With a sem-block, we we define a production, and its clauses and rules, inside a Haskell expression. The sem-block is substituted with the coroutine that is generated for |transExpr|. This coroutine is thus a Haskell expression that, and is bound to the Haskell identifier |translate|. Additional clauses and rules can be given in separate toplevel sem-blocks. The coroutines that we generate from productions are known as visit functions~\citep{DBLP:conf/ifip2-4/SwierstraA98}. Inputs to and outputs 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 (their closures) that represent the children. An invocation of such a visit function corresponds to a visit in the attribute grammar description. An invocation of a visit function of a root nonterminal thus corresponds to the partial construction of the root node of the derivation tree. Section~\ref{iter.sect.semantics} shows the translation to Haskell. In RulerCore, a production is the root of a tree of clauses. Thus, we can represent a production of a conventional grammar as a production in RulerCore. Alternative, as we do in the example, we can also introduce only one production per nonterminal, and use clauses to represent productions of a conventional grammar. The distinction is mainly technical: productions can be used when the tree is determined before attribute evaluation (the productions form an algebra), whereas clauses can be used to determine the structure of the tree based on attribute values. %% A production without clauses automatically contains a single clause with the name of that production. %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} \label{visit.sect.typingexpressions} Figure~\ref{iter.fig.example.derivation} gives a rudimentary sketch of a derivation tree and some of the nonterminals and productions that we introduce. The root node corresponds to production |wrapper| of nonterminal |Compile|. It has a child which is related to production |transExpr| of nonterminal |TransExpr|. Production |transExpr| consists of clauses |exprVar|, |exprLam|, etc.\ for the various forms of syntax of |shadow|. In locating an identifier in the environment, three nonterminals play a role. Clause |lookupTy| of nonterminal |Lookup| has a list of children, each with nonterminal |LookupMany|. Each child is associated with a clause |lookupLam| of nonterminal |LookupOne|, and represent a choice for a binding. The dotted line points to that binding. At the end of inference, at most one of these choices remains per child with nonterminal |Lookup|. \begin{figure}[htb] \centering \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=\footnotesize} , arr/.style={<-,dashed, very thick} , level distance=8mm , sibling distance=52mm ] \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]{|LookupMany.lkCons|}; \node[lab, left of=cons2]{|LookupMany.lkCons|}; \node[lab, left of=nil]{|LookupMany.lkNil|}; \node[lab, left of=lookupLam1, xshift=-2mm]{|LookupOne.lookupLam|}; \node[lab, left of=lookupLam2, xshift=-2mm]{|LookupOne.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 a derivation tree for |\(sup x u1) . \(sup x u2) . x|} \label{iter.fig.example.derivation} \end{figure} We declare a type |TransExpr| for the production |transExpr|, which describes the \emph{interface} of a nonterminal. The interface declares the visits and attributes of a nonterminal: \begin{code} itf TransExpr -- declaration of nonterminal |TransExpr| 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 further below \end{code} In this case, a production of a nonterminal |TransExpr| has a single visit named |dispatch|, and two inherited attributes. The attribute |expr| contains the expression to translate. We define more attributes and visits on |TransExpr| below. The visits are totally ordered based on value-dependencies between attributes that are derived from the clauses in the whole program. This order is constructable when the attribute dependencies are acyclic. Chapter~\rref{chapt.side-effect} explains how to derive this order, and Chapter~\rref{chapt.warren} generalizes that approach. Attribute |expr| is declared explicitly for visit |dispatch| (note the indenting). The |env| attribute is not declared for a particular visit. The latest visit it can be allocated to is determined automatically. From the interface of a nonterminal, a Haskell type for the coroutines is generated. Also, wrapper functions (Section~\rref{intro.ag.syntax}) to invoke the coroutines and access or provide values for attributes from the Haskell code are generated from the interface. We introduce a production |transExpr| with nonterminal |TransExpr| using a sem-block, embedded in Haskell code. This sem-block is translated to a coroutine in plain Haskell: \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 clauses, we subsequently introduce further sem-rules to determine what has to be done. Unlike most of the other code that we give in this section, the order of appearance is relevant for clauses. Operationally, clauses are tried in that order: \begin{code} sem transExpr -- production with clauses clause exprVar of dispatch -- typical name of first visit clause exprApp of dispatch clause exprLam of 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 parent 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 |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, analogously 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} The meaning of an assert-rule is similar to the match-rule, except that the match is expected to succeed. If not, its 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. Further below, 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 further below. \end{itemize} We introduce more forms of rules further below. 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 sem-block defines rules for clause |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} An attribute grammar distinguishes two categories of attributes: inherited and synthesized. The names of attributes within the same category need 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 -- test for |AppS| child f :: TransExpr = translate -- recurses on |f| child a :: TransExpr = translate -- recurses on |a| f.expr = loc.f -- passes |loc.f| as expr-attribute a.expr = loc.a -- passes |loc.a| as expr-attribute f.env = lhs.env -- passes the environment topdown a.env = lhs.env -- passes the environment topdown \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 variants of default-rules. We show further below 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 -- extends the interface of |TransExpr| syn ty :: Ty -- synthesized attr in unspecified visit chn subst1 :: Subst -- chained attr in unspecified 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` env| 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 below. 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 nonterminal |Fresh|. Therefore, it consists of a single anonymous visit. When a production does not specify a visit-block, an anonymous visit-block is implicitly defined. Similarly, when a production does not define clauses for a production, an anonymous clause-block is implicitly defined. We can wrap any Haskell function, including a data constructors, as a production, and represent an application of this function as child of the production (Section~\rref{intro.sect.higherorder}). This is convenient in case of |fresh|, because we use default rules to automatically deal with the substitution attribute. 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. The Lookup-child 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} We pass the substitution to child |fr|, and pass the resulting substitution upwards to the parent node: \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~\citep{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 clauses based on two inherited attributes: the attributes |ty1| and |ty2| of nonterminal |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 -- variable on the left clause matchVarR of dispatch -- variable on the right 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. We omit here the actual implementation, since the implementation 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 -- implemented with RulerCore 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 its first parameter a list of values of attributes |attr| of the children that have this attribute. If |f| is not given, we use the Haskell function |last| for |f| (Section~\rref{intro.outline.sideeffect}): \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|, which are computed by applying the substitution to |lhs.ty1| and |lhs.ty2|. 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 ready 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 in an unconventional way. Instead of transporting the information needed to construct the lookup-derivation tree in |exprVar|, the environment transports a coroutine |loc.lk| defined in |exprLam|. We define the production |lookupLam| locally in |exprLam|, such that the rules of |lookupLam| have access to the attributes of |exprLam|: \begin{code} itf LookupOne -- nonterminal of \emph{nested} production |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 production (shown further below) have access to the local state (i.e. attributes) of the enclosing production. 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{iter.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. From 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 RulerCore 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{iter.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 production |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 element 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 -- passes the types by default downwards to |hd| and |tl| \end{code} If all the matching |lookupsOne|s 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 for a child. We intend to invoke the |resolve| visit multiple times. We show further below 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| demonstrate the use of the hide-rule: \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 rules of the |lkCons| clause represent a choice. If from the attributes of the children can be concluded that 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" The states of child nodes that are introduced by a previous visit are properly maintained if their visits are also repeated. However, child nodes that are created in a visit are not retained when the visit is repeated. To prevent a created node from being discarded, it is possible to store a node 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: \begin{code} attr = detach visitname of childname rangle \end{code} Evaluation of a detach-rule takes the child |childname| that is evaluated up to but not including visit |visitname|, and stores it in an attribute |attr|. A detached child can be attached with an attach-rule: \begin{code} attach visitname of childname = expr \end{code} The Haskell expression |expr| represents a tree in a state prior to visit |visitname|. If |childname| already exists as child, the attach-rule overrules the visits starting from |visitname|. The |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 substitutions \emph{defaults} the choice for 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 further below: \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 production |iterInner|, which invokes visit |resolve| one or more times. The iterate-rule denotes the repeated invocation of a visit of a child: \begin{code} iterate visitname of childname = expr \end{code} The expression |expr| represents the coroutine of a special production (|iterNext|, explained further below) that computes the inherited attributes for the visit of the next iteration from synthesized attributes of the previous iteration. The iterations stop when this special production 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 production 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 production |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 the 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} The remaining code of the compiler invokes the coroutine generated from the |compile| production. It provides the |ExprS| expressions, and obtains the type and an |ExprT| back. We omit these details. \subsection{Discussion} \label{sect.iter.discussion} \paragraph{Performance.} Clauses introduce backtracking. In the worst case, this leads to a number of traversals that are exponential in the size of the (longest intermediate) tree. In practice, clause selection is typically 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 RulerCore programs expressible in UUAG. We verified that programs generated from RulerCore exhibit the same time and memory behavior as programs generated from UUAG. %% 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 the information to other parts, which allows 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 RulerCore 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 RulerCore program is typically easy to prove. Completeness, however, is a different issue. That largely depends on decisions made about unknown types. With RulerCore, we make explicit when choices are made, and when visits are repeated. We believe this helps when 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{iter.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{iter.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 RulerBack, a small core language for Attribute Grammars. We translate a RulerCore program in two steps to Haskell. We first desugar RulerCore. This gives us a RulerBack program. We then translate the latter to Haskell. The separately defined attributes of RulerCore are grouped together in RulerBack, 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 translation, as it is similar to the frontend of UUAG~\citep{uuagc}. %% Should make here some commercial for doaitse's new parser combinators :P Instead, we focus on the translation to Haskell, which precisely defines the semantics of RulerBack, and thus forms the underlying semantics of RulerCore. %% If 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 RulerBack 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 production |x| t ::= visit x1 chn (many x2) (many r) (many c) -- visit def, with common rules |r| | terminator -- end of the visit sequence 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 partially evaluated 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 implementation is parametrizable over any backtracking monad. In this chapter, we use |IO| as example. \subsection{Example} %format sumCons1 %format sumNil1 %format sumCons2 %format sumNil2 %format noIterationS = noIteration "_" S The following example is taken from Section~\tref{side.sem.rulercore}. It demonstrates how to to compute the sum of a list of integers in two visits in RulerBack. In the first visit, the attribute |l| is inspected to obtain the elements in the list. In the second visit, the elements are summed up: \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 sumNil1 -- 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 terminator -- no next visit clause sumCons1 -- 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| terminator -- no next visit \end{code} %format S_v1 %format S_v2 We translate a RulerBack production 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, terminator))) \end{code} Inherited attributes become parameters, and synthesized attributes are returned as a tuple of results. Each visit also returns two continuations of type |S_v1| and |S_v2| respectively. The first continuation represents the current visit itself (which may be re-invoked with updated internal state), the second continuation represents the next visit, or |terminator| if there is no subsequent visit. Since no inherited attributes have been declared for the second visit, the continuation of type |S_v2| can actually be represented as a value: \begin{code} newtype S_v2 = S_v2 (IO (Int, (S_v2, terminator))) \end{code} The coroutine |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 vis_tl_v1 %format vis_tl_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 -- the initial state 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 = terminator -- 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 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 = terminator -- 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 RulerCore names to Haskell names. The right-hand sides of these definitions consist of string concatenations: \begin{code} outp "loc" x = "locL" x ^^^^ inp "loc" x = "locL" x outp "lhs" x = "lhsS" x ^^^^ inp "lhs" x = "lhsI" x outp c x = c "I" x ^^^^ inp c x = c "S" x outp y = "visitS" y ^^^^ inp y = "visitI" y vis c x = "vis_" c "_" x ^^^^ prod x = "sem_" 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} Note that an attribute |c.x| for some child |x| at an \emph{output position} represents the inherited attribute |x| of |c|, and vice versa for attributes at input positions. The types of the coroutines are generated from an interface declaration: %% 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 (prod x)) = semt I t in semb (prod 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 using a let-statement, which ensures 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 RulerCore or RulerBack program is well typed, then so is the generated Haskell program, and vice versa. %if False Further investigation requires a discussion of RulerCore's type system, which we omit for reasons of space. %endif 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{iter.sect.visit.relatedwork} Attribute grammars as defined by \citet{DBLP:journals/mst/Knuth68} are extensions of context free grammars. Typically, an attribute grammar is defined in terms of a context-free abstract grammar of the language to analyze or compile. The attribute evaluator computes attributes of the abstract syntax tree that is determined apriori by a parser. In case of type inference, when the typing relations are not directed by syntax, the derivation tree is not known beforehand. Thus, the derivation tree cannot be expressed directly in terms of attribute grammars, unless higher-order attributes are used~\citep{DBLP:conf/pldi/VogtSK89}. \paragraph{Tree manipulations.} There are many extensions to attribute grammars to facilitate changing the tree during attribute evaluation. Silver~\citep{DBLP:journals/entcs/WykBGK08}, JastAdd~\citep{DBLP:conf/oopsla/EkmanH07} and UUAG~\citep{uuagc} support higher-order attributes. These grammars allow the tree to be extended with subtrees that are 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 RulerCore, a child itself selects a clause to make a choice, and a choice can be made per visit. JastAdd and Aster~\citep{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 difficult to express 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. 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~\citep{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 RulerCore, 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{Arbab:1986:CCA:13831.13837} show how to translate attribute grammars to Prolog. However, this approach does not allow the inspection of partial |LookupOne| derivations of Section~\ref{iter.sect.lookups}, nor the defaulting, to be implemented easily. With RulerCore, we offer alternative constructions of the tree per visit in combination with backtracking. 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{iter.sect.semantics}. %% Arguably, some manual intervention is required, for example to implement %% the defaulting mechanism in Section~\ref{iter.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 RulerCore. \citet{DBLP:journals/jacm/EngelfrietF89} show the expressiveness of classes of attribute grammars. Unsurprisingly, deterministic AG evaluators have lower computational complexity bounds compared to non-deterministic ones. With RulerCore, we target large compilers (i.e. UHC), that processes large abstract syntax trees, thus we need the control on the exploration of alternatives 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~\citep{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 also provide guarded rules, but in addition also allow children to be conditionally defined. \citet[chap. 3]{Saraiva99} describe multi-traversal functions in a functional language (or visit functions~\citep{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{iter.sect.visit.conclusion} We presented the extensions that RulerCore, a conservative extension of ordered attribute grammars, provides to describe type inference algorithms. We explained RulerCore with an extensive example in Section~\ref{iter.sect:casestudy} and described its semantics in Section~\ref{iter.sect.semantics}. RulerCore has several distinct features. Firstly, in contrast to most attribute grammar systems, construction of a derivation tree and the evaluation of its attributes is intertwined in RulerCore. 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, 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 RulerCore, derivation trees are first class and can be inspected by visiting them, which facilitates such reasoning in terms of attributed trees. %% Following up on these ideas, %% As future work, we started a project to describe UHC's type inference %% algorithm as attribute grammar with RulerCore. With RulerCore, %% we can express unification and context reduction, which paves the %% way for a full description of UHC's inference algorithm with attribute %% grammars.