Dependently Typed Attribute Grammars

Arie Middelkoop, Atze Dijkstra, and S. Doaitse Swierstra

Universiteit Utrecht, The Netherlands

Abstract. Attribute Grammars (AGs) are a domain-specific language for functional and composable descriptions of tree traversals. Given such a description, it is not immediately clear how to state and prove properties of AGs formally. To meet this challenge, we apply dependent types to AGs. In a dependently typed AG, the type of an attribute may refer to values of attributes. The type of an attribute is an invariant, the value of an attribute a proof for that invariant. Additionally, when an AG is cycle-free, the composition of the attributes is logically consistent. We present a lightweight approach using a preprocessor in combination with the dependently typed language Agda.

1 Introduction

Functional programming languages are known to be convenient languages for implementing a compiler. As part of the compilation process, a compiler computes properties of Abstract Syntax Trees (ASTs), such as environments, types, error messages, and code. In functional programming, these syntax-directed computations are typically written as catamorphisms^{1}. An algebra defines an inductive property in terms of each constructor of the AST, and a catamorphism applies the algebra to the AST. Catamorphisms thus play an important role in a functional implementation of a compiler.

Attribute Grammars (AGs) [3] are a domain-specific language for composable descriptions of catamorphisms. AGs facilitate the description of complex catamorphisms that typically occur in complex compiler implementations.

An AG extends a context-free grammar by associating attributes with nonterminals. Functional rules are associated with productions, and define values for the attributes that occur in the nonterminals of associated productions. As AGs are typically embedded in a host language, the rules are terms in the host language, which may additionally refer to attributes. Attributes can easily be composed to form more complex properties. An AG can be compiled to an efficient functional algorithm that computes the synthesized attributes of the root of the AST, given the root’s inherited attributes.

It is not immediately clear how to formally specify and write proofs about programs implemented with AGs. Dependent types [1] provide a means to use types to encode

1 Catamorphisms are a generalization of folds to tree-like data structures. We consider catamorphisms from the perspective of algebraic data types in functional programming instead of the equivalent notion in terms of functors in category theory. A catamorphism cata_{τ} (f_{1}, ..., f_{n}) replaces each occurrence of a constructor c_{i} of τ in a data structure with f_{i}. The product (f_{1}, ..., f_{n}) is called an algebra. An element f_{i} of the algebra is called a semantic function.

properties with the expressiveness of (higher-order) intuitionistic propositional logic, and terms to encode proofs. Such programs are called correct by construction, because the program itself is a proof of its invariants. The goal of this paper is therefore to apply dependent types to AGs, in order to formally reason with AGs.

Vice versa, AGs also offer benefits to dependently typed programming. Because of the Curry-Howard correspondence, dependently typed AGs are a domain-specific language to write structurally inductive proofs in a composable, aspect-oriented fashion; each attribute represents a separate aspect of the proof. Additionally, AGs alleviate the programmer from the tedious orchestration of multi-pass traversals over data structures, and ensure that the traversals are total: totality is required for dependently typed programs for reasons of logical consistency and termination of type checking. Hence, the combination of dependent types and AGs is mutually beneficial.

We make the following contributions in this paper:

– We present the language AGda (Section 3), a light-weight approach to facilitate dependent types in AGs, and vice versa, AGs in the dependently typed language Agda. AGda is an embedding in Agda via a preprocessor. In contrast to conventional AGs, we can encode invariants in terms of dependently typed attributes, and proofs as values for attributes. This expressiveness comes at a price: to be able to compile to a total Agda program, we restrict ourselves to the class of ordered AGs, and demand the definitions of attributes to be total.

– We define a desugared version of AGda programs (Section 4) and show how to translate them to plain Agda programs (Section 5).

– Our approach supports a conditional attribution of nonterminals, so that we can give total definitions of what would otherwise be partially defined attributes (Section 6).

In Section 2, we introduce the notation used in this paper. However, we assume that the reader is both familiar with AGs (see [10]) and dependently typed programming in Agda (see [7]).

2 Preliminaries

In this warm-up section, we briefly touch the Agda and AG notation used throughout this paper. As an example, we implement the sum of a list of numbers with a catamorphism. We give two implementations: first one that uses plain Agda, then another using AGda. This example does not yet use dependently typed attributes. These are introduced in the next section.

In the following code snippet, the data type List represents a cons-list of natural numbers. The type T′List is the type of the value we compute (a number), and A′List is the type of an algebra for List. Such an algebra contains a semantic function for each constructor of List, which transforms a value of that constructor into the desired value (of type T′List), assuming that the transformation has been recursively applied to the fields of the constructor. The catamorphism cata_{List} performs the recursive application.

\underline{data} List: Set \underline{where}  -- represents a cons-list of natural numbers
nil : List  -- constructor has no fields

cons : → List → List  -- constructor has a number and tail list as fields
T′List=  -- defines a type alias T′List: Set,
A′List= (T′List, → T′List→ T′List)  -- and A′List: Set
cata_{List} : A′List→ List → T′List  -- applies algebra to list
cata_{List}(n, ) nil = n  -- in case of nil, replaces nil with n
cata_{List}alg l \underline{with}alg | l  -- otherwise, matches on alg and l
cata_{List}alg l | ( , c)| cons x xs \underline{with}cata_{List} alg xs -- recurses on xs
cata_{List}alg l | ( , c)| cons x xs | r = c x r  -- replaces cons with c

