Choral is an object-oriented language with statically-typed high-level abstractions for the programming of choreographies (multiparty protocols).
In Choral, choreographies are objects (and objects are choreographies). Choral objects have types of the form T@(R1, ..., Rn)
, where T
is the usual interface of the object, and R1, ... , Rn
are the roles that collaboratively implement the object.
The state and behaviour of an object can be distributed over the roles of its type, which is the key feature that allows us to express choreographies.
Values in Choral must be located at roles as well.
For example, the literal "Hello"@A
is a string value "Hello"
located at role A
. All existing Java types can be used in Choral as types that live at a single world (like the string "Hello"
here).
Code involving different roles can be freely mixed in Choral, as in the following snippet.
class HelloRoles@(A, B) {
public static void sayHello() {
String@A a = "Hello from A"@A;
String@B b = "Hello from B"@B;
System@A.out.println(a);
System@B.out.println(b);
}
}
Try it yourself: see the source code on .
The code above defines a class, HelloRoles
, parameterised over two roles, A
and B
.
Its method sayHello
defines a variable a
of type “String at A” (String@A
) to which we assign the value "Hello from A"
located at A
("Hello from A"@A
).
Similarly, we define and assign a value to a variable b
as a string located at B
.
In the last two lines of the method, we print variable a
by using the System
object at A
(System@A
), and then we print variable b
at role B
.
Roles are part of data types in Choral, adding a new dimension to typing. For example, the statement String@A a = "Hello from B"@B
would be ill-typed, because the expression on the right returns data at a different role from that expected by the left-hand side.
Given the class HelloRoles
, the Choral compiler generates for each role a Java class with the behaviour for that role, in compliance with the source Choral class.
Assuming we saved the Choral program above in a file called HelloRoles.ch
, we can launch the Choral compiler with the command choral epp HelloRoles.
We will obtain two Java classes: the Java class for role A
is HelloRoles_A
and the class for B
is HelloRoles_B
.
class HelloRoles_A {
public static void sayHello() {
String a = "Hello from A";
System.out.println( a );
}
}
class HelloRoles_B {
public static void sayHello() {
String b = "Hello from B";
System.out.println( b );
}
}
Each generated class contains only the instructions that pertain to that role.
If Java developers want to implement the behaviour of method sayHello
for a specific role of the HelloRoles
choreography, say A
, they just need to invoke the generated sayHello
method in the respective generated class (HelloRoles_A
).
Using the @
symbol in types comes from the tradition in hybrid logic, where @
is used to express the “world” at which a statement is valid. Similarly, in Choral, @
expresses the roles at which a data type lives.
You can still use the @
symbol to write also common Java-like annotations in other places, like in Java.