Droid2Core

This is the core language of Droid, the one the normal syntax get expanded to during parsing.

Some parts of the full language are actually kept in their original version in the current implementation, because some features are easier to implement that way. There is no problem with expressing them in the core language though.

Placeholders

In order to talk about the syntax in general, we define some placeholders. Everything else is actual syntax. Don't memorize these, just use it as a fallback if they're not clear from the context.

Uppercase versions of these are collections of zero or more. For example, E1 is a collection of zero or more expressions (comma-separated in the concrete syntax).

When I say "the type t1" or "the value e1" I really mean the result of evaluating these expressions. When I say "the type of e1" I mean the type of the result of evaluating these expressions.

Method Calls

e1.m1(E2)

Primitive feature, the combination of looking up the method named m1 in the object which is the result of evaluating e1 and applying it to the arguments E2, each of which is evaluated before the application (call by value). It has the type bound to m1, but which may depend on e1 and E2.

Field Access

When the above case doesn't match, this case is tried.

e1.m1

This returns an object v1 that has a get method with the same type as m1 and which does the same as e1.m1(E2) when called as v1.get(E2).

Variables

val v1: t1 = e1

This creates a "variable" which cannot be changed (a value binding). It's visible to anything following the definition in the rest of the enclosing scope. It has the name v1, the type t1 and the value e1. Wherever v1 is visible and occurs in a value position, it evaluates to it's value.

If : t1 is not present, it is taken to be the type of e1, or if this type cannot be fully inferred from e1 alone, the type checking fails.

If : t1 is present, it is taken to be the expected type of e1.

var v2: t2 = e2

Has the same semantics as val, except that it can be assigned to. When this happens the old value is forgotten and it gets a new value, thus performing a destructive update. This means that the value of such a variable can change over time. The assignment looks like:

v2 = e3

The return value of variable definitions and assignments is Void, which is the only value that has the type Void.

Operators

e1 and e2
e3 or e4
not e5

Logical conjunction, disjunction and negation respectively. The two first are lazy, meaning that e2 won't be evaluated if e1 is false, and e4 won't be evaluated if e3 is true. It won't type check if any of the expressions are not of type Bool.

Functions

fun v1[N1](A1): t1 where Y1 do b1 end

Defines a function called v1 that has generics N1 with constraints Y1, takes the arguments A1, returns something of the type t1 and has the body b1. If any of the types in A1 are left out, the type checker fails. If : t1 is left out, the type of b1 is assumed, except when it can't be inferred from b1, t1 and A1 alone, in which case the type checker fails.

Generics and constraints are explained in the class section.

The functions have the same visibility/scoping rules as variables. However, they also capture any variables that are visible at this point in the enclosing scope, so that these can be used inside the function, and are remembered as long as the function is alive. Variables must never be copied (semantically), they must be shared across all scopes that can see them.

The v1 "function" is actually a value binding to a functional value. As in the case of field access, a functional value is an object with a get method that corresponds to the function.

Each function in a sequence of one or more functions can "see" all the functions in that sequence. In other words, they can call each other (and themselves) and be mutually recursive.

The function definition itself evaluates to Void.

Anonymous Functions

fun[N1](A2): t2 where Y1 do b2 end

This evaluates to a functional object similar to what v1 would contain above. The only difference is that the function has no name, so there is no direct way to make it recursive (and no direct support for mutual recursion).

Classes

class n1[N2](A1): T2 where Y1 do b1 methods F1 end

This is the class named n1 whose constructor takes the arguments A1 (with explicit types) and which implements the interfaces T2 (type checking fails if they are not all interfaces). It is generic in the type names N2. It can only be constructed if for each type pair (t1, t2) in Y1 , t1 is a subtype of t2 . It's constructor body is b1 and it has the methods F1.

Each method definition in F1 looks like a named function definition.

The type names N2 are visible in T2's generic type arguments. At least one of the sides of each type pair Y1 must occur in N1. The constraints introduced by the where clause on the type names N1 are visible between do and end, as are A1 and N2.

The [N1], : T2, where Y1 and methods F1 can each be left out if they are empty. (A1) cannot be left out.

Any variables/functions declared in the outermost scope between do and methods are visible to F1. A special variable this is automatically introduced after the last variable definition in the outermost scope of the constructor. This variable refers to the object being constructed, and thus makes available all of it's methods. Because if it's late introduction time, all variables used in methods are initialized at that point.

Only instances of the class have type n1 (possibly with generics). Nothing can inherit from a class.

Companion Objects

Outside the class declaration, the only visible artifact is the type named by n1. However, a companion singleton object of the same name (but with no nameable type) is automatically created. It's get method takes the same arguments (and generics and constraints) as the class constructor and returns a new instance of the class. Calling this method looks like:

n1.get[T2](E2)

Which has the semantics explained in the method call section. If you want to make the constructor private, or provide additional functionality that does not require an instance of the class, you can define the companion object yourself:

object n1: T3 do b3 methods F3 end

The semantics are similar to that of the class, except from the missing parameters and that at most one instance can exist at any one time (per process). The unique instance is guaranteed to be initialized before the first method call on it. Circular initialization where objects mutually need each other to finish their constructor will either generate a compile time error or a runtime exception.

The get method won't be automatically generated if the companion object is manually defined, but inside (and only inside) the body and methods of the companion object the class constructor can be called like:

class[T4](E4)

The generics T4 are optional.

It is legal to define a companion object without it's corresponding class (or interface, or enum).

Enums

enum n1[N2] where Y1 do C1 methods F1 end

Enums are like classes, except there are multiple constructors C1, and the constructors have no body. It has a top level name n1, generics N2, constraints Y1 and methods F1, just like a class.

Each named constructor in C1 looks like this:

n2(A2)

If A2 is empty, the parenthesis must be omitted. The n2 is reachable through n1 as n1_n2, or if the expected type is the one bound to n1, directly as n2 without the prefix.

Default equality equal and pretty printing toString is defined structurally and using the Any.toString and Any.equal methods. Manual implementations of these take precedence.

Only instances of the enum have type n1 (possibly with generics). Nothing can inherit from an enum.

Interfaces

interface n1[N2]: T1 where Y1 do F1 end

Defines a structural interface called n1. It is similar to a class, except it has no constructor (or arguments) and cannot be instantiated.

The T1 type expressions must evaluate to interfaces. The methods of these interfaces are added to the n1 interface. If there are any methods with the same name but with different types (except for the variance rules as described below), the type checking fails.

A type is a subtype of an interface precisely if it contains at least the methods that the interface defines. However, in the type, argument types are allowed to be less specific (contravariant), and return types are allowed to be more specific (covariant).

A type is said to implement an interface if it's a subtype of it. It is also said to explicitly implement it if the interface occurs in the : T1 clause (and in that case, it only type checks if the implementing type indeed is a subtype of the interface).

Switch

Packages

Literals

Type Checking

Apart from the mentioned subtyping rules, the type checker uses a combination of expected type and type evaluation to compute the type of an expression.

Globally visible types on method and type boundaries are explicitly typed. Implicit types are only available in constructor and method bodies, and can only be used when the type can be inferred without looking at the following expressions in the sequence (if any).

TODOs

Figure out if it's possibly to statically detect all circular initialization dependencies for companion objects.

Explain why (for generics) var is invariant while val is covariant. Introduce notation for variance and covariance (verify that it's still required with the constraint model).

Formal type inference rules.