In Agda, a function is defined by one or more equations. A with-construct facilitates pattern matching against intermediate values. An equation that ends with \underline{with} e_{1} | ...| e_{n} parameterizes the equations that follow with the values of e_{1}, ..., e_{n} as additional arguments. Vertical bars separate the patterns intended for the additional parameters.

The actual algebra itself simply takes 0 for the nil constructor, and + for the cons constructor. The function sum_{List} shows how the algebra and catamorphism can be used.

sem_{nil} : T′List  -- semantic function for nil constructor
sem_{nil} = 0  -- T′List= (defined above)
sem_{cons} : → T′List→ T′List  -- semantic function for cons constructor
sem_{cons} = +  -- + : → → (defined in library)
sum_{List} : List → T′List  -- transforms the List into the desired sum
sum_{List} = cata_{List} (sem_{nil}, sem_{cons}) -- algebra is semantic functions in a tuple

In the example, the sum is defined in a bottom-up fashion. By taking a function type for T′List, values can also be passed top-down. Multiple types can be combined by using products. Such algebras quickly become tedious to write. Fortunately, we can use AGs as a domain-specific language for algebras. In the code below, we give an AG implementation: we specify a grammar that describes the structure of the AST, declare attributes on productions, and give rules that define attributes.

We now give an implementation of the same example using AGda. The code consists of blocks of plain Agda code, and blocks of AG code. To ease the distinction, Agda’s keywords are underlined, and keywords of AGda are typeset in bold.

A grammar specification is a restricted form of a data declaration (for an AST): data constructors are called productions and their fields are explicitly marked as terminal or nonterminal. A nonterminal field represents a child in the AST and has attributes, whereas a terminal field only has a value. A plain Agda data-type declaration can be derived from a grammar specification. In such a specification, nonterminal types must have a fully saturated, outermost type constructor that is explicitly introduced by a grammar declaration. Terminal types may be arbitrary Agda types^{2}.

grammar List: Set -- declares nonterminal List of type Set
prod nil : List -- production nil of type List (no fields)
prod cons : List -- production cons of type List (two fields)

2 In general, although not needed in this example, nonterminal types may be parametrized, production types may refer to its field names, and field types may refer to preceding field names.

term  hd :  -- terminal field hd of type
nonterm tl : List -- nonterminal field tl of type List

With an interface specification, we declare attributes for nonterminals. Attributes come in two fashions: inherited attributes (used in a later example) must be defined by rules of the parent, and synthesized attributes may be used by the parent. Names of inherited attributes are distinct from names of synthesized attributes; an attribute of the same name and fashion may only be declared once per nonterminal. We also partition the attributes in one or more visits. These visits impose a partial order on attributes. Inherited attributes may not be defined in terms of a synthesized attributes of the same visit or later. We use this order in Section 4 to derive semantic functions that are total.

itf List  -- interface for nonterminal List,
visit compute -- with a single visit that is named compute,
syn sum: -- and a synthesized attribute named sumof type

Finally, we define each of the production’s attributes. We may refer to an attribute using child.attr notation. For each production, we give rules that define the inherited attributes of the children and synthesized attributes of the production itself (with lhs as special name), using inherited attributes of the production and synthesized attributes of the children. The special name loc refers to the terminals, and to local attributes that we may associate with a production.

datasem List -- defines attributes of List for constructors of List
prod nil lhs.sum = 0  -- rule for sumof production nil
prod cons lhs.sum = loc.hd + tl.sum -- refers to terminal hd and attr tl.sum

The left-hand side of a rule is a plain Agda pattern, and the right-hand side is either a plain Agda expression or with-construct (not shown in this example). Additionally, both the left and right-hand sides may contain attribute references.

During attribute evaluation, visits are performed on children to obtain their associated synthesized attributes. We do not have to explicitly specify when to visit these children, neither is the order of appearance of rules relevant. However, an inherited attribute c.xmay not depend on a synthesized attribute c.yof the same visit or later (in the interface). This guarantees that the attribute dependencies are acyclic, so that we can derive when children need to be visited and in what order.

AGs are a domain-specific language to write algebras in terms of attributes. From the grammar, we generate the data type and catamorphism. From the interface, we generate the T′List type. From the rules, we generate the semantic functions sem_{nil} and sem_{cons}. AGs pay off when an algebra has many inherited and synthesized attributes. Also, there are many AG extensions that offer abstractions over common usage patterns (not covered in this paper). In the next section we present AGs with dependent types, so that we can formulate properties of attributes (and their proofs).

3 Dependently Typed Example

In this section, we use AGda to implement a mini-compiler that performs name checking of a simple language Source, and translates it to target language Target if all used identifiers are declared, or produces errors otherwise. A term in Source is a sequence of identifier definitions and identifier uses, for example: def a ⋄ use b ⋄ use a. In this case, b is not defined, thus the mini-compiler reports an error. Otherwise, it generates a Target term, which is a clone of the Source term that additionally carries evidence that the term is free of naming errors. Section 3.2 shows the definition of both Source and Target.

We show how to prove that the mini-compiler produces only correctly named Target terms and errors messages that only mention undeclared identifiers. The proofs are part of the implementation’s code. Name checking is only a minor task in a compiler. However, the example shows many aspects of a more realistic compiler.

3.1 Support Code Dealing With Environments

We need some Agda support code to deal with environments. We show the relevant data structures and type signatures for operations on them, but omit the actual implementation. We represent the environment as a cons-list of identifiers.

