Ruler Strategy
ArieMiddelkoop
Entities
Rule
A rule is a relation between attributes.Attribute
An attribute is either a value or a rule. An attribute has properties: a type and a direction.Issues
- Grouping mechanism for attributes
- Separate specification of attribute flow
- Explicit rules versus implicit rule applications
- First-class rules
Grouping mechanism
Attribute flow
Explicit/Implicit
First-classness
Allow rules to be first-class. The type of a rule is its dependencies.Extensions
Type variables in AST
Add type variables to AST specification:
ast Expr n
| Var
nm : n
| App
fun : Expr n
arg : Expr n
| Lam
nm : n
body : Expr n
* Treat the type variables as non-terminals. Rule application dependent on choice type variables.
* Treat the type variables as terminals. First-class rules and dependencies? Higher-order type constructors?
Outdated crap follows...
Patterns
The goal of the ruler project is to come up with an incremental way of specifying type rules. One way is to start with a declarative formulation of a type rule and add additional information to transform it an algorithmic variant. In this section, we explore the other direction: start with an algorithmic variant and add syntax to get closer to the declarative formulation.Environments
Environments are responsible for lots of obfuscation in the type rules of EHC. For example, the rule for declarations involve at least four explicitly named gamma's, of which two actually occur on both sides of the turn style (see figure 5.1 of Atze's printed thesis). On the other hand, the rule for expressions only contain one environment. The difference between these environments are actually only important when mapping the type rules to an executable model. In a declarative model, these environments are allowed to be represented by only a single environment. Consider the type rules for declarations (Figure 4.4 of Atze's thesis). Replace all Gammas by a single Gamma and put them to the left side of the turn style. We lose some information this way. We cannot use the operations on the environments to check four doubly defined identifiers. Also, an oracle has to guess which mappings should be in the environment. For a declarative formulation of the type rules, this is not an issue. However, we cannot generate an implementation from this new formulation anymore, unless we supply additional information.
Invariant (general):
Gamma contains a mapping between identifiers and the corresponding type.
This is an invariant that has to hold for any environment named Gamma.
We need other invariants to hold in other circumstances:
Invariant (after typing has finished):
Gamma:fin contains a mapping for exactly those identifiers in scope to their final type (after type reconstruction).
Invariant (during typing):
Gamma:syn contains a mapping for exactly those identifiers that occur in type signatures in scope, with their corresponding type (obtained from the abstract syntax)
goal: to be able to specify these invariants as separate aspects, in isolation.
Observation: we can already accomplish this with AG. However, for some of these invariants, there is interaction with other aspects (like constraints of type inference). Inversion of control: declare that a certain aspect that satisfies a certain invariant is required and let the ruler system combine the aspects together.
Some idea: - Use ATTR-like AG constructs to indicate which nonterminals have access to a certain attribute.
- Use ATTR-like AG constructs to indicate directions and other information for specific aspects of an attribute.
- Use rules to construct attribute 'flow'.