Type-scoped advice is put into good use to bring in new cases of
toSpine
for the ever-growing set of data types. For example,toSpine [1,2,3]
producesApp (App (Con (Descr (:)) 1) [2,3])
This shallow encoding is pushed inwards by generic functions that make use of it, as we will see shortly. Since all data types are now mapped to a single one,
Spine
, we can easily define functions that work on this representation. For example, the following code collects strings from a structure.strings :: a -> [String]
strings x = strings’ (toSpine x) strings’ :: Spine a -> [String]
strings’ (Con c) = []
strings’ (App f x) = strings’ f ++ strings x
The intention of the above program is to uniformly traverse the structures of any data types (including strings seen as lists of Chars). To be able to collect strings, we need a small exception of this generic behavior that returns a string when the input is a string. This is another type-directed operation. It is tempting to use type-scoped advice here to advise
strings
. However, we notice that the call tostrings
in the body ofstrings’
is given the second argument ofApp
as input, whose type is existentially quantified in the definition ofSpine
and is not available statically. This makes type-scoped advice, together with any other type-directed-programming mechanisms that relies on static resolution, not applicable.A standard technique for handling this exception case, which can be found in the generic programming literature, is to use dynamic ‘‘type’’ testing based on some kinds of term encodings of types [12,13,7]. Independently, encoding of dynamic type casting in statically type languages [24,3] is also available. Here, we choose to follow Hinze and Löh [7] by wrapping a value of type
a
with a type representation to form a data type,Typed a
, and use acast
function that compares the type representation with a target type. As a result, the exceptional case of string inputs can be handled by the following advice.n@advice around {strings} (x) =
case cast x :: Maybe String of Just s -> [s]
Nothing -> proceed x
This advice intercepts all executions of
strings
. When the input is dynamically verified to be a string, we return that string in the result; otherwise, control is passed back tostrings
if there is no other intercepting advice. (We need to adapt the earlier definition oftoSpine
to acceptTyped a
as its argument type. The detail is omitted here.)We think this ability of accepting dynamic type casting with aspects is one of the strengths of AOP, since it allows modular extensions. Suppose we later implement a data type of ASCII code of characters and wish to consider a list of ASCII’s as a string, function
strings
can be easily extended with another special case using the following aspect.n1@advice around {strings} (x) =
case cast x :: Maybe [Ascii] of Just s -> [s]
Nothing -> proceed x
This modular extensibility is difficult to achieve with other type-directed approaches such as Haskell type classes. It is worth mentioning that just like encodings of dynamic typing do not render static typing obsolete, the use of type casts in advices does not replace static weaving.
Programs π ::= dinπ |e Declarations d ::= x=e|f =e|
n::σ@advice around{pc}(arg) =e Arguments arg ::= x|x::t
Pointcuts pc ::= ppc|pc+cf |pc−cf Primitive PC’s ppc ::= fx¯|any|any\[¯f] |n Cflows cf ::= cflow(f) |cflow(f(_::t)) |
cflowbelow(f) |cflowbelow(f(_::t))
Label l ::= f :t|
Expressions e ::= c|x|λlx:t.e|e e|letx = eine| e{t} |Λa.e|proceed|tjp Types t ::= Int|Bool|a|t→t| [t] Type Schemes σ ::= ∀¯a.t
Fig. 3. Syntax of EA.
Expressions e ::= · · · |th
AdvStore A ::= Adv
Advice Adv ::= (n:σ,pc,t,e) Environments E ::= x7→th
Values v ::= c|cl
Thunk th ::= (|e, E|) |cl
Closure cl ::= (|λlx:t.e, E|) | (|Λa.e, E|)
Fig. 4. Semantic domains for EA.
3. The semantics ofAspectFun
This section presents an operational semantics forAspectFun. As type information is required at the triggering of advice for execution, our semantics is presented in terms of an explicitly typed version ofAspectFun, referred asEAin the following discussion.Fig. 3displays the syntactic constructs ofEA.
The syntactic structure ofEAremains the same as that ofAspectFun. The main enhancements are four type-related constructs at the expression level. The constructs of type applications and type abstractions are standard ones; they are denoted by e
{
t}
andΛa.
e, respectively. The type annotations for lambda parameters are also common in explicitly typed languages. The only new construct is a set of labels which annotate lambda expressions that can be the target of advice weaving. Essentially, a label specifies the name and the type of a function with which the lambda expression is associated via a top-level declaration. Hence, a label identifies a join point and its type context.The types and type schemes ofEAfollow the convention of the Hindley–Milner type system. The semantics specification ofEAincludes the following notations on types. We write t D t0, denoting that type t is more general than or equivalent to type t0, iff there exists a substitution S over type variables in t such that St
=
t0, and the notation, S=
t D t0, is an abbreviation for it. We write t≡
t0iff t D t0and t0 D t. When t D t0but t6≡
t0, we say t is more general than t0. Similarly, we say a type t is more specific than a type t0if t0 D t and t6≡
t0. Finally, the most general unifier between two types, t and t0, is denoted by mgu(
t,
t0)
.Conversion fromAspectFuntoEAis done by the standard Hindley–Milner type inference with few straightforward enhancements. First, type abstractions and type applications are made explicit. Second, when inferring the type for a piece of advice, invocation of the underlying advised function via proceed is treated as a recursive function call. Finally, top-level lambda expressions are annotated with labels that specify the name and type of the function they define.
3.1. Operational semantics forEA
The operational semantics forEAis specified in terms of the judgementE
;
A` π ⇓ v
, whereπ
is anEAprogram,E is an environment that maintains the bindings of variables and functions, andAis a repository that keeps advice-related information derived from advice declarations inπ
. We shall often refer to the environment and advice store pair as the operational semantics context for brevity. The full semantic domains and the set of environment-based, big-step reduction rules to define the judgement are shown inFigs. 4and5, respectively.We adopt call-by-name evaluation forEA.4Thus we add a new form of expression, called thunk, which is only used in the operational semantics, but not in the source expression. A thunk is a pair of an expression and an environment. When the
4 Note that Haskell uses call-by-need evaluation.
(OS:Value) E ; A `c⇓c
Fig. 5. Operational semantics for EA.
expression in a thunk is a lambda expression or a type abstraction, the thunk is called a closure. Constants and closures are considered values inEAand will not be further evaluated. Finally, during the evaluation of anEAprogram, the environment associates a name with a thunk as its binding. We writeE
[
y7→
th]
for the environment which extendsEby assigning thunk th to variable y, assuming that any name clash has been resolved via proper renaming.Among the reduction rules for EA three rules, namely (OS:Decl), (OS:Adv) and (OS:Adv-An), process top-level declarations; and the rest of rules handle various forms of expressions. Rule (OS:Decl) makes a thunk out of the defining expression of a global variable or function and the current environment, and then puts it into the environment for further evaluation of the underlying program. On the other hand, rules (OS:Adv) and (OS:Adv-An) collect the set of advice declared in a program and deposit it in the advice store,A. BothAandEare essential to the evaluation of the expression inside an EAprogram.
The (OS:Adv) rule simply delegates the collection task to the (OS:Adv-An) rule, making non-type-scoped advice a special case of type-scoped advice with the inferred parameter type as the scope. The (OS:Adv-An) performs the real work of advice collection: organizing a type-scoped advice into a quadruple,
(
n: σ ,
pc,
t,
e)
, and appending it to the advice storeA. The quadruple consists of advice name type pair, pointcut, type scope and thunkified advice body.As to the reduction rules for expressions ofEA they mostly follow the standard ones for a typed lambda calculus with constants. The only exception is the rule for function application, (OS:App), which also handles the triggering and weaving of advice. Specifically, the closure to apply and the label associated with it are passed to the advice triggering function Trigger, which is specified inFig. 6together with other auxiliary function declarations. The Trigger function first chooses the set of eligible advice based on the label and the argument type, and weaves them into the function invocation – through a series of environment extension of advice closures – for execution. Note that, although we adopt the call-by-name evaluation strategy, our weaving scheme does not rely on this choice.
Three points worth mentioning here. First, in the main body of Weave function, the function Trigger is invoked again to handle any possible triggering of second-order advice. Second, among the advice matched by JPMatch, the function Choose keeps all the advice whose type scope is more general than the type passed to it, regardless of its return type. Consequently, it is likely that, during the subsequent execution of the woven advice, a run-time type error may occur and the reduction fails (unless, of course, the program has been analyzed to be safe by our type system). Third, the set of advice selected by Choose is kept in a list and ordered according to the sequential ordering of their declarations in the program. While we believe
Trigger : e×l→e
Trigger(e, ) =e
Trigger((|λx:tx.e, Ef|),f :tf) =Weave((|λx:tx.e, Ef|),tf,Choose(f,tx))
Weave : e×t×Adv→e
Weave(e,tf, []) =e
Weave(ef,tf,adv :advs) = Let (n: ∀¯a.tn,pc,t, (|Λ¯a.e, En|)) =adv
¯t be types such that[¯t/¯a]tn=tf
ep=Weave(ef,tf,advs) (λn:tn0x:tx.ea) = [¯t/¯a]e
In Trigger((|λx:tx.ea, En.proceed=ep|),n:tn0) Choose(f,t) = [(ni:σi,pci,ti,ei) | (ni:σi,pci,ti,ei) ∈ A,ti D t,
∃pc∈pcis.t.JPMatch(f,pc)]
JPMatch(f,pc) = (f ≡pc) ∨ (pc≡any) ∨ (pc≡any\ [ ¯h] ∧f 6∈ ¯h)
Fig. 6. Operational semantics for EA: Auxiliary function declarations.
that the issue of chaining order is orthogonal to our study here, it is understood that advice is to be chained in a specific order during execution. Hence, we fix the order in our semantics definition, and assume that the order chosen during static weaving (Section4) is the same.
3.2. Example
We use a contrived example to demonstrate how the semantics ofAspectFunworks. TheAspectFunprogram listed in Example 3includes three kinds of advice, namely type-scoped advice, polymorphic advice and second-order advice. They will be triggered according to the type context at different join points during the execution of the program.
Example 3.