Ident = String  -- Ident : Set
Env = List Ident -- Env: Set

In intuitionistic type theory, a data type represents a relation, its data constructors deduction rules for such a relation, and values built using these constructors are proofs for instances of the relation. We use some data types to reason with environments.

A value of type ι ∈ Γ is a proof that an identifier ι is member of an environment Γ. A value here indicates that identifier is at the front of the environment. A value next means that the identifier can be found in the tail of the environment, as described by the remainder of the proof.

\underline{data} ∈ : Ident → Env → Set \underline{where} here : {ι: Ident} {Γ : Env} → ι ∈ (ι:: Γ) next: {ι_{1} : Ident} {ι_{2} : Ident} {Γ : Env} → ι_{1} ∈ Γ → ι_{1} ∈ (ι_{2} :: Γ)

The type Γ_{1} ⊑ Γ_{2} represents a proof that an environment Γ_{1} is contained as a subsequence of an environment Γ_{2}. A value subLeft means that the environment Γ_{1} is a prefix of Γ_{2}, and subRight means that Γ_{1} is a suffix. With trans, we transitively compose two proofs.

\underline{data} ⊑ : Env → Env → Set \underline{where}

subLeft : {Γ_{1} : Env} {Γ_{2} : Env} → Γ_{1} ⊑ (Γ_{1} ++ Γ_{2})
subRight: {Γ_{1} : Env} {Γ_{2} : Env} → Γ_{2} ⊑ (Γ_{1} ++ Γ_{2})
trans : {Γ_{1} : Env} {Γ_{2} : Env} {Γ_{3} : Env} → Γ_{1} ⊑ Γ_{2} → Γ_{2} ⊑ Γ_{3} → Γ_{1} ⊑ Γ_{3}

The following functions operate on proofs. When an identifier occurs in an environment, function inSubsetproduces a proof that the identifier is also in the superset of the environment. Given an identifier and an environment, ι ∈_{?} Γ returns either a proof ι ∈ Γ that the element is in the environment, or a proof that it is not.

inSubset: {ι: Ident} {Γ_{1} : Env} {Γ_{2} : Env} → Γ_{1} ⊑ Γ_{2} → ι ∈ Γ_{1} → ι ∈ Γ_{2}
∈_{?}  : (ι: Ident) → (Γ : Env) → ¬(ι ∈ Γ) ⊎ (ι ∈ Γ)

A value of the sum-type α ⊎ β either consists of an α wrapped in a constructor inj_{1} or of a β wrapped in inj_{2}.

3.2 Grammar of the Source and Target Language

Below, we give a grammar for both the Source and Target language, such that we can analyze their ASTs with AGs^{3}. The Target language is a clone of the Source language, except that terms that have identifiers carry a field proof that is evidence that the identifiers are properly introduced.

grammar Root : Set  -- start symbol of grammar and root of AST
prod root : Root nonterm top : Source -- top of the Source tree
grammar Source : Set  -- grammar for nonterminal Source
prod use  : Source  -- ’result type’ of production
term  ι : Ident  -- terminals may have arbitrary Agda types
prod def  : Source  -- ’result type’ may be parametrized
term  ι : Ident
prod ⋄ : Source -- represents sequencing of two Source terms
nonterm left : Source  -- nonterminal fields must have a nonterm as
nonterm right : Source  -- outermost type constructor.
grammar Target : Env → Set -- grammar for nonterminal Target
prod def  : Target Γ -- production type may refer to any field,
term^{?} Γ : Env  -- e.g. Γ. Agda feature: implicit terminal
term  ι : Ident  -- (inferred when building a def)
term  ϕ : ι ∈ Γ  -- field type may refer to preceding fields
prod use  : Target Γ
term^{?} Γ : Env  -- a Target term carries evidence: a
term  ι : Ident  -- proof that the identifier is in the
term  ϕ : ι ∈ Γ  -- environment
⋄  : Target Γ
term^{?} Γ : Env
nonterm left : Target Γ -- nonterm fields introduce children that
nonterm right : Target Γ -- have attributes
\underline{data} Err : Env → Set where  -- data type for errors in Agda notation

scope : {Γ : Env} (ι: Ident) → ¬(ι ∈ Γ) → Err Γ

Errs Γ = List (Err Γ)  -- Errs : Env → Set

As shown in Section 2, we generate Agda data-type definitions and catamorphisms from this specification.

3 In our example, we could have defined the type Target instead using conventional Agda notation. However, the grammar for Target serves as an example of a parameterized nonterminal.

The concrete syntax of the source language Source and target language Target of the mini-compiler is out of scope for this paper; the grammar defines only the abstract syntax. Similarly, we omit a formal operational semantics for Source and Target: it evaluates to unit if there is an equally named def for every use, otherwise evaluation diverges.

3.3 Dependent Attributes

In this section, we define dependently typed attributes for Source. Such a type may contain references to preceding^{4} attributes using inh.attrNm or syn.attrNm notation, which explicitly distinguishes between inherited and synthesized attributes. The type specifies a property of the attributes it references; an attribute with such a type represents a proof of this property.

In our mini-compiler, we compute bottom-up a synthesized attribute gathEnv that contains identifiers defined by the Source term. At the root, the gathEnv attribute contains all the defined identifiers. We output its value as the synthesized attribute finEnv (final environment) at the root. Also, we pass its value top-down as the inherited attribute finEnv, such that we can refer to this environment deeper down the AST. We also pass down an attribute gathInFin that represents a proof that the final environment is a superset of the gathered environment. When we know that an identifier is in the gathered environment, we can thus also find it in the final environment. We pass up the attribute outcome, which consists either of errors, or of a correct Target term.

