# Featherweight Java

Featherweight Java is a lightweight functional version of Java, which focuses on a few basic features. It is not intended to be used as a programming language, but as a formal framework for studying properties of Java (A. Igarashi, B. Pierce, and P.Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM TOPLAS, 23(3):396-450, 2001.). In this section we will see how to write the type system of FJ using Xsemantics. (As future work we will also define the operational semantics of FJ in Xsemantics.)

## FJ in a nutshell

FJ focuses on the following features: mutually recursive class definitions, inheritance, object creation, method invocation, method recursion through this, subtyping and field access. In particular, a FJ program is a list of class definitions and a single main expression. Here's an example of an FJ program:

class A extends Object { }
class B extends Object { }
class Pair extends Object {
Object fst;
Object snd;
Pair setfst(Object newfst) {
return new Pair(newfst, this.snd);
}
Pair setsnd(Object newscd) {
return new Pair(this.fst, newscd);
}
}
new Pair(new A(), new B()).setfst(new A()).fst

Since in FJ the class constructor has a fixed shape, we consider a simplified version of the language by assuming constructors as implicit; in particular when invoking new we should pass an argument for each field in the class, including inherited fields, in the same order of the hierarchy. Thus, if we have the following classes

class A { int i; boolean b; }
class B extends A { String s; }

we must create an instance of B2 as follows: new B(10, true, "foo").

## FJ implemented in Xtext

