We propose a Java-like calculus where declared variables can be annotated by coeffects 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 coeffects desired for a specific application. We formalize the type system and prove subject reduction, which includes preservation of coeffects, and show several examples.
Type-and-coeffect systems [1,2,3,4,5,6,7,8] are type systems where the typing judgment takes an enriched form, such as x 1 : c 1 C 1 , . . . , x π : cπ C π β’ e : C , with c 1 , . . . , c π coeffects modeling how the corresponding variables are used in e.
For instance, coeffects 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 coeffect annotations: πx :int[0].5, πx :int [1].x , and πx :int[π].x + x . Other typical examples are exact usage (coeffects are natural numbers), and privacy levels. Coeffects 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-coeffect system, hence allowing the programmer to write function declarations as those above. In Granule, different kinds of coeffects can be used at the same time, including naturals for exact usage, security levels, intervals, infinity, and products of coeffects; however, the available coeffects 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 coeffect annotations in variable declarations.
Moreover, we rely on the inheritance mechanism of OO languages to allow the programmer to write her/his own coeffects. More in detail, coeffect 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-coeffect 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 e 1 , . . . , 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 coeffect class. In addition to standard constructs (variable, field access, constructor and method invocation, and block) we include a typecase construct, since in coeffect 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 coeffect 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 coeffect class. The syntax of coeffect 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 coeffect annotation, and an expression. Expression e 1 is executed if the result of the initial expression has a subtype of C 1 , with x 1 bound to such result; otherwise, expression e 2 is executed, with x 2 bound to the result, provided that it has a subtype of C 2 . 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 coeffects c ::= n | v ^, with n β N, and v ^user-defined coeffect, that is, value expected to be of a coeffect class.
The typing judgment has shape Ξ β’ e : C , where Ξ is a (type-and-coeffect) context, that is, a (finite) map from variables to pairs of a coeffect and a type (class name), written Ξ = x 1 : c 1 C 1 , . . . , x π : cπ C π . Equivalently, Ξ can be seen as the pair of a coeffect context and a type context, maps from variables to coeffects and types, respectively, with the same domain.
As customary in type-and-coeffect systems, in typing rules contexts are combined by means of some operations, which are, in turn, defined in terms of the corresponding operations on coeffects. We first define the operations on contexts, then we show the typing rules, and finally we define how the assumed operations on coeffects are derived from user-defined methods in coeffect classes.
The operations on contexts are the following:
As the reader can note, operations on coeffect contexts are obtained by pointwise application of the corresponding operations on coeffects, and then they are lifted to type-and-coeffect 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 coeffects; however, to stress that they can be actually computed bottom-up, we prefer a presentation where overapproximation of coeffects 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), coeffects of the subterms are summed.
In rule (t-invk), the coeffects of the arguments are summed, after multiplying each of them with the sup (greatest lower bound) of the coeffect annotation of the corresponding parameter, and the one coeffect. The sup with the one coeffect guarantees to take into account the coeffects 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-coeffect 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 coeffect annotations. Such coeffect annotations should have a coeffect class as type.
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 coeffects which are (overapproximated by) those specified in the annotations. Formally, if mbody(C , m) = (x 1 . . . x π , e), and mtype
In rule (t-block), the coeffects of the initialization expression are multiplied by the sup of the coeffect annotation of the variable, and the one coeffect, and then summed with those of the body. Analogously to method invocation, the sup with the one coeffect 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 coeffect. In rule (t-case), coeffects are handled analogously as in rule (t-block). The first side-condition ensures that the cases are exhaustive.
We describe now how operations on coeffects are derived from user-defined methods in the coeffect classes. The predefined class Coeffect is defined as follows:
Being subclasses of Coeffect, coeffect classes implement the above methods, corresponding to the expected operations on coeffects: 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 coeffect classes always terminate, so that normal forms in the definitions below are defined.
Recall that coeffects are either natural numbers or user-defined coeffects (values of a coeffect class). Natural numbers are internally used2 by the type system, notably in rule (t-var) which is independent from coeffect classes in the program. As a consequence, operations on coeffects derived from user-defined methods need to handle natural numbers as well. This is achieved through a translation into user-defined coeffects, which corresponds to the unique homomorphism from the initial semiring to another one. That is, in v ^(n ) is the user-defined coeffect corresponding to n in the class of v ^, defined by:
We can now define operations on coeffects. To avoid confusion, standard operations on natural numbers have the explicit subscript N.
Note that the order β€ on coeffects can be derived from the β¨ operator, as follows:
We prefer to implement the sup operator, rather than the order, in coeffect 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-coeffect systems, that not only types, but also coeffects 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 (1-8) with an additional order-theoretic structure (9-15). Ensuring such properties is in charge of the programmer, possibily using some verification tool.
Assumptions 1. For all user-defined coeffects 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).
1. Proof 3. By induction on the reduction relation. We show some significant cases.
(ctx) By Lemma 2 we have
.π and Ξ = Ξ 1 + . . . + Ξ π . We know that π β 1...π, v ^π = e β² and Ξ π β’ e β² : C . By Assumptions (12) and (10) we know Ξ β€ Ξ π , so we have the thesis .
(block) By Lemma 1 (5) we have β’ v ^:
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 coeffect annotation are assumed to have a new Coeffect() coeffect. Some other simplifications in code are explained when used. Coeffect annotations are emphasized in grey to help the reader.
Example 1. Linearity As first example we show how to implement the classical coeffect system mentioned in the Introduction, which traces when a variable is either not used (coeffect 0), or used linearly (that is, exactly once, coeffect 1), or used in an unrestricted way (coeffect π). 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 : 1 A β’ this : A 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
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:
this : 1 A β’ this : A this : 2 A β’ new Pair(this, this) : Pair this : 2 A β’ new Pair(this, this).fst : A However, this : new One() A β€ this : 2 A does not hold, since 2 β° new 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:
(t-new) (t-var)
x : We can see that natural numbers are translated into user-defined linearity coeffects when coeffect operations occur in the derivation.
Finally, we show an example motivating that in rules (t-invk), (t-block), and (t-case) the sup with 1 is needed. For instance, in this way we can derive the judgment y : π A β’ {Pair[new Zero()] x = y.duplicate; new A()} : A.
The following example shows that, besides single coeffect classes, the programmer can also define general constructions. The class Product implements coeffects which are the product of two arbitrary coeffects. Example 4. Sessions Finally, we show a more significant programming example, which also uses the coeffect type Level, providing a way to specify the privacy level of data. In this case, the coeffects 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
It is easy to write the Level classes which implement the previous definitions.
The example illustrates how binary sessions could be implemented using our coeffect 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. The linearity of the channel is expressed by annotating the receiver of the send and receive methods with the One coeffect of the Linearity coeffects. 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
We proposed a Java-like calculus supporting, in variable declarations, coeffect 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 coeffect 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 coeffects, 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 coeffects (grades) [2,6,8], also similar to types annotated with modifiers or capabilities [11,12,13], would allow to overcome this limitation.
Coeffects 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 coeffect, expressing how an expression uses external resources, cannot be captured by just assigning independent scalar coeffects 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 coeffect 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 coeffects 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 coeffect 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).
message does not have a coeffect 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. 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. 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.