itf Root  -- attributes for the root of the AST
visit compile syn finEnv : Env
syn outcome : (Errs syn.finEnv) ⊎ (Target syn.finEnv)
itf Source -- attributes for Source
visit analyze syn gathEnv : Env -- attribute of first visit
visit translate inh finEnv : Env -- attributes of second visit
inh gathInFin : syn.gathEnv ⊑ inh.finEnv
syn outcome : (Errs inh.finEnv) ⊎ (Target inh.finEnv)
itf Target Γ -- interface for Target (parameterized) is not used in the example.

As we show later, at the root, we need the value of gathEnv to define finEnv. This requires gathEnv to be placed in a strict earlier visit. Hence we define two visits, ordered by appearance.

Attribute gathInFin has a dependent type: it specifies that gathEnv is a subsequence of finEnv. A value of this attribute is a proof that essentially states that we did not forget any identifiers. Similarly, in order to construct Target terms, we need to prove that finEnvdefines the identifiers that occur in the term. In the next section, we construct such proofs by applying data constructors. We may use inherited attributes as assumptions and pattern matches against values of attributes as case distinctions. Thus, with a

4 We may refer to an attribute that is declared earlier (in order of appearance) in the same interface. There is one exception due to the translation to Agda (Section 5): in the type of an inherited attribute, we may not refer to synthesized attributes of the same visit.

dependently typed AG we can formalize and prove correctness properties of our implementation. Agda’s type checker validates such proofs using symbolic evaluation driven by unification.

3.4 Semantics of Attributes

For each production, we give definitions for the declared attributes via rules. At the root, we pass the gathered environment back down as final environment. Thus, these two attributes are equal, and we can trivially prove that the final environment is a subsequence using either subRight or subLeft.

datasem Root prod root  -- rules for production root of nonterm Root
top.finEnv = top.gathEnv -- pass gathered environment down
top.gathInFin = subRight {[ ]} -- subsequence proof, using: [ ] ++ Γ_{4} ≡ Γ_{4}
lhs.finEnv = top.gathEnv -- pass gathEnv up
lhs.outcome = top.outcome -- pass outcomeup

For the use-production of Source, we check if the identifier (terminal loc.ι) is in the environment. If it is, we produce a Target term as value for the outcome attribute, otherwise we produce a scope error. For def, we introduce an identifier in the gathered environment. No errors can arise, hence we always produce a Target term. We prove (loc.ϕ_{1}) that the identifier loc.ι is actually in the gathered environment, and prove (loc.ϕ_{2}) using inSubset and attribute lhs.gathInFin that it must also be in the final environment. For ⋄ , we pass finEnvdown to both children, concatenate their gathEnvs, and combine their outcomes.

datasem Source  -- rules for productions of Source
prod use
lhs.gathEnv = [ ]  -- no names introduced
lhs.outcome \underline{with}loc.ι ∈_{?} lhs.finEnv  -- tests presence of ι
| inj_{1} notIn= inj_{1} [scope loc.ι notIn] -- when not in env
| inj_{2} isIn = inj_{2} (use loc.ι isIn)  -- when in env
prod def
lhs.gathEnv = [loc.ι]  -- one name introduced
loc.ϕ_{1}  = here {loc.ι} {syn.lhs.gathEnv}-- proof of ι in gathEnv
loc.ϕ_{2}  = inSubset lhs.gathInFin loc.ϕ_{1} -- proof of ι in finEnv
lhs.outcome = inj_{2} (def loc.ι loc.ϕ_{2})  -- never any errors
prod ⋄
lhs.gathEnv = left.gathEnv ++ right.gathEnv -- pass names up
left.finEnv = lhs.finEnv -- pass finEnvdown
right.finEnv = lhs.finEnv  -- pass finEnvdown
left.gathInFin = trans subLeftlhs.gathInFin  -- proof for left
right.gathInFin = trans (subRight {syn.lhs.gathEnv} {lhs.finEnv})
lhs.gathInFin  -- proof for right
lhs.outcome \underline{with}left.outcome  -- four alts.
| inj_{1} es \underline{with}right.outcome

| inj_{1} es_{1} | inj_{1} es_{2} = inj_{1} (es_{1} ++ es_{2}) -- 1: both in error
| inj_{1} es_{1} | inj_{2} = inj_{1} es_{1}  -- 2: only left
| inj_{2} t_{1} \underline{with}left.outcome
| inj_{2} t_{1} | inj_{1} es_{2} = inj_{1} es_{2}  -- 3: only right
| inj_{2} t_{1} | inj_{2} t_{2} = inj_{2} (t_{1} ⋄ t_{2})  -- 4: none in error

Out of the above code, we generate each production’s semantic function (and some wrapper code), such that these together with a catamorphism form a function that translates Source terms. The advantage of using AGs here is that we can easily add more attributes (and thus more properties and proofs) and refer to them.

4 AG Descriptions and their Core Representation

In the previous sections, we presented AGda(by example). To describe the dependentlytyped extension to AGs, we do so in terms of the core language AG{x \atop da} (a subset of AGda). Implicit information in AG descriptions (notational conveniences, the order of rules, visits to children) is made explicit in AG{x \atop da}. We sketch the translation from AGda to AG{x \atop da}. In previous work [4, 5], we described the process in more detail (albeit in a non-dependently typed setting).