We had already implemented FJ in Xtext (that implementation can be found at http://fj-eclipse.sourceforge.net). In that implementation, the type system was implemented directly in Java. With Xsemantics we ship another implementation of FJ where the type system is written using Xsemantics instead of manually written Java code.

grammar org.eclipse.xsemantics.example.fj.FJ with org.eclipse.xtext.common.Terminals
generate fj "http://xsemantics.sf.net/example/fj/FJ"
Program :
(classes += Class)*
(main = Expression)? ;
Type: BasicType | ClassType;
BasicType : basic=('int' | 'boolean' | 'String');
ClassType : classref=[Class];
Class:
'class' name=ID ('extends' superclass=[Class])? '{'
(members += Member)*
'}' ;
Member: Field | Method;
Field: type=Type name=ID ';' ;
Method:
type=Type name=ID '(' (params+=Parameter (',' params+=Parameter)*)? ')' '{'
body=MethodBody
'}' ;
Parameter: type=Type name=ID ;
TypedElement: Member | Parameter;
MethodBody: 'return' expression=Expression ';' ;
Expression:
TerminalExpression
=>(
{Selection.receiver=current} '.'
message=[Member]
('(' (args+=Expression (',' args+=Expression)*)? ')')?
)* ;
TerminalExpression returns Expression:
This |
ParamRef |
New |
=>Cast |
Constant |
Paren ;
This: variable='this';
ParamRef: parameter=[Parameter];
New: 'new' type=ClassType '(' (args+=Expression (',' args+=Expression)*)? ')';
Cast: '(' type=ClassType ')' expression=TerminalExpression;
Paren returns Expression: '(' Expression ')';
Constant: IntConstant | BoolConstant | StringConstant;
StringConstant: constant=STRING;
IntConstant: constant=INT;
BoolConstant: constant = ('true' | 'false');

## FJ Type System

We start by defining the name (we skip imports), the auxiliary descriptions (which will be used for auxiliary functions, section Auxiliary) and the judgments (section Judgments); we also use an injected field (section Fields) of type FjTypeUtils which contains some auxiliary functions that we will use in the rules.

system org.eclipse.xsemantics.example.fj.typing.FjTypeSystem
inject FjTypeUtils fjTypeUtils
auxiliary {
superclasses(Class cl) : List<Class>
fields(Class cl) : List<Field>
methods(Class cl) : List<Method>
overrides(Method current, Method previous)
error current.name + " does not override the superclass method"
source current
isValue(Expression e) : Boolean
/* replaces in a copy of the body's expression:
* 'this' with thisReplacement and
* param references with args */
replaceThisAndParams(MethodBody body,
Expression thisReplacement,
List<Parameter> params, List<Expression> args
) : MethodBody
}
judgments {
type |- Expression expression : output Type
error "cannot type " + stringRep(expression)
source expression
classtype |~ Expression expression : output ClassType
error stringRep(expression) + " has not a class type"
source expression
subtype |- Type left <: Type right
error stringRep(left) + " is not a subtype of " + stringRep(right)
assignable |- Expression expression |> Type target
error stringRep(expression) + " is not assignable for " + stringRep(target)
source expression
equalstype |- Type left ~~ Type right
error stringRep(left) + " is not the same type as " + stringRep(right)
subtypesequence |-
Expression owner ~>
List<Expression> expressions << List<? extends TypedElement> elements
error "invalid arguments for expected parameters"
source owner
}

In the following we explain the rules of these judgments. Note that auxiliary functions corresponding to the above defined auxiliary descriptions must be defined before implementing the rules. However, in this document, we will concentrate on the implementations of the rules, and show the auxiliary functions when they are used by the rules.

### Typing FJ Expressions

Let's start with simple expressions

axiom TParamRef
G |- ParamRef paramref : paramref.parameter.type
// you can manually create the BasicType with EMF FjFactory...
axiom TStringConstant
G |- StringConstant s : {
val result = FjFactory::eINSTANCE.createBasicType();
result.basic = 'String'
result
}
// ...or use an utility class...
axiom TIntConstant
G |- IntConstant i : fjTypeUtils.createIntType
// ...or closures
axiom TBoolConstant
G |- BoolConstant b :
[
BasicType t |
t.basic='boolean'
t
].apply(FjFactory::eINSTANCE.createBasicType())

The type of a parameter reference is simply the type of the referred parameter (since Parameter is an element with an explicit type).

Just to show the syntax of rules in Xsemantics which rely on Xbase, we present above three different ways of creating the basic types (initialized with the corresponding string). This is just a demonstration: probably, the best way is relying on static utility methods implemented for your DSL (as we did with FjTypeUtils). Alternatively, as we did with the Expressions example (see section Expressions), we could have a different class for each basic type.

rule TNew
G |- New newExp : newExp.type
from {
var fields = fields(newExp.type.classref)
// we want the superclasses' fields first
G |- newExp ~> newExp.args << fields
}

The type of a New expression is the classtype mentioned in the expression itself (e.g., the type of the expression new C() is C). However, we must also check that the expression is well-typed, i.e., that all the arguments passed to the new expression are subtypes of the corresponding fields of the classtype (see section FJInANutshell for the syntax of constructors in our implementation of FJ). In order to collect all the fields of the given class (including the inherited ones), we use the auxiliary function fields (which, in turns, rely on the auxiliary function superclasses):

auxiliary superclasses(Class cl) {
getAll(cl,
FjPackage::eINSTANCE.class_Superclass,
FjPackage::eINSTANCE.class_Superclass,
typeof(Class)
)
}
auxiliary fields(Class clazz) {
var Iterable<Field> fields = new ArrayList<Field>
// inherited fields must come first
for (superclass : superclasses(clazz)) {
fields =
(EcoreUtil2::typeSelect(superclass.members, typeof(Field))
+ fields)
}
fields = fields + EcoreUtil2::typeSelect(clazz.members, typeof(Field))
Lists::newArrayList(fields)
}

Note that, in order to get all the superclasses of a class we use getAll, section GetAll (Remember that using getAll avoids infinite loops in cases of cycles in the AST).

Now that we have all the fields, we can check that the types of the arguments are subtypes of the types of these fields (we use the judgment subtypesequence, described in section FJSubTyping).

rule TCast
G |- Cast cast : cast.type
from {
G |- cast.expression : var Type expType
G |- cast.type <: expType
or
G |- expType <: cast.type
}

A cast expression, statically, is well-typed if the type of the object and the type we cast to are related, and has the type of the type we cast to.

rule TSelection
G |- Selection selection : selection.message.type
from {
G |- selection.receiver : var ClassType receiverType
// check message if it's a method call
val message = selection.message
switch (message) {
Method: {
G |- selection ~> selection.args << message.params
}
}
}

The type of the selection is the type of the selected Message (which refers to a Member). However, we must check that the received of the message is well-typed, and in particular that it has a class type (since message selection, i.e., field access or method invocation, is allowed only on class instances). We perform this check by using as the output argument a ClassType (thus, that rule invocation would fail if the receiver had a basic type).

Furthermore, if the message refers to a Method, we must check that the arguments types are subtypes of the method parameters (we use the judgment subtypesequence, described in section FJSubTyping).

axiom TThis
G |- This _this : env(G, 'this', ClassType)

For the type of this we use the predefined function env (see section Environment) which returns the value contained in the environment (first parameter of env) which corresponds to the passed key ('this' in this case), provided the mapped value is a ClassType. The function env fails (and thus makes the rule fail) if no mapping for the specified key is found in the environment. Who puts the mapping for 'this' in the environment? We'll see that later (section FJScoping and section FJValidation). However, we assume that if this rule fails it is because we are trying to type this from outside a method body (e.g., in the program's main expression).

