=Paper=
{{Paper
|id=Vol-3284/8563
|storemode=property
|title=A Java-Like Calculus with User-Defined Coeffects
|pdfUrl=https://ceur-ws.org/Vol-3284/8563.pdf
|volume=Vol-3284
|authors=Riccardo Bianchini,Francesco Dagnino,Paola Giannini,Elena Zucca
|dblpUrl=https://dblp.org/rec/conf/ictcs/BianchiniDGZ22
}}
==A Java-Like Calculus with User-Defined Coeffects==
https://ceur-ws.org/Vol-3284/8563.pdf
A Java-like Calculus with User-Defined Coeffects
Riccardo Bianchini1,* , Francesco Dagnino1 , Paola Giannini2 and Elena Zucca1
1
University of Genova, Italy
2
University of Piemonte Orientale, Italy
Abstract
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.
Keywords
type systems, operational semantics, Java-like languages
1. Introduction
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 x1 :c1 C1 , . . . , xπ :cπ Cπ β’ e : C , with c1 , . . . , 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 lan-
guages, by allowing the programmer to write coeffect annotations in variable declarations.
Proceedings of the 23rd Italian Conference on Theoretical Computer Science, Rome, Italy, September 7-9, 2022
*
Corresponding author.
" riccardo.bianchini@edu.unige.it (R. Bianchini); francesco.dagnino@dibris.unige.it (F. Dagnino);
paola.giannini@uniupo.it (P. Giannini); elena.zucca@unige.it (E. Zucca)
0000-0003-0491-7652 (R. Bianchini); 0000-0003-3599-3535 (F. Dagnino); 0000-0003-2239-9529 (P. Giannini);
0000-0002-6833-6470 (E. Zucca)
Β© 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
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.
2. Calculus
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 coeffect class.
e ::= x | e .f | new C (es ) | e .m (es ) | {C [v^ ] x = e ; e β² } expression
| case e of (C1 [v^ 1 ] x1 )e1 (C2 [v^ 2 ] x2 )e2
v ::= new C (vs ) value
β° ::= [ ] | β° .f | new C (vs, β°, es ) | β° .m (es ) | v .m (vs, β°, es ) evaluation context
| {C [v^ ] x = β° ; e} | case β° of (C1 [v^ 1 ] x1 )e1 (C2 [v^ 2 ] x2 )e2
e β eβ²
(ctx)
β°[e] β β°[e β² ]
fields(C ) = C1 f1 ; . . . Cπ fπ ;
(field-access)
new C (v1 , . . . , vπ ).fπ β vπ π β 1..π
mbody(C , m) = (x1 . . . xπ , e)
(invk) β²
new C (vs ).m (v1 , . . . , vπ ) β e β² e = e[new C (vs )/this][v1 /x1 ] . . . [vπ /xπ ]
(block)
{C [v^ ] x = v ; e} β e[v /x ]
(case-1) C β€ C1
^ 1 ] x1 )e1 (C2 [v^ 2 ] x2 )e2 β e1 [new C (vs )/x1 ]
case new C (vs ) of (C1 [v
C ΜΈβ€ C1
(case-2)
^ 1 ] x1 )e1 (C2 [v^ 2 ] x2 )e2 β e2 [new C (vs )/x2 ] C β€ C2
case new C (vs ) of (C1 [v
Figure 1: Calculus
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
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.
3. Type System
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
Ξ = x1 :c1 C1 , . . . , 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:
Sup β
β¨Ξ=Ξ
(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 Ξ β€ Ξ
Sum β
+Ξ = Ξ (x :c C , Ξ)+Ξ = x :c C , (Ξ+Ξ) if x β
/ dom(Ξ)
(x :c C , Ξ)+(x :c β² C , Ξ) = x :c+c β² C , (Ξ+Ξ)
1
Coeffect annotations could be generalized to be arbitrary expressions; here we use this simpler assumption to make
the presentation lighter.
Ξ β’ e : Cβ²
(t-sub) Cβ² β€ C (t-var)
Ξβ’e:C (0ΓΞ) + x :1 C β’ x : C
Ξ β’ e : C fields(C ) = C1 f1 ; . . . Cπ fπ ;
(t-field-access)
Ξ β’ e .fπ : Cπ π β 1..π
Ξπ β’ eπ : Cπ βπ β 1..π
(t-new) fields(C ) = C1 f1 ; . . . Cπ fπ ;
Ξ1 + . . . +Ξπ β’ new C (e1 , . . . , eπ ) : C
Ξ0 β’ e0 : C Ξπ β’ eπ : Cπ βπ β 1..π mtype(C , m) = v^ 0 , C1v^1 . . . Cπv^π β C
(t-invk)
(c0β² ΓΞ0 )+ . . . +(cπβ² ΓΞπ ) β’ e0 .m(e1 , . . . , eπ ) : C cπβ² = v^ π β¨1 βπ β 0..π
β
β’ v^ : Coeffect
Ξβ’e:C Ξβ² , x :c C β’ e β² : C β² c β€ v^
(t-block)
(c ΓΞ)+Ξ β’ {C [v^ ] x = e ; e β² } : C β² c β² = v^ β¨1
β² β²
β
β’ v^ π : Coeffect βπ β 1..2
Ξβ’e:C
Ξπ , x :cπ Cπ β’ eπ : C β² βπ β 1..2 C ΜΈβ€ C1 implies C β€ C2
(t-case) cπ β€ v^ π βπ β 1..2
(c1β² β¨c2β² )ΓΞ+(Ξ1 β¨ Ξ2 ) β’ case e of (C1 [v^ 1 ] x1 )e1 (C2 [v^ 2 ] x2 )e2 : C β² β²
cπ = v^ π β¨1 βπ β 1..2
Figure 2: Coeffect system with user defined coeffects
Scalar multiplication cΓβ
= β
cΓ(x :c β² C , Ξ) = x :cΓc β² C , (cΓΞ)
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. Formally, if mtype(C , m) = v^ 0 , C1v^1 . . . Cπv^π β 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 coeffects 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 . . . Cπv^π β 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 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:
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, 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 homomor-
phism from the initial semiring to another one. That is, inv^ (n) is the user-defined coeffect
corresponding to n in the class of v^ , defined by:
inv^ (0) = nf(v
^ .zero()) inv^ (1) = nf(v
^ .one())
v^ v
^
in (n + 1) = nf(in (n).sum(v ^ .one())) for n β₯ 1
We can now define operations on coeffects. To avoid confusion, standard operations on
natural numbers have the explicit subscript N.
2
Derivations in Example 2 illustrate their interplay with user-defined coeffects.
v^ β¨n = nf(v^ .sup(inv^ (n))) nβ¨v^ = nf(inv^ (n).sup(v^ ))
Sup
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^ ))
Sum
v^ 1 + v^ 2 = nf(v^ 1 .sum(v^ 2 )) n1 + n2 = n1 +N n2
v^ Γ n = nf(v^ .mul(inv^ (n))) n Γ v^ = nf(inv^ (n).mul(v^ ))
Multiplication
v^ 1 Γ v^ 2 = nf(v^ 1 .mul(v^ 2 )) n1 Γ n2 = n1 ΓN n2
Note that the order β€ on coeffects can be derived from the β¨ operator, as follows: c1 β€ c2 iff
c1 β¨c2 = c2 . 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 :
1. v^ 1 + v^ 2 = v^ 2 + v^ 1 9. v^ 1 β¨ v^ 1 = v^ 1
2. v^ 1 + (v^ 2 + v^ 3 ) = (v^ 1 + v^ 2 ) + v^ 3 10. v^ 1 β¨ (v^ 2 β¨ v^ 3 ) = (v^ 1 β¨ v^ 2 ) β¨ v^ 3
3. v^ 1 + 0 = v^ 1 11. v^ 1 β¨ v^ 2 = v^ 2 β¨ v^ 1
4. v^ 1 Γ 1 = 1 Γ v^ 1 = v^ 1 12. v^ 1 β¨ (v^ 1 + v^ 2 ) = (v^ 1 + v^ 2 )
5. v^ 1 Γ 0 = 0 Γ v^ 1 = 0 13. v^ 1 + (v^ 2 β¨ v^ 3 ) = (v^ 1 + v^ 2 ) β¨
6. v^ 1 Γ (v^ 2 Γ v^ 3 ) = (v^ 1 Γ v^ 2 ) Γ v^ 3 (v^ 1 + v^ 3 )
7. v^ 1 Γ(v^ 2 +v^ 3 ) = v^ 1 Γv^ 2 +v^ 1 Γv^ 3 14. v^ 1 Γ (v^ 2 β¨ v^ 3 ) = (v^ 1 Γ v^ 2 ) β¨
8. (v^ 1 +v^ 2 )Γv^ 3 = v^ 1 Γv^ 3 +v^ 2 Γv^ 3 (v^ 1 Γ v^ 3 )
15. (v^ 2 β¨ v^ 3 ) Γ v^ 1 = (v^ 2 Γ v^ 1 ) β¨
(v^ 3 Γ v^ 1 )
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 . . . Cπv^π β 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 β² .
6. If Ξ β’ case e of (C1 [v^ 1 ] x1 )e1 (C2 [v^ 2 ] x2 )e2 : C then we have Ξ = (c1β² β¨c2β² )ΓΞβ² +(Ξ1 β¨
Ξ2 ), β
β’ v^ π : Coeffect for π β 1..2, Ξβ² β’ e : C , Ξπ , x :cπ Cπ β’ eπ : C β² for π β 1..2,
C ΜΈβ€ C1 implies C β€ C2 , cπ β€ v^ π for π β 1..2 and cπβ² = v^ π β¨1 for π β 1..2.
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(2) we have Ξ β’ new C (v1 , . . . , vπ ) : C and fields(C ) =
C1 f1 ; . . . Cπ fπ ; with Cπ = C . By Lemma 1(3) we have fields(C ) = C1 f1 ; . . . Cπ fπ ;,
Ξπ β’ v^ π : Cπ for all π β 1..π 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 ^ : Coeffect, Ξ = Ξβ² + c β² Γ Ξβ² where c β² = v^ β¨ 1, c β€ v^ ,
Ξβ² β’ e : C and Ξβ² , x :c C β² β’ e β² : C β² . Applying Lemma 4 we derive Ξβ² + c β² Γ Ξβ² β’
e2 [e1 /x ] : C β² . Applying Assumption (14) we derive the thesis.
4. Examples
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 π).
class Linearity extends Coeffect{ class One extends Linearity{
Coeffect zero(){ new Zero()} Coeffect sup(Coeffect c) {
Coeffect one(){new One()} case c of
} (One x) new One()
(Linearity x) new Omega()
class Zero extends Linearity{ (Coeffect x) new Coeffect()}
Coeffect sup(Coeffect c) { }
case c of Coeffect sum(Coeffect c) {
(Zero x) x case c of
(Linearity x) new Omega() (Zero x) new One()
(Coeffect x) new Coeffect() (Linearity x) new Omega()
} (Coeffect x) new Coeffect()
} }
Coeffect sum(Coeffect c) { Coeffect mult(Coeffect c) {
case c of case c of
(Linearity x) x (Linearity x) x
(Coeffect x) new Coeffect() (Coeffect x) new Coeffect()
} }
Coeffect mult(Coeffect c) { }
case c of
(Linearity x) new Zero()
(Coeffect x) new Coeffect()
}
}
class Omega extends Linearity{ Coeffect mult(Coeffect c) {
Coeffect sup(Coeffect c) { case c of
case c of (Zero x) new Zero()
(Linearity x) new Omega() (Linearity x) new Omega()
(Coeffect x) new Coeffect() (Coeffect x) new Coeffect()
} }
Coeffect sum(Coeffect c) { }
case c of
(Linearity x) new Omega()
(Coeffect x) new Coeffect()
}
Example 2. Using linearity coeffects After declaring the above coeffect classes, the pro-
grammer 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:
(t-var) (t-var)
this :1 A β’ this : A this :1 A β’ this : A
(t-new)
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π (2).sup(π ))
β’ inπ (2) = nf((π .zero().sum(π .one())).sum(π .one())) = π
β’ nf(π .sup(π )) = π
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:
(t-var) (t-var)
this :1 A β’ this : A this :1 A β’ this : A
(t-new)
this :2 A β’ new Pair(this, this) : Pair
(t-field-access)
this :2 A β’ new Pair(this, this).fst : A
However, this :new One() A β€ this :2 A does not hold, since 2 β° new One():
β’ 2 β¨ new One() = nf(innew One() (2).sup(new One()))
β’ innew One() (2) =
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-var) (t-var)
x :1 A β’ x : A y :1 A β’ y : A
(t-new)
x :1 A, y :1 A β’ new Pair(x , y ) : Pair
(t-field-access)
x :1 A, y :1 A β’ new Pair(x , y ).fst : A
(t-invk)
x :π A, y :π A β’ new Pair(x , y ).fst.duplicate() : Pair
where mtype(A, dup) = π, π β Pair, π = π β¨ 1, and π = π Γ 1.
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.
Example 3. Product of coeffects 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.
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 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 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 coeffect anno-
tations. 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 meth-
ods 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
3
To simplify the code we allow the method to return a triple here.
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.
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)
5. Conclusion
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).
Acknowledgments
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).
References
[1] T. Petricek, D. A. Orchard, A. Mycroft, Coeffects: a calculus of context-dependent com-
putation, in: J. Jeuring, M. M. T. Chakravarty (Eds.), ACM International Conference
on Functional Programming, ICFP 2014, ACM Press, 2014, pp. 123β135. doi:10.1145/
2628136.2628160.
[2] A. Brunel, M. Gaboardi, D. Mazza, S. Zdancewic, A core quantitative coeffect calcu-
lus, in: Z. Shao (Ed.), European Symposium on Programming, ESOP 2013, volume
8410 of Lecture Notes in Computer Science, Springer, 2014, pp. 351β370. doi:10.1007/
978-3-642-54833-8\_19.
[3] R. Atkey, Syntax and semantics of quantitative type theory, in: A. Dawar, E. GrΓ€del (Eds.),
IEEE Symposium on Logic in Computer Science, LICS 2018, ACM Press, 2018, pp. 56β65.
doi:10.1145/3209108.3209189.
[4] M. Gaboardi, S. Katsumata, D. A. Orchard, F. Breuvart, T. Uustalu, Combining effects
and coeffects via grading, in: J. Garrigue, G. Keller, E. Sumii (Eds.), ACM International
Conference on Functional Programming, ICFP 2016, ACM Press, 2016, pp. 476β489. doi:10.
1145/2951913.2951939.
[5] D. R. Ghica, A. I. Smith, Bounded linear types in a resource semiring, in: Z. Shao
(Ed.), European Symposium on Programming, ESOP 2013, volume 8410 of Lecture Notes in
Computer Science, Springer, 2014, pp. 331β350. doi:10.1007/978-3-642-54833-8\_18.
[6] D. Orchard, V. Liepelt, H. E. III, Quantitative program reasoning with graded modal types,
Proceedings of ACM on Programming Languages 3 (2019) 110:1β110:30. doi:10.1145/
3341714.
[7] P. Choudhury, H. E. III, R. A. Eisenberg, S. Weirich, A graded dependent type system with
a usage-aware semantics, Proceedings of ACM on Programming Languages 5 (2021) 1β32.
doi:10.1145/3434331.
[8] U. Dal Lago, F. Gavazzo, A relational theory of effects and coeffects, Proceedings of ACM
on Programming Languages 6 (2022) 1β28. doi:10.1145/3498692.
[9] A. Igarashi, H. Nagira, Union types for object-oriented programming, J. Object Technol. 6
(2007) 47β68. doi:10.5381/jot.2007.6.2.a3.
[10] O. Dardha, E. Giachino, D. Sangiorgi, Session types revisited, in: D. D. Schreye, G. Janssens,
A. King (Eds.), PPDPβ12, ACM, 2012, pp. 139β150. doi:10.1145/2370776.2370794.
[11] P. Haller, M. Odersky, Capabilities for uniqueness and borrowing, in: T. DβHondt (Ed.),
European Conference on Object-Oriented Programming, ECOOP 2010, volume 6183 of
Lecture Notes in Computer Science, Springer, 2010, pp. 354β378.
[12] C. S. Gordon, M. J. Parkinson, J. Parsons, A. Bromfield, J. Duffy, Uniqueness and reference
immutability for safe parallelism, in: G. T. Leavens, M. B. Dwyer (Eds.), ACM Symp. on
Object-Oriented Programming: Systems, Languages and Applications 2012, ACM Press,
2012, pp. 21β40.
[13] C. S. Gordon, Designing with static capabilities and effects: Use, mention, and invariants
(pearl), in: R. Hirschfeld, T. Pape (Eds.), European Conference on Object-Oriented Pro-
gramming, ECOOP 2020, volume 166 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fΓΌr
Informatik, 2020, pp. 10:1β10:25. doi:10.4230/LIPIcs.ECOOP.2020.10.