AG{x \atop da} contains interface declarations, but grammar declarations are absent and semantic blocks encoded differently. Each production in AGda is mapped to a semantic function in AG{x \atop da}: it is a domain-specific language for the contents of semantic functions. A terminal x : τ of the production is mapped to a parameter loc_{l}x : τ. Implicit terminals are mapped to implicit parameters. A nonterminal x : N \overline{τ} is mapped to a parameter loc_{c}x:T′N \overline{τ}. The body of the production consists of the rules for the production given in the original AG{x \atop da} description, plus a number of additional rules that declare children and their visits explicitly.

sem⋄ : T′Source → T′Source → T′Source -- derived from (non)terminal types
sem⋄ loc_{c}left loc_{c}right =  -- semantic function for ⋄
sem : Source  -- AG{x \atop da} semantics block
child left: Source = loc_{c}left -- defines a child left
child right : Source = loc_{c}right -- defines a child right
invoke analyze of left  -- rule requires visiting analyze on left
invoke analyze of right  -- rule requires visiting analyze on right
invoke translate of left
invoke translate of right
lhs.gathEnv = left.gathEnv ++ right.gathEnv -- the AGda rules
...  -- etc.

A child rule introduces a child with explicitly semantics (a value of the type T′Source). Other rules may declare visits and refer to the attributes of the child. An invoke rule declares a visit to a child, and brings the attributes of that visit in scope. Conventional rules define attributes, and may refer to attributes. The dependencies between attributes induces a def-use (partial) order.

Actually, there is one more step to go to end up with a AG{x \atop da} description. A semantics block consists of one of more visit-blocks (in the order specified by the interface), and the rules are partitioned over the blocks. In a block, the lhs attributes of that and earlier visits are in scope, as well as those brought in scope by preceding rules. Also, the synthesized attributes of the visit must be defined in the block or in an earlier block. We assign rules to the earliest block that satisfies the def-use order. We convert this partial order into a total order by giving conventional rules precedence over child/invoke rules, and using the order of appearance otherwise:

sem⋄ : T′Source → T′Source → T′Source  -- signature derived from itf
sem⋄ loc_{c}left loc_{c}right =  -- semantic function for ⋄
sem : Source  -- AG{x \atop da} block
visit analyze  -- first visit
child left: Source = loc_{c}left  -- defines a child left
invoke analyze of left  -- requires child to be defined
child right : Source = loc_{c}right  -- defines a child right
invoke analyze of right  -- requires child to be defined

syn.lhs.gathEnv = syn.left.gathEnv ++ syn.right.gathEnv

visit translate  -- second visit
inh.left.finEnv  = inh.lhs.finEnv -- needs lhs.finEnv
inh.right.finEnv = inh.lhs.finEnv -- needs lhs.finEnv
inh.left.gathInFin = trans ...  -- also needs lhs.gathEnv
inh.right.gathInFin = trans ...  -- also needslhs.gathEnv
invoke translate of left  -- needs def of inh attrs of left
invoke translate of right  -- needs def of inh attrs of right
syn.lhs.outcome \underline{with}...  -- needs translate attrs of children

It is a static error when such an order cannot be satisfied. Another interesting example is the semantic function for the root: it has a child with a different interface as itself, and has two invoke rules in the same visit.

sem root : T′Source → T′Root  -- semantic function for the root
sem root locStop =  -- Source’s semantics as parameter
sem : Root visit compile  -- only one visit
child top : Source = loc_{c}top  -- defines a child top
invoke analyze of top  -- invokes first visit of top
inh.top.finEnv = syn.top.gathEnv -- passes gathered environment back
invoke translate of top  -- invokes second visit of top
syn.lhs.output = syn.top.gathEnv -- passes up the gathered env
syn.lhs.output = syn.top.outcome -- passes up the result

Figure 1 shows the syntax of AG{x \atop da}. In general, interfaces may be parametrized. The interface has a function type τ (equal to the type of the nonterminal declaration in AGda) that specifies the type of each parameter, and the kind of the interface (an upper bound of the kinds of the parameters). For an evaluation rule, we either use a \underline{with}-expression when the value of the attribute is conditionally defined, or use a simple

e ::= Agda[\overline{b}]  -- embedded blocks b in Agda
b ::= i | s | o  -- AG{x \atop da} blocks
o ::= inh.c.x | syn.c.x | loc.x -- embedded attribute reference
i ::= itf I \overline{x}: τ v  -- with first visit v, params x, and signature τ
v ::= visit x inh \overline{a} syn \overline{a} v -- visit declaration
|  -- terminator of visit decl. chain
a ::= x : e  -- attribute decl, with Agda type e
s ::= sem : I \overline{e} t  -- semantics expr, uses interface I \overline{e}
t ::= visit x \overline{r} t  -- visit definition, with next visit t
|  -- terminator of visit def. chain
r ::= p e′  -- evaluation rule
| invoke x of c  -- invoke-rule, invokes x on child c
| child c : I = e  -- child-rule, defines a child c, with interface I \overline{e}
p ::= o  -- attribute def
| .{e}  -- Agda dot pattern
| x \overline{p}  -- constructor match
e′::= \underline{with}e \overline{p′ e′^{?}}  -- Agda \underline{with}expression (e′absent when p′absurd)
| = e  -- Agda = expression
p′  -- Agda LHS
x, I, c -- identifiers, interface names, children respectively
τ  -- plain Agda type