### FJ Scoping

We use the generated system from the rules defined in Xsemantics in the scope provider, in particular for the scope of the members in a Selection expression: we need the type of the receiver to know which members are visible in that selection expression:

public class FJScopeProvider extends AbstractDeclarativeScopeProvider {
@Inject FjTypeSystem typeSystem;
@Inject FjTypeUtils fjTypeUtils;
public IScope scope_Member(Selection sel, EReference ref) {
return Scopes
.scopeFor(getMembers(getExpressionClass(sel.getReceiver())));
}
protected Class getExpressionClass(Expression receiver) {
ClassType classType = typeSystem.classtype(
environmentForExpression(receiver), receiver).getValue();
return (classType != null ? classType.getClassref() : null);
}
private RuleEnvironment environmentForExpression(Expression expression) {
Class containingClass = EcoreUtil2.getContainerOfType(expression,
Class.class);
if (containingClass != null) {
ClassType thisType = fjTypeUtils.createClassType(containingClass);
return new RuleEnvironment(typeSystem.environmentEntry("this",
thisType));
}
return null;
}
public List<Member> getMembers(Class cl) {
List<Member> allMembers = new LinkedList<Member>();
try {
allMembers.addAll(typeSystem.fields(cl));
allMembers.addAll(typeSystem.methods(cl));
} catch (RuleFailedException e) {
// the list will be empty
}
return allMembers;
}
}

In order to get the type of the receiver expression we use the generated system (refer to section GeneratedSystem). However, we need to provide a binding for this in the environment (see section FJTyping), thus we build a RuleEnvironment (see also section Environment) where we associate the string "this" to the class which contains the current selection expression.

We also use the generated methods corresponding to the auxiliary functions fields and methods.

Note that we do not use the type judgment, but the judgment classtype (refer to section FJTypeSystem) which already returns a ClassType as the output parameter. This judgment has only one simple rule which relies on the type judgment, but using as the output argument a ClassType:

rule TExpressionClassType
G |~ Expression expression : ClassType classType
from {
G |- expression : classType
}

Once we have the class type of the receiver, we simply use an auxiliary function to collect all the members of that class.

### FJ Subtyping

We have a judgment subtype which given a left and right arguments succeeds if the former is a subtype of the latter. Here are the rules for this judgment:

rule GeneralSubtyping
G |- Type left <: Type right
error "types " + stringRep(left) + " and " + stringRep(right) +
" are not comparable"
from {
// if we get here we're trying to mix
// a BasicType with a ClassType, thus, we fail
fail
}
rule BasicSubtyping
derives G |- BasicType left <: BasicType right
from {
left.basic.equals(right.basic)
}
rule ClassSubtyping
derives G |- ClassType left <: ClassType right
from {
left.classref == right.classref
or
right.classref.name == "Object"
or
superclasses(left.classref).contains(right.classref)
}

The general case always fails, since we cannot mix basic and class types. Then for basic types we do not have actual subtyping, thus the two basic types must be the same. For class types we have three possible cases:

1. the two classes are the same (class subtyping is reflexive)
2. the right class is Object (every class is implicitly subclass of Object)
3. The right class is a parent of the left class (class subtyping is transitive); in order to check this last case, we get all the superclasses (using the superclasses auxiliary function shown before), and use the standard Java List contains method

Remember that, since ClassType has a reference to an actual Class object, it is safe to use object identities.

We also have a assignable judgment which tells whether an Expression is assignable to a type, by getting the type of of the expression and then checking the subtyping:

rule ExpressionAssignableToType
G |- Expression expression |> Type target
from {
var Type expressionType
G |- expression : expressionType
G |- expressionType <: target
}

Since in the typing rules for expressions (see section FJTyping) we have to check whether arguments are subtypes of parameters (in the New and Selection rules) we isolate a specific judgment subtypesequence, that we recall here

judgments {
// ...
subtypesequence |-
Expression owner ~>
List<Expression> expressions << List<? extends TypedElement> elements
error "invalid arguments for expected parameters"
source owner
}

whose (single rule) is implemented as follows:

rule SubtypeSequence derives
G |- Expression owner ~>
List<Expression> expressions << List<TypedElement> typedElements
from {
expressions.size == typedElements.size
or
fail
error "expected " + typedElements.size + " arguments, but got " +
expressions.size
source owner
val typedElementsIterator = typedElements.iterator
for (exp : expressions) {
G |- exp |> typedElementsIterator.next.type
}
}

