We propose a Java-like calculus where declared variables can be annotated by coefects specifying constraints on their use, such as linearity or privacy levels. Annotations are written in the language itself, as expressions of type Coeffect, a predefined class which can be extended by user-defined subclasses, modeling the coefects desired for a specific application. We formalize the type system and prove subject reduction, which includes preservation of coefects, and show several examples.
Type-and-coefect systems [1, 2, 3, 4, 5, 6, 7, 8] are type systems where the typing judgment takes an enriched form, such as x1 :c1 C1, . . . , x :c C ⊢ e : C , with c1, . . . , c coefects modeling how the corresponding variables are used in e.
For instance, coefects of shape c ::= 0 | 1 | trace when a variable is either not used, or used linearly (that is, exactly once), or used in an unrestricted way, respectively, in the expression e. In this way, functions, e.g., x :int.5, x :int.x , and x :int.x + x , which have the same type in the simply-typed lambda calculus, can be distinguished by adding coefect annotations: x :int[0].5, x :int[1].x , and x :int[].x + x . Other typical examples are exact usage (coefects are natural numbers), and privacy levels. Coefects usually form a semiring, specifying sum +, multiplication · , and 0 and 1 constants, satisfying some natural axioms. Moreover, some kind of order relation is often required as well.
This approach has been exploited to a fully-fledged programming language in Granule [ 6], a functional language equipped with a type-and-coefect system, hence allowing the programmer to write function declarations as those above. In Granule, diferent kinds of coefects can be used at the same time, including naturals for exact usage, security levels, intervals, infinity, and products of coefects; however, the available coefects are fixed once and for all.
In this paper, we investigate the possibility of providing a similar support in Java-like languages, by allowing the programmer to write coefect annotations in variable declarations. Moreover, we rely on the inheritance mechanism of OO languages to allow the programmer to write her/his own coefects. More in detail, coefect annotations are expressions of (subclasses of) a predefined class Coeffect, analogously to Java exceptions which are expressions of (subclasses of) Exception.
In Sect. 2 we define the underlying calculus, and in Sect. 3 the type-and-coefect system, stating its soundness. In Sect. 4 we show some examples. We discuss further work in Sect. 5.
The syntax and operational semantics of the language are shown in Fig. 1. We write es as metavariable for e1, . . . , e, ≥ 0, and analogously for other sequences. We assume sets of variables x , y , z , . . ., including the special variable this, class names C , field names f , and method names m. Besides the standard predefined class Object, root of the inheritance hierarchy, we assume another predefined class Coeffect, whose definition will be given in the next section. A subclass of Coeffect is called a coefect class .
e ::= x | e.f | new C (es) | e.m(es) | {C [v^] x = e; e′}
| case e of (C1[v^1] x1)e1 (C2[v^2] x2)e2 v ::= new C (vs) ℰ ::= [ ] | ℰ.f | new C (vs, ℰ, es) | ℰ.m(es) | v .m(vs, ℰ, es) | {C [v^] x = ℰ; e} | case ℰ of (C1[v^1] x1)e1 (C2[v^2] x2)e2 expression value evaluation context e → e′ (ctx) ℰ[e] → ℰ[e′] (field-access)
fields(C ) = C1 f1; . . . C f; new C (v1, . . . , v).f → v ∈ 1.. (invk) new C (vs).m(v1, . . . , v) → e′ em′b=odey[(nCew,mC)(=vs()x/1t.h.i.sx][v,e1/)x1] . . . [v/x] (block) {C [v^] x = v ; e} → e[v /x ] (case-1) (case-2) case new C (vs) of (C1[v^1] x1)e1 (C2[v^2] x2)e2 → e1[new C (vs)/x1] C ̸≤ C1 case new C (vs) of (C1[v^1] x1)e1 (C2[v^2] x2)e2 → e2[new C (vs)/x2] C ≤ C2 C ≤ C1
In addition to standard constructs (variable, field access, constructor and method invocation, and block) we include a typecase construct, since in coefect classes a check of the runtime type will be typically needed to write binary methods, see the examples in Sect. 4. In the calculus, we choose this compact construct, essentially the same used in [9], to keep the syntax minimal; it could be encoded in true Java by using conditional, instanceof, and cast.
A block expression consists of the declaration of a local variable, and the body in which this variable can be used. A variable declaration specifies a type (a class name C ), an initialization expression e, and a coefect annotation v^, which is syntactically a value1; however, we use the meta-variable v^ rather than v to suggest that it is expected to be a value of a coefect class. The syntax of coefect annotations is inspired by that used in Granule [6].
A typecase expression consists of an initial expression e, and two alternatives, each one specifying a local variable with its type and coefect annotation, and an expression. Expression e1 is executed if the result of the initial expression has a subtype of C1, with x1 bound to such result; otherwise, expression e2 is executed, with x2 bound to the result, provided that it has a subtype of C2. This second check is guaranteed to always succeed by the type system.
Reduction rules in Fig. 1 are straightforward. To be concise, the class table is abstractly modeled as follows, omitting its (standard) syntax: • ≤ is the subtyping relation (the reflexive and transitive closure of the extends relation) • fields(C ) gives, for each class C , the sequence of fields with their types, the inherited first • mbody(C , m) gives, for each method m of class C , parameters and body.
The type system uses coefects c ::= n | v^, with n ∈ N, and v^ user-defined coefect , that is, value expected to be of a coefect class.
The typing judgment has shape Γ ⊢ e : C , where Γ is a (type-and-coefect) context, that is, a (finite) map from variables to pairs of a coefect and a type (class name), written Γ = x1 :c1 C1, . . . , x :c C. Equivalently, Γ can be seen as the pair of a coefect context and a type context, maps from variables to coefects and types, respectively, with the same domain.
As customary in type-and-coefect systems, in typing rules contexts are combined by means of some operations, which are, in turn, defined in terms of the corresponding operations on coefects. We first define the operations on contexts, then we show the typing rules, and finally we define how the assumed operations on coefects are derived from user-defined methods in coefect classes.
The operations on contexts are the following: Sup Sum ∅ ∨ Γ = Γ (x :c C , Γ) ∨ Δ = x :c C , (Γ ∨ Δ) if x ∈/ dom(Δ) (x :c C , Γ) ∨ (x :c′ C , Δ) = x :c∨c′ C , (Γ ∨ Δ) Partial order
(x :c C , Γ) ≤ (x :c′ C , Δ) if c′ ≤ c and Γ ≤ Δ ∅+Γ = Γ (x :c C , Γ)+Δ = x :c C , (Γ+Δ) if x ∈/ dom(Δ) (x :c C , Γ)+(x :c′ C , Δ) = x :c+c′ C , (Γ+Δ) 1Coefect annotations could be generalized to be arbitrary expressions; here we use this simpler assumption to make the presentation lighter.
Γ ⊢ e : C ′ (t-sub) Γ ⊢ e : C
C ′ ≤ C As the reader can note, operations on coefect contexts are obtained by pointwise application of the corresponding operations on coefects, and then they are lifted to type-and-coefect contexts. In this lifting, sum becomes partial since a variable in the domain of both contexts is required to have the same type.
The typing rules are given in Fig. 2. In the subsumption rule (t-sub), the type can be made more general, as usual. The context could, symmetrically, be made more specific ( Γ ≤ Γ′), by pointwise overapproximating coefects; however, to stress that they can be actually computed bottom-up, we prefer a presentation where overapproximation of coefects is an explicit side condition of the rules where it is needed, see rules (t-block) and (t-case).
In rule (t-var), the given variable is used exactly once. In rules (t-field-access) and (t-new), coefects of the subterms are summed.
In rule (t-invk), the coefects of the arguments are summed, after multiplying each of them with the sup (greatest lower bound) of the coefect annotation of the corresponding parameter, and the one coefect. The sup with the one coefect guarantees to take into account the coefects of the initialization expression for parameters not used in the body, see the last part of Example 2 in Sect. 4. This is customary in type-and-coefect systems for call-by-value calculi. The rule uses the auxiliary function mtype which returns an enriched method type, where the types of the parameters and of this have coefect annotations. Such coefect annotations should have a coefect class as type. Formally, if mtype(C , m) = v^0, C1v^1 . . . Cv^ → C , then ∅ ⊢ v^ : Coeffect for ∈ 0... Moreover, mtype(C , m) and mbody(C , m) should be either both undefined or both defined with the same number of parameters; in the latter case, the method body should be well-typed with respect to the method type, notably by typechecking the method body we should get coefects which are (overapproximated by) those specified in the annotations. Formally, if mbody(C , m) = (x1 . . . x, e), and mtype(C , m) = v^0, C1v^1 . . . Cv^ → C , the following condition must hold: (t-meth) this :c0 C , x1 :c1 C1, . . . , x :c C ⊢ e : C c ≤ v^ ∀ ∈ 0..
In rule (t-block), the coefects of the initialization expression are multiplied by the sup of the coefect annotation of the variable, and the one coefect, and then summed with those of the body. Analogously to method invocation, the sup with the one coefect is needed when the variable is not used in the body. The side condition c ≤ v^ checks that the variable is used in the body accordingly with the annotation v^ written by the programmer. The premise ∅ ⊢ v^ : Coeffect checks that v^ is a user-defined coefect. In rule (t-case), coefects are handled analogously as in rule (t-block). The first side-condition ensures that the cases are exhaustive.
We describe now how operations on coefects are derived from user-defined methods in the coefect classes. The predefined class Coeffect is defined as follows: class Coeffect {
Coeffect sup(Coeffect c) { new Coeffect() } Coeffect sum(Coeffect c) { new Coeffect() } Coeffect mult(Coeffect c) { new Coeffect() } Coeffect zero() { new Coeffect() }
Coeffect one() { new Coeffect() } }
Being subclasses of Coeffect, coefect classes implement the above methods, corresponding to the expected operations on coefects: sup, sum, multiplication, zero, and one. In the class Coeffect, such operations are those of the trivial semiring consisting of only one element.
Let nf(e) denote the normal form of e. The normal form, if any, is unique, since it is easy to see that the reduction relation is deterministic. Moreover, we assume that methods sup, sum, mult, zero, and one in coefect classes always terminate, so that normal forms in the definitions below are defined.
Recall that coefects are either natural numbers or user-defined coefects (values of a coefect
class). Natural numbers are internally used2 by the type system, notably in rule (t-var) which is
independent from coefect classes in the program. As a consequence, operations on coefects
derived from user-defined methods need to handle natural numbers as well. This is achieved
through a translation into user-defined coefects, which corresponds to the unique
homomorphism from the initial semiring to another one. That is, inv^(n) is the user-defined coefect
corresponding to n in the class of v^, defined by:
inv^(0) = nf(v^.zero()) inv^(
We can now define operations on coefects. To avoid confusion, standard operations on natural numbers have the explicit subscript N. 2Derivations in Example 2 illustrate their interplay with user-defined coefects.
Sup Sum v^∨n = nf(v^.sup(inv^(n))) n∨v^ = nf(inv^(n).sup(v^)) v^1∨v^2 = nf(v^1.sup(v^2)) n1∨n2 = maxN(n1, n2) v^ + n = nf(v^.sum(inv^(n))) n + v^ = nf(inv^(n).sum(v^)) v^1 + v^2 = nf(v^1.sum(v^2)) n1 + n2 = n1 +N n2 Multiplication v^ × n = nf(v^.mul(inv^(n))) n × v^ = nf(inv^(n).mul(v^)) v^1 × v^2 = nf(v^1.mul(v^2)) n1 × n2 = n1 × N n2 Note that the order ≤ on coefects can be derived from the ∨ operator, as follows: c1 ≤ c2 if c1∨c2 = c2. We prefer to implement the sup operator, rather than the order, in coefect classes, since the latter would require to include the primitive type boolean in the calculus.
Our main technical result is subject reduction (Theorem 1), expressing, as customary in
type-and-coefect systems, that not only types, but also coefects are preserved by reduction.
As expected, to prove this property we need, as in proofs in the literature, assumptions on
operations derived from user-defined methods, corresponding to have a semiring (
Assumptions 1. For all user-defined coefects
v^1, v^2, v^3:
The proof of Theorem 1 uses the standard lemmas of inversion for expressions and contexts (Lemmas 1 and 2), and substitution in evaluation contexts and terms (Lemmas 3 and 4). Lemma 1 (Inversion).
1. If Γ ⊢ x : C , then Γ = (0× Γ′) + x :1 C for some Γ′. 2. If Γ ⊢ e.f : C , then we have Γ ⊢ e : C and fields(C ) = C1 f1; . . . C f; and C = C . 3. If Γ ⊢ new C (e1, . . . , e) : C , then we have fields(C ) = C1 f1; . . . C f;, Γ ⊢ e : C for all ∈ 1.. and Γ = Γ1 + . . . + Γ. 4. If Γ ⊢ e0.m(e1, . . . , e) : C , then we have Γ0 ⊢ e0 : C , mtype(C , m) = v^0, C1v^1 . . . Cv^ → C , c′ = v^ ∨ 1 for all ∈ 0.., Γ ⊢ e : C for all ∈ 1.. and Γ = (c0′ × Γ0) + (c1′ × Γ1) + . . . + (c′ × Γ). 5. If Γ ⊢ {C [v^] x = e; e′} : C ′, then we have ∅ ⊢ v^ : Coeffect and Γ = c′ × Δ′ + Γ′ where c′ = v^ ∨ 1, c ≤ v^ and Δ′ ⊢ e : C and Γ′, x :c C ′ ⊢ e′ : C ′.
Lemma 2 (Context Inversion). If Γ ⊢ ℰ [e] : C , then Γ′ +x :c C ′ ⊢ ℰ [x ] : C and Δ ⊢ e : C ′ for some Γ′, Δ, x ̸∈ dom(Γ), c and C ′ such that Γ = Γ′ + c × Δ.
Proof 1. By induction on ℰ .
Lemma 3 ( Context Substitution). If Δ ⊢ e : C ′ and Γ + x :c C ′ ⊢ ℰ [x ] : C , with x ∈/ dom(Γ), then Γ + c × Δ ⊢ ℰ [e] : C .
Proof 2. By induction on the derivation of Γ + x :v^ C ⊢ ℰ [x ] : C ′.
Lemma 4 (Substitution). If Δ ⊢ e′ : C ′ and Γ, x :c C ′ ⊢ e : then Γ + c × Δ ⊢ e[e′/x ] : C . Theorem 1. If Γ ⊢ e : C and e → e′, then Γ′ ⊢ e′ : C such that Γ ≤ Γ′.
Proof 3. By induction on the reduction relation. We show some significant cases.
(ctx) By Lemma 2 we have Γ′ + x :v^ C ′ ⊢ ℰ [x ] : C , Δ ⊢ e : C ′ and Γ = Γ′ + v^ × Δ. By
induction hypothesis we derive Δ ⊢ e′ : C ′. By Lemma 3 we derive Γ′ + v^ × Δ ⊢ ℰ [e′] : C ,
that is, Γ ⊢ ℰ [e′] : C .
(field-access) By Lemma 1(
We use as syntactic sugar case expressions with more than two alternatives, which can be easily encoded in the calculus. Moreover, variable declarations with no coefect annotation are assumed to have a new Coeffect() coefect. Some other simplifications in code are explained when used. Coefect annotations are emphasized in grey to help the reader.
Example 1. Linearity As first example we show how to implement the classical coefect system mentioned in the Introduction, which traces when a variable is either not used (coefect 0), or used linearly (that is, exactly once, coefect 1), or used in an unrestricted way (coefect ). Example 2. Using linearity coefects After declaring the above coefect classes, the programmer can use them in annotations, as in the simple example below, where they are used for the annotation of this, written between the method name and the list of parameters. class Pair { A fst; A snd; } class A {
A drop [new Zero()] () {new A()} A identity [new One()] () {this}
Pair duplicate [new Omega()] () { new Pair(this,this)}
}
Let us see some examples of how the type system works. To check that, e.g., the method
duplicate is well-typed, we have to typecheck the method body, and then verify the condition
(t-meth) at page 5. A type derivation for the method body is as follows:
this :2 A ⊢ new Pair(this, this) : Pair
Set = new Omega(). The condition (t-meth) requires this : A ≤ this :2 A, and this holds
since we can derive 2 ≤ from
• 2 ∨ = nf(in(
If the expression new Pair(this, this).fst was the body of method identity, instead,
then the method would be ill-typed. Indeed, we would have a similar derivation:
However, this :new One() A ≤ this :2 A does not hold, since 2 ≰ new One():
• 2 ∨ new One() = nf(innew One()(
nf((new One().zero().sum(new One().one())).sum(new One().one())) = • nf(.sup(new One())) = A call of duplicate can be typed as shown below:
Example 3. Product of coefects The following example shows that, besides single coefect classes, the programmer can also define general constructions. The class Product implements coefects which are the product of two arbitrary coefects. class Product extends Coeffect{ Coeffect left; Coeffect right;
Coeffect one(){new Product(left.one(),right.one())} Coeffect zero(){new Product(left.zero(),right.zero())} Coeffect sup(Coeffect c) { case c of (Product p) new Product(this.left.sup(p.left),this.right.sup(p.right)) (Coeffect x) new Coeffect() Coeffect sum(Coeffect c) { case c of (Product p) new Product(this.left.sum(p.left),this.right.sum(p.right)) (Coeffect x) new Coeffect() } Coeffect mult(Coeffect c) { case c of (Product p) new Product(this.left.mul(p.left),this.right.mul(p.right)) (Coeffect x) new Coeffect() Example 4. Sessions Finally, we show a more significant programming example, which also uses the coefect type Level, providing a way to specify the privacy level of data. In this case, the coefects form a three point lattice: Public, Private and Irrelevant with zero being Irrelevant, one being Private and order Irrelevant≤ Private≤ Public. Sum is the sup and product is defined by c1 × c2 =Irrelevant if either c1 =Irrelevant or c2 =Irrelevant, otherwise c1 × c2 = c1 ∨ c2. It is easy to write the Level classes which implement the previous definitions.
The example illustrates how binary sessions could be implemented using our coefect annotations. We take inspiration from the encoding of sessions into the -calculus with variants and linear I/O types of [10]. We assume to have the following classes implementing linear input and output channels over which we can send a message and, if needed, some private data. class OutPrivChannel{
Unit send [new One()] (Msg msg,OptData [new Private()] data,
InPrivChannel [new One()] cont) {...} } class InPrivChannel{
(Msg,OptData,OutPrivChannel) rcv [new One()] (OutPrivChannel [new One()] cont) {...} } class Unit{ } class OptData{ } class Some extends OptData{A inf;} class None extends OptData{ } class Msg { } class NextData extends Msg{ } class Stop extends Msg{ } class OK extends Msg{ } class KO extends Msg{ } The linearity of the channel is expressed by annotating the receiver of the send and receive methods with the One coefect of the Linearity coefects. The send method of the class OutPrivChannel takes as input, in addition to the message and the data to be sent, an input channel that will be used, by whoever is sending the message, to wait for the answer to the sent message. On the other side, the rcv method of class InPrivChannel returns a message, a data and an output channel3 that will be used, by whoever received the message, to continue the conversation. The 3To simplify the code we allow the method to return a triple here. message does not have a coefect as this is irrelevant.
The class Server that follows implements a server which waits for a message that can be either NextData or Stop. In the first case, the server sends to whoever sent the message the message OK, processes the data, and goes back to waiting for a message. In the second case, it stops returning OK (we use this message also to signal that the protocol ended successfully). If it receives any other message, the server stops returning KO, meaning failure of the exchange. class Server {
Msg main(InPrivChannel [new One()] c){ (Msg msg,OptData [new Private()] d,OutPrivChannel [new One()] c1)=c.rcv(); case msg of (NextData [new Zero()] y){
OutPrivChannel [new One()] outCh= new OutPrivChannel(); InPrivChannel [new One()] inCh= new InPrivChannel(); c1.send(msg,new None(),outCh) main(inCh) } (Stop [new Zero()] y) new OK() (Msg [new Zero()] y) new KO() } } Note that the server receives the initial message from the client on the channel which is the parameter of the method. After receiving the message the channel cannot be used any longer. A client of the previous server sends a data to the server and then, if the response of the server is OK, either sends a NextData or a Stop message. If the response is not OK the client returns KO, meaning failure of the exchange. class Client {
Msg main(OutPrivChannel [new One()] c){
OutPrivChannel [new One()] outCh=new OutPrivChannel(); InPrivChannel [new One()] inCh=new InPrivChannel(); c.send(new nextData(),new Some(new A()),outCh){ (Msg msg,Data [new Private()] d,OutPrivChannel [new One()] c1)=inCh.rcv(); case msg of (OK [new Zero()] y){c1.send(Stop,new None(),new InPrivChannel()); new OK()} (Msg [new Zero()] y) new KO() }
} The client above sends just one data, however clients could interact with the server sending more data. As for the server, the initial message of the client is sent on the channel which is the parameter of the method, and then a new pair of channels is generated and used for the successive interaction.
The computation of the server and the client is started by sending an output channel to the client and an input channel to the server. The fact that the channels are linear ensures that they will be used to realise the wanted binary session. Assuming to have a parallel composition operator, the server and the client can be started as follows.
OutPrivChannel [new One()] outCh = new OutPrivChannel(); InPrivChannel [new One()] inCh = new InPrivChannel();
new Client().main(outCh) | new Server().main(inCh)
We proposed a Java-like calculus supporting, in variable declarations, coefect annotations, allowing to express how such variables should be used. Thanks to the inheritance mechanism of OO languages, programmers are able to define their own coefect annotations. Indeed, they are expressions of (subclasses of) Coeffect, a predefined class which can be extended by user-defined subclasses, similarly to Java exceptions which are expressions of (subclasses of) Exception. We formally defined the type system and proved subject reduction, which includes preservation of coefects, and provided several examples.
There are many interesting directions for further work. The most natural development is adding graded modal types. Indeed, a limitation of the current proposal is that, whereas it is possible to specify how a variable should be used (e.g., a parameter should be used at most once in a method’s body), it is not possible to do the same for the result of an expression (e.g., the result of a method). Graded modal types, which are, roughly, types annotated with coefects (grades) [2, 6, 8], also similar to types annotated with modifiers or capabilities [11, 12, 13], would allow to overcome this limitation.
Coefects considered in this paper are structural, in the sense that they are expressed and computed on a per-variable basis. However, in some cases the coefect, expressing how an expression uses external resources, cannot be captured by just assigning independent scalar coefects to single variables, but should be assigned to the whole context [ 1]. In our work, this would correspond to allow a “global” annotation in a method’s signature.
Finally, expressive power could be added by allowing variables in coefect annotations, so to specify, e.g., that a variable should be used no more than a certain number computed at runtime. This approach would require first the study of dependent coefects on the foundational side, which, to the best of our knowledge, have not been developed yet.
On the more applicative side, we could investigate how the proposal scales to realistic subsets of Java. Implementations could use in a parametric way auxiliary tools, notably a termination checker to prevent divergence in methods implementing coefect operations, and/or a verifier to ensure that they provide the required properties (assumptions at page 6).
The authors thank the anonymous referees who provided useful and detailed comments. This work was partially funded by the MUR project “T-LADIES” (PRIN 2020TL3X8X).