Fig. 1: Syntax of ruler-core

equation as RHS. In the next section, we plug such an expression in a function defined via with-expressions, hence we need knowledge about the with-structure of the RHS.

5 Translation to Agda

To explain the preprocessing of AG{x \atop da}to Agda, we give a translation scheme in Figure 2 (explained via examples below). This translation scheme is a denotational semantics for AG{x \atop da}. Also, if the translation is correct Agda, then the original is correct AG{x \atop da}.

A semantics block in a AG{x \atop da} program is actually an algorithm that makes precise how to compute the attributes as specified by the interface: for each visit, the rules prescribe when to compute an attribute and when to visit a child. The idea is that we map such a block to an Agda function that takes values for its inherited attributes and delivers a dependent product^{5} of synthesized attributes. However, such a function would be cyclic: in the presented example, the result gathEnv would be needed for as input for finEnv. Fortunately, we can bypass this problem: we map to a k-visit coroutine instead.

5 A dependent product Σ τ f = (τ, f τ) parameterizes the RHS f with the LHS τ.

A coroutine is a function that can be invoked k times. We associate each invocation with a visit of the interface. Values for the inherited attributes are inputs to the invocation. Values for the synthesized attributes are the result of the invocation. In a pure functional language (like Agda), we can encode coroutines as one-shot continuations (or visit functions [8]).

itf I \overline{x}: \overline{τ_{x}} → τ v  _{iv}v \overline{x:τ_{x}} ; I,τ ; sig I : τ ; sig I = sig I (name v)
ivvisit x inh \overline{a} syn \overline{b} v \overline{g} ; I,τ _{iv}v _{I,τ}^{\overline{g}++ \overline{a}++ \overline{b}} -- interface type for later visits
sig I x : _{at} g_{1} → ...→ _{at} g_{n} → resultty τ
sig I x \overline{_{an} g} = _{a} inh.a_{1} → ...→ _{a} inh.a_{n} →
typrod (\overline{syn}.b) (sig I (name v))
iv \overline{g} ; I,τ  sig I =  -- terminator (some unit-value)
a x : e  atname x : e -- extract attribute name and type
at x : e  e  -- extract attribute type
an x : e  atname x  -- extract attribute name
sem x : I \overline{e} t  vis lhs (name t) \underline{where} _{ev}t _{I}^{\overline{e},∅} -- top of semfun
evvisit x \overline{r} t _{I}^{\overline{e},\overline{g}}  vis lhs x : sig I x \overline{e} \overline{_{an} g} -- type of visit fun
vis lhs x inhs I x = _{r} \overline{r} _{ς} -- chain of rules
ς  = valprod (syns I x) (vis lhs (name t))
\underline{where} _{ev}t _{I}^{\overline{g}++ \overline{a}++ \overline{b}}  -- next visit
ev _{I}^{\overline{e},\overline{g}}  vis lhs : sig I \overline{e} \overline{_{an} g} ; vis lhs =
r child c : I = e _{k}  \underline{with} e ...| vis I (firstvisitI) k -- k: remaining rules
r invoke x of c _{k} \underline{with} vis (itf c) x inhs (itf c) x -- pass inh values
...| (valprod (syns (itf c) x)) k  -- match syn values
r p e′ _{k}  _{ep} e′ _{p}^{k}  -- translation for attr def rule
ep \underline{with}e \overline{p e′} _{p}^{k}  \underline{with}e \overline{...| p _{r} p e′ _{k}} -- rule RHS is with-constr
ep = e _{p}^{k}  \underline{with}e ...| p k -- rule RHS is expr
atref inh.c.x = c_{i}x atname inh.x = inh_{a}x  -- naming conventions
atref syn.c.x= c_{s}x atname syn.x= syn_{a}x  -- atref : ref to attr value
atref loc.x = loc_{l}x atname x = x  -- atname: ref to attr in type
vis I x = vis lhs x  sig I = T′I  -- vis: name of visit function
vis c x = c_{v}x  sig I x = T′I′x  -- sig: itf types

Fig. 2: Translation of AG{x \atop da} to Agda.

We generate types for coroutines and for the individual visit functions that make up such a coroutine. These types are derived from the interface. For each visit (e.g. translate of Source), we generate a type that represents a function type from the attribute types of the inherited attributes for that visit, to a dependent product (Σ) of the types of the synthesized attributes and the type of the next visit function. These types are parameterized with the attributes of earlier visits (e.g. T′Source′translate syn_{a}gathEnv). The type of the coroutine itself is the type of the first visit.

T′Source  = T′Source′analyze
T′Source′analyze = Σ Env T′Source′translate
T′Source′translate syn_{a}gathEnv =

(inh_{a}finEnv : Env) → (inh_{a}gathInFin : syn_{a}gathEnv ⊑ inh_{a}finEnv) →

Σ (Errs inh_{a}finEnv⊎ Target inh_{a}finEnv)

(T′Source′ syn_{a}gathEnv inh_{a}finEnvinh_{a}gathInFin)

T′Source′ syn_{a}gathEnv inh_{a}finEnvinh_{a}gathInFin syn_{a}outcome =

The restrictions on attribute order in the interface ensure that referenced attributes are in scope. The scheme for _{iv}v _{g,τ}^{I} formalizes this translation, where g is the list of preceding attribute declarations, and τ the type for I. The typrod function mentioned in the scheme constructs a right-nested dependent product.