First of all, the sizes of the two collections must be the same; if this first check fails we explicitly fail (see section ExplicitFailure) with an informative error; in order to make the error really informative and, most of all, to make the error marker generation effective (see section ErrorGeneration), we need the "owner" of this check, i.e., the expression context where this check has to be carried out, in order to specify that expression as the source of the error (section ErrorSpecification). Compare this with the way this judgment is used in the typing of New and Selection (section FJTyping). If this first check succeeds, we check that every expression is a subtype of the corresponding type; in order to do this we rely on assignable statement, described before.

We also have the judgment equalstype for type equality, similar to subtype, which will be used in check rules for validation (section FJValidation):

rule GeneralEquals
G |- Type left ~~ Type right
error "types " + stringRep(left) + " and " + stringRep(right) +
" are not comparable"
from {
// if we get here we're trying to mix
// a BasicType with a ClassType, thus, we fail
fail
}
rule BasicEquals
derives G |- BasicType left ~~ BasicType right
from {
left.basic.equals(right.basic)
}
rule ClassEquals
derives G |- ClassType left ~~ ClassType right
from {
left.classref == right.classref
}

## FJ Validation

We define some checkrules (section CheckRules) for validating an FJ program.

checkrule CheckMethodBody for
Method method
from {
val typeForThis = FjTypeUtils::createClassType(
EcoreUtil2::getContainerOfType(method, typeof(Class))
)
'this' <- typeForThis |- method.body.expression |> method.type
}

This rule checks that the return expression of a method body is a subtype of the declared method's type. It relies on the judgment assignable seen in section FJSubTyping. However, since this will involve being able to type possible occurrences of this we must also pass an explicit envrionment (section Environment) with a mapping for 'this' (mapped to the class type of the class containing the method). This is similar to what we do for FJ scoping (section FJScoping).

checkrule CheckField for
Field field
from {
val clazz = field.eContainer as Class
if (clazz.superclass != null) {
var inheritedFields = fields(clazz.superclass)
// make sure no duplicate fields in the hierarchy
inheritedFields.forEach [
inheritedField |
if (field.name == inheritedField.name) {
fail
error "field already defined in superclass " +
stringRep(inheritedField.eContainer)
}
]
}
}

For a Field we must check that a field with the same name is not defined in the superclasses (for fields with the same name in the same class this check is already done by Xtext predefined NamesAreUniqueValidator (src)). Again, we rely on the auxiliary function fields.

For methods we cannot execute the same check, since subclasses are allowed to redefine methods, provided they keep the same signature (in FJ covariance of return type is not allowed); thus we defined an auxiliary function, overrides, defined as follows:

auxiliary overrides(Method current, Method previous) {
current.name != previous.name
or
{
empty |- current.type ~~ previous.type
or
fail error
"cannot change return type of inherited method: " +
stringRep(previous.type)
source current
feature FjPackage::eINSTANCE.typedElement_Type
current.params.size == previous.params.size
val previousParamsIt = previous.params.iterator
for (param : current.params) {
empty |- param.type ~~ previousParamsIt.next.type
}
}
}

Which basically says that a method correctly overrides another one if their names are different (no actual overriding to check) or if they have exactly the same signature (relying on judgment equalstype).

Thus, the checkrule for Method is

checkrule CheckMethodOverride for
Method method
from {
val clazz = method.eContainer as Class
if (clazz.superclass != null) {
var inheritedMethods = methods(clazz.superclass)
val methods = EcoreUtil2::typeSelect(clazz.members, typeof(Method))
// check override predicate
inheritedMethods.forEach [
inheritedMethod |
methods.forEach [
overrides(it, inheritedMethod)
]
]
}
}

Note the use of Xbase closure (please refer to section ExpressionsInPremises for the way Xsemantics interprets boolean expressions inside premises and closures).

For a Class we need to check that its superclass hierarchy is not cyclic:

checkrule CheckClassHierachyNotCyclic for
Class cl
from {
if (cl.superclass != null) {
!superclasses(cl).contains(cl)
or
fail
error "Cyclic hierarchy for " + cl.name
source cl
}
}

which basically checks that the current class is not in the superclasses of itself.

Finally, we check that we can give a type to the main expression of an FJ program, in the empty environment:

checkrule CheckMain for
Program program
from {
program.main == null // nothing to check
or
empty |- program.main : var Type mainType
}

## FJ Operational Semantics

The operational semantics, i.e., reduction rules, are implemented, but documentation for this part has to be written yet.