The coroutine itself consists of nested continuation functions (one for each visit). Each continuation takes the visit’s inherited attributes as parameter, and consists of a tree of with-constructs that represent intermediate computations for computations of attributes and invocations of visits to children. Each leaf ends in a dependent product of the visit’s synthesized attributes and the continuation function for the next visit^{6}.

sem⋄ : T′Source → T′Source → T′Source  -- example translation for ⋄
sem⋄ loc_{c}left loc_{c}right = lhs_{v}analyze \underline{where}  -- delegates to first visit function
lhs_{v}analyze : T′Source′analyze  -- signature of first visit function
lhs_{v}analyze \underline{with}...  -- computations for analyze here
...= (lhs_{s}gathEnv, lhs_{v}translate) ahwere  -- result of first visit function
lhs_{v}translate : T′Source′translate lhs_{s}gathEnv -- last visit function
lhs_{v}translate lhs_{i}finEnvlhs_{i}gathInFin \underline{with}... -- computations for translate here
...= (lhs_{s}outcome, lhs_{v} ) \underline{where}  -- result of second visit function
lhs_{v} : T′Source′ lhs_{s}gathEnv lhs_{i}finEnvlhs_{i}gathInFin lhs_{s}outcome
lhs_{v} =  -- explicit terminator value

The scheme _{ev}v _{I}^{\overline{e},\overline{g}} formalizes this translation for a visit v of interface I, where \overline{e} are type arguments to the interface (empty in the example), and \overline{g} are the attributes of previous visits.

The with-tree for a visit-function consists of the translation of child-rules, invokerules and evaluation rules. Each rule plugs into this tree. For example, the translation for child left: Source = loc_{s}left is:

... \underline{with}loc_{s}left  -- evaluate RHS to get first visit fun
...| left_{v}analyze \underline{with}... -- give it a name + proceed with remainder

For invoke translate of left the translation is:

... \underline{with}left_{v}translate left_{i}finEnvleft_{i}gathInFin -- visit fun takes inh attrs
...| (left_{s}outcome, left_{v}sentinel) \underline{with}...  -- returns product of syn attrs

6 As a technical detail, a leaf of the with-tree may also be an absurd pattern. These are used in Agda to indicate an alternative that is never satisfyable. A body for such an alternative cannot be given.

For lhs.gathEnv = left.gathEnv ++ right.gathEnv :

... \underline{with}left_{s}gathEnv ++ right_{s}gathEnv -- translation for RHS
...| lhs_{s}gathEnv \underline{with}...  -- LHS + remainder

For lhs.outcome \underline{with}... (where the RHS is a with-construct), we duplicate the remaining with-tree for each alternative of the RHS:

... \underline{with}left_{s}outcome  -- translation for RHS
...| inj_{1} es \underline{with}right_{s}outcome
...| inj_{1} es_{1} | inj_{1} es_{2} \underline{with}inj_{1} (es_{1} ++ es_{2}) -- alternative one of four
...| inj_{1} es_{1} | inj_{1} es | lhs_{s}outcome \underline{with}... -- LHS + remainder
...| inj_{1} es_{1} | inj_{2} \underline{with}inj_{1} es_{1} -- alternative two of four
...| inj_{1} es_{1} | inj_{2}  | lhs_{s}outcome \underline{with}... -- LHS + remainder
...| inj_{2} ...  -- remaining two alternatives

The scheme _{r} r _{k} formalizes this translation, where r is a rule and k the translation of the rules that follow r.

The size of the translated code may be exponential in the number of rules with withconstructs as RHS. It is not obvious how to treat such rules otherwise. Agda does not allow a with-construct as a subexpression. Neither can we easily factor out the RHS of a rule to a separate function, because the conclusions drawn from the evaluation of preceding rules are not in scope of this function. Fortunately, for rules that would otherwise cause a lot of needless duplication, the programmer can perform this process manually.

When dependent pattern matching brings assumptions in scope that are needed across rules, the code duplication is a necessity. To facilitate that pattern matching effects are visible across rules, we need to ensure that the rule that performs the match is ordered before a rule that needs the assumption. We showed in previous work how such non-attribute dependencies can be captured [4].

The translated code has attractive operational properties. Each attribute is only computed once, and each node is at most traversed k times.

6 Partially Defined Attributes

A fine granularity of attributes is important to use an AG effectively. In the minicompiler of Section 3, we could replace the attribute outcome with an attribute code and a separate attribute errors. This would be more convenient, since it would not require a pattern match against the output attribute to collect errors. However, we cannot produce a target term in the presence of errors, thus code would not have a total definition. Therefore, we were forced to combine these two aspects into a single attribute outcome. It is common to use partially defined attributes in an AG. This holds especially when the attribute’s value (e.g. errors) determines if another attribute is defined (e.g. code). We present a solution that uses the partitioning of attributes over visits.

The idea is to make the availability of visits dependent on the value of a preceding attribute. We split up the translate visit in a visit report and a visit generate. The visit report has errors as synthesized attribute, and generate has code. Furthermore, we enforce that generate may only be invoked (by the parent in the AST) when the list of errors reported in the previous visit is empty. We accomplish this with an additional attribute noErrors on generate that gives evidence that the list of errors is empty. With this evidence, we can give a total definition for code.

itf Source -- Root’s visit needs to be split up in a similar way
visit report syn errors : Errs inh.finEnv -- parent can inspect errors
visit generate inh noErrors : syn.errors ≡ [ ] -- enforces invariant
syn code : Target inh.finEnv -- only when errors is empty
datasem Source prod use -- example for production use
loc.testInEnv = loc.ι ∈_{?} lhs.finEnv  -- scheduled in visit report
lhs.code \underline{with}loc.testIn | lhs.noErrors -- scheduled in visit generate
| inj_{1} | () -- cannot happen, hence an absurd pattern
| inj_{2} isIn | refl = use loc.ι isIn  -- extract the evidence needed for the code term
datasem Source prod ⋄ -- leftNil: (α: Env) → (β: Env) → (α + + β ≡ [ ]) → (α ≡ [ ])
left.noErrors = leftNilleft.errors right.errors lhs.noErrors -- right.noErrors similar
lhs.code  = left.code ⋄ right.code -- scheduled in visit generate

For this approach work, it is essential that visits are scheduled as late as possible, and only those that are needed.

We can generalize the presented approach by defining a fixed number of alternative sets of attributes for a visit, and use the value of a preceding attribute to select one of these sets [6].

7 Related Work

Dependent types originate in Martin-Löf’s Type Theory. A variety of dependently typed programming languages are gaining popularity, including Agda [7], Epigram, and Coq. We present the ideas in this paper with Agda as host language, because it has a concept of a dependent pattern match, to which we straightforwardly map the left-hand sides of AG rules. Also, in Coq and Epigram, a program is written via interactive theorem proving with tactics or commands. The preprocessor-based approach of this paper, however, suits a declarative approach more.

Attribute grammars [3] are considered to be a promising implementation for compiler construction. Recently, many Attribute Grammar systems arose for mainstream languages, such as the systems JastAdd and Silver for Java, and UUAG [10] for Haskell. These approaches may benefit from the stronger type discipline as presented in this paper; however, it would require an encoding of dependent types in the host language.

AGs have a straightforward translation to cyclic functions in a lazy functional programming language [9]. To prove that cyclic functions are total and terminating is a non-trivial exercise. Kastens [2] presented Ordered Attribute Grammars (OAGs). In OAGs, the evaluation order of attribute computations as well as attribute lifetime can be determined statically. Saraiva [8] described how to generate (noncyclic) functional coroutines from OAGs. The coroutines we generate are based on these ideas.

8 Conclusion

We presented AGda, a language for ordered AGs with dependently typed attributes: the type of an attribute may refer to the value of another attribute. This feature allows us to conveniently encode invariants in the type of attributes, and pass proofs of these invariants around as attributes. With a dependently typed AG, we write algebras for catamorphisms in a dependently typed language in a composable way. Each attribute describes a separate aspect of the catamorphism.

The approach we presented is lightweight, which means that we encode AGs as an embedded language (via a preprocessor), such that type checking is deferred to the host language. To facilitate termination checking, we translate the AG to a coroutine (Section 5) that encodes a terminating, multi-visit traversal, under the restriction that the AG is ordered and definitions for attributes are total.

The preprocessor approach fits nicely with the interactive Emacs mode of Agda. Type errors in the generated program are traceable back to the source: in a statically checked AGda program these can only occur in Agda blocks. These Agda blocks are literally preserved; due to unicode, even attribute references can stay the same. Also, the Emacs mode implements interactive features via markers, which are also preserved by the translation. The AG preprocessor is merely an additional preprocessing step.

With some generalizations, the work we have presented is a proposal for a more flexible termination checker for Agda that accepts k-orderable cyclic functions, if the function can be written as a non-cyclic k-visit coroutine.

Acknowledgments. This work was supported by Microsoft Research through its European PhD Scholarship Programme. We thank the anonymous reviewers of IFL’10 for their extensive comments and suggestions during the post-refereeing process.

References

1. Bove, A., Dybjer, P.: Dependent Types at Work. In: Language Engineering and Rigorous Software Development. LNCS, vol. 5520, pp. 57–99 (2009)

2. Kastens, U.: Ordered Attributed Grammars. Acta Informatica 13, 229–256 (1980)

3. Knuth, D.E.: Semantics of Context-Free Languages. Mathematical Systems Theory 2(2), 127–145 (1968)

4. Middelkoop, A., Dijkstra, A., Swierstra, S.D.: Attribute Grammars with Side Effect. In: HOSC (2010), http://people.cs.uu.nl/ariem/wgt10-journal.pdf

5. Middelkoop, A., Dijkstra, A., Swierstra, S.D.: Iterative Type Inference with Attribute Grammars. In: GPCE ’10. pp. 43–52 (2010)

6. Middelkoop, A., Dijkstra, A., Swierstra, S.D.: Visit Functions for the Semantics of Programming Languages. In: WGT ’10 (2010), http://people.cs.uu.nl/ariem/wgt10-visit.pdf

7. Norell, U.: Dependently-typed Programming in Agda. In: TLDI ’09. pp. 1–2 (2009)

8. Saraiva, J., Swierstra, S.D.: Purely Functional Implementation of Attribute Grammars. Tech. rep., Universiteit Utrecht (1999)

9. Swierstra, S.D., Alcocer, P.R.A.: Attribute Grammars in the Functional Style. In: Systems Implementation 2000. pp. 180–193 (1998)

10. Universiteit Utrecht: Homepage of the Universiteit Utrecht Attribute Grammar System. http://www.cs.uu.nl/wiki/HUT/AttributeGrammarSystem (1998)