Static Semantics

The static semantics describes what can be known about a program before it runs, and the checks that this knowledge makes possible (Section 1.2). Checking a program and working out the types of its phrases is called elaboration. A program that elaborates without error is accepted; one that does not is rejected with a compile-time error, and never reaches the dynamic semantics of Chapter 5.

This chapter first describes the types (Section 4.1) and the names in scope during elaboration (Section 4.2), then the relation between types on which every check depends, conformance (Section 4.3). The remaining sections give the checks themselves: for expressions, statements, contracts, generics, free functions, and the structure of classes.

4.1Types

A type is one of the following.

• A numeric type: Integer, Byte, Integer16, Integer32 or Real.
• Another scalar type: Char, Boolean or String.
• A class type, written A or A[T1, …, Tn], where A names a class and T1 to Tn are types supplied for its generic parameters.
• A type variable: a generic parameter of an enclosing class or routine, such as G within class Box [G].
• A function type, written Function(a1: T1, …, an: Tn): T, the type of a function that takes arguments of types T1 to Tn and returns a T.
• The unconstrained function type, written Function with no parameter list, to which every function type conforms.
• A detachable type, written ?T, whose values are the values of T together with nil.
• Any, the type to which every type conforms. It is the type of the root class Any.
• The void type, the type of a statement and of a call to a routine that declares no return type. It is not a value type, so no field, parameter or variable may have it.
• The nil type, the type of the constant nil. It conforms to every detachable type and to Any, and to nothing else.

The scalar types, Any, Function and the collection types are not primitive in any deep sense. They are ordinary classes of the standard environment (Appendix B), and a scalar type such as Integer is simply a class type. They are listed separately only because the lexer treats their names specially.

4.2The Static Environment

Each phrase is elaborated against a static environment: the names in scope at that point, and what each one means. It has three parts.

• The classes in scope. For each class name, the environment records the class’s signature: its generic parameters and their constraints, its modifiers (deferred, sealed), its parents, the fields it declares with their types, and the parameter and return types of its methods and constructors.
• The variables in scope, with their types: the parameters and local variables of the enclosing routine or block, and the fields of the current object.
• The type variables in scope: the generic parameters of the enclosing class and routine.

A declaration of a variable adds it to the environment for the rest of its scope, and shadows any variable of the same name in an enclosing scope.

The fields and methods of a class are those it declares itself together with those it inherits from its parents. A class’s own declaration of a member overrides any inherited member of the same name.

4.2.1Qualified Names and Ambiguity

The classes in scope come from two sources: the classes the current compilation unit declares itself, and those brought in by each of its intern declarations (Section 3.6). Each interned class is in scope under both its bare name and its qualified name (Section 3.6.1).

• The current unit takes precedence. If the unit declares a class A itself, the name A means that class, whatever any interned unit also declares under the bare name A.
• A qualified name is never ambiguous. It always names the one class it spells out, however many other units declare a class with the same bare name.
• The same unit interned twice counts once. Two intern declarations that reach the same compilation unit, directly or through what each interns in turn, contribute its classes once, not twice. The procedure of Section 7.2 visits each compilation unit at most once, so this is never a source of ambiguity.
• A bare name may be ambiguous. If the current unit does not declare A and more than one interned unit does, the bare name A is an ambiguous reference. It is a compile-time error to write it unqualified as a type, as a parent in an inherit clause, in a create, or in a match pattern.

Writing the class’s qualified name always avoids the ambiguity. So does renaming the interned unit with as (Section 3.6), provided the renamed intern names a path. Renaming an intern that has no path gives no qualified spelling to fall back on; it only renames access to whichever single class the bare name already denotes.

4.3Conformance

The central relation of the static semantics is conformance. When a type S conforms to a type T, a value of type S may be used wherever a value of type T is expected: assigned to a variable of type T, passed as an argument for a parameter of type T, or returned from a routine whose return type is T. S is then also called a subtype of T.

One type conforms to another exactly when the rules of this section say so.

General rules

• Every type conforms to itself.
• If S conforms to T and T conforms to U, then S conforms to U.
• Every type conforms to Any.

Inheritance

A class type conforms to each of its parents, with the type arguments substituted through the inherit clause. For example, if a class is declared class LabelledBox [G] inherit Box [G], then LabelledBox[Integer] conforms to Box[Integer], where Box is the generic class of Section 4.7.

class Animal
  create make() do end
feature
  speak(): String do result := "..." end
end

class Dog
  inherit Animal
  create make() do Animal.make() end
feature
  speak(): String do result := "woof" end
end

let a: Animal := create Dog.make()
print(a.speak())

The let is accepted because Dog conforms to Animal, so a Dog may stand where an Animal is expected. The call a.speak() has type String. At run time it prints woof, because the call dispatches on the class of the object (Section 5.4).

The rule makes no distinction between a Nex parent and an imported host interface or class (Section 4.9), which is a class type like any other. A class that implements a host interface conforms to it, and a class that extends a host class conforms to that class, exactly as Dog conforms to Animal. A value of such a class may therefore be assigned to a variable whose type is the host interface or class, whether or not the code is inside a with "java" block (Section 5.8).

Inheritance is the only way one class type conforms to another. In particular, two types made from the same generic class conform only if their type arguments are the same: Box[Dog] does not conform to Box[Animal], even though Dog conforms to Animal.

Numeric types

There are exactly five numeric types: Integer, Real, and the three fixed-width integer types Byte, Integer16 and Integer32. (Integer64 is another name for Integer, not a further type.) None of them conforms to another. Even Integer does not conform to Real. Numeric conversions are explicit, and are made by methods of the numeric classes (to_byte, to_integer16, to_integer32, to_integer, to_real; Appendix B). Each method that narrows checks that its result is in range.

In particular, a numeric constant is never converted to fit its context. The constant 200 has type Integer, which does not conform to Byte, so let b: Byte := 200 is a compile-time error; the constant 200u8 has type Byte. Equally, a Byte is not accepted where an Integer parameter is declared, nor the reverse. Nor does convert change a number’s type (Section 4.5): two different numeric types are related by conformance in neither direction, so a convert from one to the other is a compile-time error.

The one implicit numeric rule belongs to the arithmetic operators, not to conformance. The operands of an arithmetic operator may be of any two numeric types. The result is a Real if either operand is a Real, and an Integer otherwise (Section 4.4). So an Integer operand is accepted beside a Real one, and arithmetic on fixed-width operands yields an Integer, never a fixed-width value: Byte plus Byte is an Integer. Unary minus on a signed fixed-width operand is the one exception (Section 4.4). This rule is recorded with the arithmetic operators in Appendix B.

Detachable types

A detachable type ?T has the values of T together with nil. A type that is not detachable is attached: no value of it is ever nil.

• T conforms to ?T.
• The nil type conforms to every detachable type.
• If S conforms to T, then ?S conforms to ?T.

?T does not conform to T. A value of a detachable type can be used where a non-detachable one is expected only after a test has shown that it is not nil (Section 4.5, Narrowing).

Function types

A function type conforms to another when it accepts at least the arguments the other accepts, and returns at most what the other promises. Precisely, Function(a1: S1, …, an: Sn): S conforms to Function(b1: T1, …, bn: Tn): T when both take the same number of parameters, each Ti conforms to the corresponding Si, and S conforms to T. Parameters vary in the opposite direction to the function type (they are contravariant), and the result in the same direction (it is covariant). Every function type conforms to the unconstrained function type Function.

So a Function(a: Animal): String conforms to a Function(a: Dog): String, because a function that handles any animal can stand in wherever a function that handles dogs is wanted. The reverse does not hold.

Refinement types

A refinement type, declared declare type R = B where n: p (Section 3.5.1), conforms to its base type B. Widening is therefore free: a value of type R may be used wherever a B is expected.

The reverse is not a conformance. A B does not conform to R, because not every B satisfies the predicate p. Instead, a value of the base type enters a refinement type only at a narrowing site: a variable, parameter, field or return of type R, or an explicit convert … to a variable of type R. At each such site, elaboration attaches the predicate as a contract to be checked at run time (Section 5.6).

The refinement type’s name is kept during elaboration, so these narrowing sites stay visible to the checker. It disappears only in the representation of values, where an R is exactly a B. Consequently, an operation on refinement values has the base type: q1 + q2 for two Quantity operands is an Integer, and is checked again only if it flows into a target of type Quantity.

4.4Elaboration of Expressions

For each kind of expression, this section gives the conditions under which it is accepted and the type it has. If a condition does not hold, it is a compile-time error. The kinds of expression follow the grammar of Section 2.7.

Constants and variables

A constant has the type of its scalar class. An integer constant is an Integer; with the suffix u8, i16 or i32 it is a Byte, Integer16 or Integer32 (Section 2.2). A real constant is a Real, and string, character and boolean constants are String, Char and Boolean. The constant nil has the nil type.

A variable has the type the environment records for it. The variable result has the declared return type of the enclosing routine, and is in scope only within a routine that declares one (Section 2.9).

The current object and its ancestors

• this is in scope within the body of a method or constructor, and has the type of the current class.
• super is in scope there too, provided the current class inherits exactly one class. Its type is that class. In a class that has no inherit clause, or names more than one parent (Section 3.2), every use of super is a compile-time error, and the intended ancestor must be named instead.
• The name of an ancestor, B, may be written where super could be, as in B.describe. B must be a class to which the current class conforms, other than the current class itself, and need not be a direct parent. Its type is B.

Naming an ancestor in this way works as follows for each kind of member.

• Methods. B.describe is checked like a call on a receiver of type B (see Member access and calls, below). It finds a method that B declares or inherits.
• Constructors. The same form written before a constructor’s name, B.make(…), does not create an object. It delegates to that ancestor’s constructor (see Object creation, below, and Section 5.5). Here B must declare the constructor itself: one it only inherits does not qualify.
• Fields. B.f reads the field f as B would see it, whether B declares or inherits it. This is how to pick out a particular ancestor’s copy of a field when repeated inheritance has produced more than one (Section 4.9): a plain f cannot say which copy is meant, but B.f can.

Naming an ancestor lets a class read through it, but not assign through it. However the receiver is written (f, this.f, super.f or B.f), an assignment to a field is accepted only in the class that declares the field (Section 4.5, Field assignment). So B.f := e is a valid assignment only when the class doing the writing is B itself.

Operators

• Arithmetic operators (+ - * / % ^) on numeric operands. The operands may be of any two numeric types. The result is a Real if either operand is a Real, and an Integer otherwise (Section 4.3). Unary minus yields the type of its operand, an Integer16 or Integer32 included, except that on a Byte it yields an Integer.
• Ordering operators require operands of the same type, and yield Boolean. A Byte cannot be ordered against an Integer, nor an Integer against a Real, until one of them is converted.
• Equality operators (=, /=, ==, !=) require the type of one operand to conform to the type of the other, and yield Boolean. So 1 = 1.0 and 65u8 = 65 are compile-time errors.
• Logical operators require Boolean operands and yield Boolean.

An infix operator stands for a method of its left operand’s class, and a class may make this literally true for itself. A class binds an arithmetic operator to a one-argument method with an alias clause (Section 3.4), declared in the class or in one of its ancestors. When the left operand of that operator is not numeric, the operator is checked as the call it abbreviates: the right operand’s type must conform to the method’s parameter type, and the type of the expression is the method’s return type.

The numeric rule is tried first, so an alias can never displace built-in arithmetic. If neither rule applies, the expression is a compile-time error.

Member access and calls

A field access e.f is accepted if:

• the type of e is a class type, say A[T1, …, Tk]; and
• A has a field named f, declared or inherited, that is accessible at the point of the access; and
• f is not ambiguous on A (Section 4.9, Ambiguous inherited names).

The type of the access is the type of the field, with A’s generic parameters replaced by T1 to Tk (Section 4.7).

A call e.m(e1, …, en) is accepted if:

• the type of e is a class type, say A[T1, …, Tk];
• A has a method named m with n parameters, declared or inherited, that is accessible at the point of the call;
• m with n parameters is not ambiguous on A (Section 4.9, Ambiguous inherited names); and
• the type of each argument ei conforms to the type of the corresponding parameter, after A’s generic parameters are replaced by T1 to Tk.

A bare name f or call m(e1, …, en) in the text of a class that denotes a member of the class, rather than a local, a parameter or a global, is checked as this.f or this.m(e1, …, en), and so falls under the same rule. An ancestor name P.f or P.m(…) checks the name on P instead.

The type of the call is the method’s return type, with the same replacement, or the void type if the method declares no return type.

A member is accessible unless it is declared in a private feature section of A and the access is written outside the text of A.

class Counter
  create make() do count := 0 end
feature
  count: Integer
  bump(n: Integer): Integer do result := count + n end
end

let c := create Counter.make()
print(c.bump(5))

The receiver c has type Counter. The method bump takes one Integer and returns one, and the argument 5 conforms to Integer, so the call c.bump(5) is accepted and has type Integer. It evaluates to 5. An argument of the wrong type, or the wrong number of arguments, is a compile-time error.

A bare call m(e1, …, en) is checked as a call on this if m is a method of the current class, and otherwise as a call of the free function m (Section 4.8).

The safe access e?.f may be applied to a receiver of detachable type. If e has type ?T, the conditions are those of e.f on a receiver of type T, and if that access has type S, the safe access has type ?S: it yields nil when e is nil. An ordinary access or call on a receiver of detachable type is a compile-time error.

Object creation

A creation create A[T1, …, Tn].k(e1, …, en) is accepted if:

• A is not deferred;
• A[T1, …, Tn] is a well-formed type (Section 4.7);
• k is a constructor of A, declared or inherited, that is not ambiguous on A (Section 4.9); and
• the type of each argument conforms to the type of the corresponding parameter of k.

Its type is A[T1, …, Tn]. A creation that names no constructor, create A, is accepted only if A has no constructors at all, neither declared nor inherited.

A constructor delegation, written P.k(e1, …, en) or, where super is allowed, super.k(e1, …, en), runs another constructor on the object already being built, instead of creating a new one. It may appear anywhere a statement may, but is most often the first statement of a constructor, delegating to a parent’s constructor. It is accepted if:

• P is a proper ancestor: the current class conforms to P, but is not P;
• P declares k itself; and
• the type of each argument conforms to the type of the corresponding parameter of k.

The second condition is stricter than for an ordinary call, which accepts a method found further up the ancestry. A constructor’s job is to initialise the fields declared alongside it. Delegating to a constructor two levels up would skip whatever the intermediate ancestor’s constructor sets up for its own fields.

A delegation produces no value and declares no names; it is checked like a statement (Section 4.5), even though it is written as a call. Its run-time behaviour is described in Section 5.5.

Conditional expressions

A conditional expression when c then a else b end requires c to be a Boolean. Its type is the join of the types of a and b: the narrowest type to which both conform. The join of Dog and Animal is Animal, and the join of Dog and the nil type is ?Dog. Every type conforms to Any, so a join always exists. Where there is no single narrowest type, the join is Any: the join of Integer and Real is Any, and so is the join of two classes that both inherit Animal and Swimmer, since neither of those conforms to the other. The condition narrows the types of variables in the two branches as an if statement’s does (Section 4.5, Narrowing).

Anonymous functions

An anonymous function fn(x1: T1, …, xn: Tn): T do body end has the type Function(x1: T1, …, xn: Tn): T. Its body is checked with the parameters in scope, and with result of type T.

Parameter types, and the result type, may be left out where the anonymous function stands in a place that expects a function type Function(y1: U1, …, yn: Un): U: as the initialiser of a let of that type, the value assigned to a variable (or to result) of that type, or an argument whose parameter has that type (of a routine, a constructor, or a function value). Each omitted Ti is then Ui, and an omitted T is U; the anonymous function must have n parameters, and any type it does write must agree with the expected one. For a call to a generic routine or constructor, the type arguments are first inferred from the other arguments (Section 4.7), and the expected type is the parameter’s type in that instance:

function apply_to[T](x: T, f: Function(v: T): T): T do
  result := f(x)
end
print(apply_to(10, fn (v) do result := v + 1 end))   -- v is an Integer

Where no function type is expected, every parameter type must be written.

An expression function fn (ps) => e (Appendix C.8) whose result type is neither written nor supplied by the context has as its result type the type of e, checked with the parameters in scope. In particular, a generic parameter that only the expected result type mentions, such as U in map_all[T, U](xs: Array[T], f: Function(x: T): U), is not imposed on the function; it is inferred from the function’s result:

let lengths := map_all(["a", "bb"], fn (s) => s.length)   -- Array[Integer]

Object tests

An object test ? e as x requires e to have a detachable type, and has type Boolean. It is true when e is not nil. Used as the condition of an if, it makes x available in the then branch with the non-detachable type (Section 4.5, Narrowing).

4.5Elaboration of Statements

A statement is checked against the environment in force where it is written. A statement that declares a name adds it to the environment for the statements that follow it in the same block. A statement that declares nothing leaves the environment as it was. A block is checked one statement at a time, each against the environment the statements before it have built.

Local declarations

A declaration let x: T := e is accepted if the type of e conforms to T, and no other variable named x is declared in the same block. A variable in an enclosing block may be shadowed. After the declaration, x is in scope with type T. A let with no type annotation, let x := e, gives x the type of e.

let x: Integer := 10
if x > 5 then
  let y: Integer := x * 2
  print(y)
else
  print(0)
end

The let puts x, of type Integer, in scope for the if that follows. Inside the then branch, y is added as well, but only for that block. It is not in scope in the statements after the if.

Self- and mutually recursive closures

There is one exception to the rule that a let puts its name in scope only after the declaration, mirroring the treatment of free functions in Section 4.8. When the initialiser e is itself an anonymous function fn…, the name x is already in scope while e is checked.

let fact: Function(n: Integer): Integer := fn(n: Integer): Integer do
  if n <= 1 then
    result := 1
  else
    result := n * fact(n - 1)
  end
end
print(fact(5))                       -- 120

A closure declared this way can call itself, just as a named function can (Section 4.8).

The same applies to a run of consecutive lets in one block whose initialisers are all anonymous functions. All of their names are put in scope together, before any of the bodies is checked, so the closures may call one another whichever is written first. No declare function-style signature is needed, because the whole run is checked as one unit.

let is_even := fn(n: Integer): Boolean do
  if n = 0 then result := true else result := is_odd(n - 1) end
end
let is_odd := fn(n: Integer): Boolean do
  if n = 0 then result := false else result := is_even(n - 1) end
end
print(is_even(10))                   -- true

This exception is withdrawn for any name that is introduced a second time within reach of the closures, by another let in the same block or as a parameter of one of the closures. The ordinary rule then applies, and the name is simply not yet in scope. A program that relies on self- or mutual reference should therefore give each such closure, and every name it refers to, a name used nowhere else in the enclosing block.

Assignment

An assignment x := e to a variable is accepted if x is a variable in scope and the type of e conforms to the type of x. It leaves the environment unchanged. Assigning a once field anywhere other than in a constructor of its class is a compile-time error; this is the static enforcement of a once field’s immutability.

Field assignment

A field can be assigned through several spellings: this.f := e, super.f := e, an arbitrary object expression o.f := e, an explicit ancestor name B.f := e, or the bare form f := e with no receiver at all. All of them are checked by the same rule, whichever spelling is used. An assignment to a field is accepted if:

• the type of e conforms to the declared type of f; and
• the assignment is written in the text of the class that declares f.

The second condition holds whatever the receiver’s static type, whatever object it refers to at run time, and whether or not a receiver is written. The bare form is just this.f := e with the receiver left out. So a class may assign a field of another object of its own class, other.f := e, from within one of its methods. But it can never assign a field it only inherits, from a constructor or anywhere else, under any spelling.

The one exception is where a let or a parameter in scope has the same name as the field. The bare form f := e then assigns that variable, by the rule for assignment above.

Inheriting a field therefore gives a class no way to assign it directly, only to read it. A subclass constructor that needs to initialise an inherited field has two options: delegate to a constructor of the declaring class (Section 4.4), or call a method that the declaring class provides for the purpose. These are the same options any other code outside that class has.

This is why the derived forms of Appendix C, such as the variant constructors generated for an enum union, route every such assignment through a method the parent declares. An ordinary method dispatches normally and allocates nothing, so it is the natural way to provide this, without resorting to constructor delegation for something that is not really about construction.

The run-time rule for field assignment (Section 5.8) has no restriction of its own: by the time a program runs, this rule has already ensured that every field assignment in it is allowed.

Conditionals and narrowing

The condition of an if must be a Boolean. Each branch is checked against the environment the if is given, except that the condition may narrow the types of some variables within a branch. In the then branch:

• after x /= nil, where x is a local variable or parameter of type ?T, x has type T;
• after convert e to x: S, x has type S rather than ?S;
• after ? e as x, where e has type ?T, x is in scope with type T;
• after a and b, the narrowings of both a and b apply.

In the else branch, after x = nil, where x is a local variable or parameter of type ?T, x has type T.

No other condition narrows anything. In particular, or and implies narrow nothing in either branch, and an and condition narrows nothing in the else branch.

Narrowing also applies within the condition itself. The right operand of an and is checked with the narrowings of its left operand in effect, so in if x /= nil and x.v > 0 then the access x.v is accepted. This holds for every and, wherever it appears: in a require, ensure or invariant clause, an assert, an assignment or an argument, so print(x /= nil and x.v > 0) is accepted too. It is sound because and evaluates its right operand only when the left is true (Section 5.3). The narrowing ends with the and: after let ok := x /= nil and x.v > 0, x still has type ?T. The right operand of an implies is checked the same way, since it too runs only when the left operand is true: x /= nil implies x.v > 0 and ? e as y implies y.v > 0 are accepted, the second with y in scope only in the right operand. The conditional expression when narrows its branches in the same way as if (Section 4.4).

class Point
  create make(v: Integer) do value := v end
feature
  value: Integer
end

function find_point(n: Integer): ?Point do
  if n > 0 then result := create Point.make(n) end
end

let x := find_point(3)
if x /= nil then
  print(x.value)              -- x has type Point here
end
print(when x = nil then 0 else x.value end)

x has type ?Point. In the then branch of the if, and in the else branch of the when, it has type Point, so x.value is accepted. The program prints 3 twice.

A nil test never narrows a field. Between the test and the use, any call may set the field to nil again, and so may another task (Chapter 6). A detachable field is used through ? f as y, which binds its attached value to a new local y; no later assignment to the field affects y.

A narrowing of a local variable or parameter x lasts only while nothing can have made x nil again:

• An assignment to x of nil, or of a value of a detachable type, ends it for the rest of the narrowed branch, including after any nested block that contains the assignment. An assignment of a value of a non-detachable type leaves it in effect. An assignment in one branch of an if, or in one clause of a match, does not affect the other branches or clauses.
• A loop body that assigns x ends a narrowing made before the loop, throughout the loop: the body runs again after the assignment.
• A variable that is assigned inside an anonymous function or a spawn body is never narrowed, unless it belongs to that body (a parameter of the function, or a variable it declares): any call may run the function, and a task runs alongside the code that spawned it.
• Inside an anonymous function or a spawn body, a narrowing made outside it applies only to a variable that no assignment in the enclosing routine targets, since the body may run after such an assignment.
• A narrowing applies to the variable that was tested, not to one with the same name declared in a nested block.

Blocks and scope

The loop, case, match, across and do/rescue statements check their blocks with any variable they introduce added to the environment: the cursor variable of across, or the bound variable of a match clause. A block never makes its local variables visible to the statements after it.

Type dispatch and exhaustiveness

A match whose subject has class type A dispatches on the class of the subject’s object at run time. Each clause B as x then block requires B to conform to A, and checks its block with x in scope with type B.

A destructuring clause B(…) also puts each field it names in scope in the block, with that field’s declared type. A guard if g requires g to be a Boolean, and is checked with those names in scope.

If A is sealed, the clauses must cover every subclass of A, unless an else clause covers the rest. A missing variant is a compile-time error.

• A clause is identified by the class declaration it names, not by how the name is spelt. Naming a variant by its qualified name (Section 4.2.1) covers the same subclass a clause with the bare name would, never an additional one.
• A clause that can fail after its class matches does not count toward coverage, since control may fall through to the next clause. This is a clause with a guard, a nested pattern, or a type test f: T on a field whose declared type does not already conform to T. A variant whose only clause is of this kind still needs a plain clause, a wildcard, or an else.

This exhaustiveness check is the whole purpose of the sealed modifier, and is why a sealed class is required to be deferred (Section 4.9).

Type conversion

The expression convert e to x: S tests whether the value of e can be viewed as an S, and binds x to it if so. It is accepted if the type of e and S are related by conformance, in either direction. Its type is Boolean, and it puts x in scope with type ?S, or S in the then branch of an if whose condition it is (Narrowing, above).

At run time it succeeds, binding x to the value, when the class of the value conforms to S. Otherwise it yields false, with x bound to nil. Because two different numeric types are related by conformance in neither direction (Section 4.3), convert never turns an Integer into a Byte or a Real; the conversion methods do that.

4.6Contract Formation

Every assertion, in a require, an ensure, a class invariant, a loop invariant or an assert, must have type Boolean. A loop variant must have type Integer. Each kind of assertion is elaborated with its own names in scope.

• A precondition sees the routine’s parameters and the fields of the current object.
• A postcondition sees the same names, together with result and old expressions.
• A class invariant sees the fields of the class.
• An assert sees whatever is in scope at the point where it is written, like any other statement. The bare form, with no label, is elaborated exactly as the named form is.

The contract of a deferred method is elaborated in the same way, against its own signature: its precondition sees its parameters and the fields of the current object, and its postcondition sees these together with result, when the method declares a return type, and old expressions. A postcondition that reads result requires a return type here as anywhere else.

The label of an assertion has no effect on its type. It is carried into the dynamic semantics only to name the condition in a violation report.

old expressions

The expression old e may appear only in a postcondition. Its operand e is evaluated on entry (Section 5.6), so it is elaborated with only what has a value then in scope: the fields of the current object, the parameters, and the routines it can call, but not result, and not a name the postcondition itself binds with convert or an object test. Any expression that is well typed there is allowed, and old e has the same type as e. Writing old outside an ensure clause, nesting one old inside another, or applying it to a bare parameter, whose value cannot change, is a compile-time error.

class Counter
  create make() do count := 0 end
feature
  count: Integer
  bump()
  do
    count := count + 1
  ensure
    advanced: count = old count + 1
  end
end

let c := create Counter.make()
c.bump()
print(c.count)

The postcondition advanced is accepted because count is a field of the current class, so old count has type Integer, and the assertion as a whole is Boolean. At run time old count is the value the field held on entry, so after one call of bump the count is 1 and the postcondition holds.

The operand need not be a bare field. old items.length is accepted just as well, and its value is the length the collection had on entry; old size() is the value the query returned on entry, and old other.balance, for a parameter other, the balance that object held on entry (Section 5.6).

4.7Generic Elaboration

A generic class, such as class Kennel [G -> Animal], is checked once, with its generic parameters in scope as type variables. Each parameter may carry a constraint, the type after the arrow; a parameter with no constraint is constrained by Any.

A generic class type A[T1, …, Tn] is well formed if A has n generic parameters and each Ti conforms to the constraint of the corresponding parameter. Using a type that is not well formed is a compile-time error. The fields and method signatures of A[T1, …, Tn] are those of A, with each Ti in place of the corresponding parameter throughout.

A constraint is not only a test on the type argument; it is also what the body of the generic class may rely on. Within the class, a value whose type is a parameter constrained by K has the members of K: its fields may be read and its methods called, and each call is checked against K’s signature. A method that is deferred in K may be called on such a value, even though no implementation is known statically: the class of the actual object supplies one (Section 5.4). An unconstrained parameter has no members beyond those of Any.

function total_area[T -> Shape](xs: Array[T]): Integer do
  result := 0
  across xs as s do
    result := result + s.area()   -- area is deferred in Shape
  end
end

class Box [G]
  create make(x: G) do value := x end
feature
  value: G
  get(): G do result := value end
end

let b: Box[Integer] := create Box.make(42)
print(b.get())

The type Box[Integer] is well formed, since the unconstrained parameter G accepts any type argument. Within it G stands for Integer, so get() returns an Integer. Had the parameter been declared with a constraint, as in [G -> Comparable], the argument would have to conform to it.

Whether a value of a parameter’s type may be nil is decided where a type is written, not by the parameter. A type argument may itself be detachable: Box[?String] instantiates G as ?String, so a value of type G in that instance may be nil, and any parameter accepts such an argument. Within the class text, where G may stand for an attached type, nil may be assigned only to something declared ?G, which admits it whatever the argument. A leading ? on the parameter itself, as in [?G], is accepted and changes none of this.

A generic routine is checked in the same way, with its type parameters in scope only within the routine. A call may write the routine’s type arguments, as in total_area[Circle](xs). Its parameters are then those of that instance, and each argument must conform to its parameter there: an Array[Shape] is not an argument for total_area[Circle], since Array[Shape] does not conform to Array[Circle]. A call that writes no type arguments has them inferred from the types of its arguments, and each inferred argument must conform to the constraint of its parameter.

Because elaboration substitutes type arguments rather than erasing them, Array[Integer] and Array[String] are different types, with different field and method signatures. Neither conforms to the other (Section 4.3).

4.8Free Functions and the Static World

The free functions of a program are elaborated together with its classes, so any function may call any other, whatever their order in the program text. This alone is what allows mutual recursion among them: a function’s signature need not be announced before it is called.

A bare call m(e1, …, en), where m is not a method of the current class, is checked against the signature of the free function m, wherever in the program m is defined. The conditions are those of a method call (Section 4.4): the number of arguments must match, and each argument’s type must conform to its parameter’s. The type of the call is the function’s return type.

A declare function signature (Section 3.4) is a separate, optional device. It states m’s signature explicitly, at the point where a reader most wants to see it, and the later definition of m must then match it exactly. It is a check on the declaration, not a requirement for calling m before its definition.

Free functions, unlike methods of a class, cannot be overloaded: each free function name must be unique. It is a compile-time error to define a free function twice, or to define one whose signature disagrees with its declare function. The error names the function.

4.8.1Qualified Calls and Ambiguous References

The collision that Section 4.2.1 describes for classes can happen with free functions too: two units interned into the same program may each declare a function with the same bare name.

• A function declared in the current unit takes precedence, as a class does. It shadows any interned function with the same bare name, and is never part of an ambiguity.
• Otherwise, a bare name m that is not a method of the current class names a function only if at most one interned unit declares a function called m. If more than one does, m is an ambiguous reference, and it is a compile-time error to call m(…) by its bare name.

Unlike a class, a free function has no qualified-name syntax of its own (Section 3.6.2). The way around an ambiguity is a qualified call, p.m(e1, …, en), written like a call on a variable named p (Section 2.7). It is elaborated as a qualified call only when p is neither a variable in scope nor the name of a class. A variable or class of that name always takes precedence, just as a class declared in the current unit takes precedence over an interned one.

When it applies, p.m(e1, …, en) is a call of the free function whose interned unit path and name, joined by a dot, spell p.m. Its arguments are checked, and its type determined, as for an ordinary call of a free function. A longer chain, a.b.m(…), is resolved in the same way against the dotted name it spells: everything before the final call is the unit path. This is unambiguous, because the grammar of Section 2.7 allows a chain of member accesses to be divided in only one way.

4.9Well-Formedness of Classes

Beyond the typing of expressions and statements, a program must satisfy conditions on the structure of its classes. They are checked once, over the whole static world. A class that breaks one of them is a compile-time error.

• Acyclic inheritance. No class may inherit from itself, directly or through other classes.
• Ambiguous inherited names.

  Members are matched by name and, for methods and constructors, by number of parameters. A field or constant matches a method with no parameters. Constructors are matched only with constructors.

  Each public member of a class has one or more origins, the declarations it descends from. A member the class only inherits keeps the origins it has in the parent it comes through. A member the class declares itself takes the origins of the inherited members it redefines, those that match it. If it redefines none, its own declaration is its only origin. The routines of the basis classes have their origins there, so equals, hash and to_string have the same origin, in Any, in every class.

  Suppose a class inherits members that match, through two of its parents. If the two have an origin in common, they are one member reached by more than one path, and Ambiguous member resolution, below, applies. Otherwise they are two unrelated members that only share a name, and the name is ambiguous on the class, unless one of the following holds:

  • The class itself declares a public member that matches them both. This member redefines both, and must conform to each (Conformant overriding, below).
  • Both are deferred methods. They then join into one deferred method with the origins of both, which the class or a descendant implements once.

  A name ambiguous on a class stays ambiguous on its heirs, until one of them declares a matching member. Private members take no part. A private member can be used only in the text of the class that declares it, so it is never reached through an heir.

  Inheriting an ambiguous name is not itself an error. Each parent’s code keeps using its own member, and the object holds both. What is rejected is an unqualified use of the name on the class (Section 4.4): a bare x or this.x in its text, a member access e.x or call e.m(…) whose receiver has the class as its type, a constant C.k, or a creation create C.k(…). Inside the class or a descendant, an ancestor name says which one is meant: A.x reads A’s. A client can use the object as one of the parents, since it conforms to each, or the class can expose the member it means through a feature of its own.

  class A feature x: Integer end
  class B feature x: Integer end
  
  class C
  inherit A, B
  feature
    sum(): Integer do result := A.x + B.x end   -- accepted
    bad(): Integer do result := x end           -- rejected: x is ambiguous on C
  end

• Ambiguous member resolution.

  Two parents named in one class’s inherit clause, or two ancestors reached through them, may share a common ancestor. A member that ancestor declares (a field, method or constructor) can then be reached by more than one path, and may have been redefined along some of them. This is not itself an error: the versions have an origin in common, so the name is not ambiguous in the sense of Ambiguous inherited names, above.

  An unqualified reference to such a member is resolved through the first parent named in inherit, searching that parent’s own ancestors depth-first before the next parent is tried at all.

  A member reached along another path can still be used deliberately, by naming the ancestor that declares it (Section 4.4): a call, for a method or constructor, and a read, for a field. Assignment is the exception. No ancestor name allows a class to assign a field it could not already assign (Section 4.5, Field assignment), so a particular path’s copy of a field can only be set or changed through a method of the ancestor that declares it.

  Put precisely, the home of a member x in a class B is the path of parent names that leads from B to the ancestor that declares x. If B declares x itself, the path is empty. Otherwise it is the first parent of B, in inherit order, through which x can be reached, followed by the home of x in that parent. The path always ends, because inheritance is acyclic.

  An unqualified reference to x in the text of B follows the home of x in B. An ancestor name P, or super standing for P, instead fixes the first step as P, and then follows the home of x in P. That second part is empty when P declares x itself.

  Similarly, the path to B’s own nested copy of an ancestor P (which Section 5.3 needs in order to evaluate an ancestor name) is empty if B is P. Otherwise it is the first parent Q of B, in inherit order, that conforms to P, followed by the path from Q to its copy of P.

• Attachment (nil safety).

  Every constructor of a class must leave each of the class’s fields attached, holding a value of its declared type rather than nil, unless the field has a detachable type, which admits nil. A constructor that can return with a non-detachable field still unattached is a compile-time error.

  Scalar fields are attached by their zero value, and Array, Map and Set fields by a new empty collection, so neither needs an explicit assignment. Detachable fields are attached to nil by default. Every other field must be assigned, whatever its type: a user class, a basis class such as Console or Task, or a function type. A field whose type is a generic parameter of its class needs no assignment, since the parameter may stand for a scalar. This discipline is what guarantees that a non-detachable reference is never observed to be nil at run time.

  “The class’s fields” includes those declared by its ancestors. Inheriting a field carries the obligation to attach it; it does not remove it. A subclass cannot meet that obligation by assigning the field directly, under any spelling, since only the declaring class may assign a field (Section 4.5, Field assignment).

  The only ways a subclass constructor can attach an inherited field are to delegate, directly or in turn, to a constructor of the declaring class (Section 4.4), or to call a method that the declaring class provides for the purpose. So a class that inherits fields needing attachment must route each of its own constructors through one or the other. When the declaring class has constructors, Parent construction, below, already requires the first.

• Parent construction.

  If a parent named in a class’s inherit clause has constructors, declared or inherited, every constructor of the class must call one of them, written P.k(…) or super.k(…) (Section 4.4). The call may be made in a constructor of the class that this one delegates to with this.k(…). When P only inherits its constructors, a call naming the ancestor that declares one, Q.k(…), counts as well. A call on P that is not a constructor does not count. As with attachment, a call in only one branch of a conditional counts: the rule guards against forgetting a parent, and does not prove that every path constructs it.

  A class that declares no constructors of its own is created through an inherited one, which runs only its own class’s part of the object. So such a class may have at most one parent with constructors; with more, it must declare a constructor that calls one of each.

  class C
  inherit A, B
  create
    make(y: Integer) do
      A.make(y)        -- required: A has constructors
      B.make(y * 2)    -- required: B has constructors
    end
  end

• Repeated inheritance and shared ancestors. When a common ancestor reached by more than one path (see Ambiguous member resolution, above) declares a field, the field is not shared. Each path has its own copy, attached separately by whichever constructor delegation reaches it along that path. A write to one path’s copy is never seen through another’s (Section 5.1).
• Conformant overriding.

  When a class A inherits B and redefines a method m of B, the signature of A’s m must conform to that of B’s, as function types do (Section 4.3): each parameter type may be widened but not narrowed, and the return type may be narrowed but not widened. A field of B may not be redeclared with a type that does not conform to its original one.

  The rule applies to every method m redefines:

  • With several parents, m must conform to the version inherited along each inherit clause, not only the first.
  • The methods of the basis classes count as inherited too. Every class inherits Any’s equals(other: Any), so equals(other: Point) narrows a parameter and is rejected; the same holds for compare in an heir of Comparable (Appendix B). Such a method keeps the Any parameter and narrows inside its body, with convert or match.
  • After the inherited signature is restated in the heir’s terms (Section 4.3), a type parameter of the heir is a type like any other: it conforms only to itself, to its constraint and to what that conforms to. So class Stack[E] inherit Container[E] may not redefine store(x: E) as store(x: Integer), and no method may redefine take(x: Any) as take(x: E).

  This is checked at the override: a method that narrows a parameter type or widens its return type is rejected there, and the error names the method and the offending position.

• Attainable preconditions.

  Call a version of a method (Section 5.6, Inherited contracts) a first declaration when it overrides nothing: no ancestor of its class declares a method of the same name and number of parameters. A first declaration with no require clause admits every call, and an override can only widen what its ancestors admit. So a method may not have a require clause if any first declaration it inherits, along any path through its ancestors, has none: that precondition could never be checked. The error names the first declaration. The precondition belongs there instead, and a deferred first declaration may carry one (Section 3.4).

  A version that is not a first declaration and has no require clause adds no precondition of its own; it neither admits every call nor prevents its heirs from widening.

• Inherited contracts and parameter names.

  The assertions an override inherits are read under its own parameter names, matched by position (Section 5.6), so an override may rename its parameters. It may not give a parameter a name that an inherited assertion already uses for something other than the parameter at that position, such as a field: the name would then denote the parameter. A name bound inside the assertion, by a parameter of an anonymous function, is not affected.

• Complete deferral. A class that is not deferred must supply a body for every method declared deferred in any of its ancestors. A class with an unimplemented deferred method is itself deferred, and may not be instantiated. Only a method declared deferred is unimplemented: an empty body, do end, implements the method, in a deferred class as in any other, and heirs may inherit it.
• Host-type conformance.

  When a parent named in inherit is an imported host interface or class rather than a Nex class, the inheriting class must supply a method for every member the host type declares without an implementation. The method is matched by name and number of parameters against the host type’s own declaration, spelt exactly as the host spells it. No correspondence between Nex’s naming conventions and the host’s is assumed.

  This is the host-facing counterpart of Complete deferral, and is checked the same way: a class that lacks such a method is rejected, and the error names the missing member.

• Single host-class extension.

  Among all of a class’s ancestors, at most one may be a concrete (non-interface) host class. A second is a compile-time error.

  A host platform’s object model may allow a concrete class only one superclass, and this condition holds whichever platform an implementation targets.

• Host superclass construction.

  A class that extends a concrete host class must do one of two things in each of its constructors. Either it begins with a call to the host superclass’s constructor, super.new(…) or the parent named in place of super, as the constructor’s first statement and nowhere else. Or it makes no such call at all, in which case the host superclass must be constructible with no arguments.

  In the first form, the call must pass a number of arguments that one of the host superclass’s constructors accepts. new is reserved for this purpose when the target is a host superclass; everywhere else it is an ordinary identifier (Section 5.5).

• Sealed implies deferred. A sealed class must be deferred. If a sealed class could be instantiated, a plain instance of it would be a value that an exhaustive match over its subclasses (Section 4.5) fails to cover. Requiring it to be deferred removes that value, and so keeps exhaustiveness meaningful.
• Once discipline. A once field is assigned only in constructors of its class (Section 4.5, Assignment).

4.10Extensions

An extension (Section 3.2.3) adds features to its target. This section gives the rules by which its target is found, its routines are elaborated, and the features it adds are reached. They are checked over the whole static world, after module links are resolved (Section 7.2), so an extension in one unit may name a class another declares.

The target

The target of extend T is found by trying, in order:

1. a class of the program named T, bare or qualified. A bare name that more than one interned unit declares is ambiguous, as anywhere else (Section 4.2.1), and the extension must name the class it means by its qualified name;
2. a built-in type: Integer, Byte, Integer16, Integer32, Real, Char, Boolean, String, Array, Map, Set, Map_Entry, Min_Heap, Task, Channel, the atomic types, Console, Process, Program, Any or Comparable (Appendix B). No other built-in type, such as Function or a cursor type, may be extended;
3. a host class or interface that an import names T.

If none is found, the extension is a compile-time error.

Extensions of classes

An extension of a class C is folded into C (Appendix C.9), and the routines it adds are elaborated as C’s own, with three differences that follow from their being written outside C.

• A client’s view. The body of an added routine sees only the public features of C and its ancestors; a private feature of C is not visible in it. Since it is not written in the text of C, it may not assign a field of C (Section 4.5, Field assignment): it changes an object’s state only by calling the object’s routines.
• One supplier per feature. A feature is identified by its name and number of parameters, and each feature of C comes from exactly one place: either C’s own declaration or a single extension. It is therefore a compile-time error for an extension to add a feature that C already declares, or that another extension already adds to C. Features that C inherits are the exception: an extension may supply one for C, and doing so redefines it, subject to Conformant overriding (Section 4.9).
• Adoption. A feature an extension introduces on an ancestor may already be declared by an heir. The heir’s declaration then redefines it, conforming to it and inheriting its contract (Section 4.6), as though the ancestor had declared the feature first.

Otherwise an added routine is a routine of C like any other. It is inherited, may be redefined in heirs, and takes part in contract formation (Section 4.6). In particular Complete deferral (Section 4.9) applies to a routine an extension declares deferred: every concrete heir of C in the program must supply it, by its own declaration, by an extension, or by a field of the same name. Because the rule is checked over the whole static world, a program that brings together a unit adding such a routine to C and a unit adding a new heir of C is rejected until it supplies the routine for that heir.

Extensions of built-in types

A built-in type has no declaration to fold into. Each routine f, of n parameters, that an extension of a built-in type T adds becomes a feature of T:

• A call e.f(e₁, …, eₙ) whose receiver has static type T elaborates as a call of the added routine, as a call of one of T’s own features would, with the routine’s parameter types and result type. For T = Any the receiver may have any type; for T = Comparable, any type that conforms to Comparable.
• In the body, this names the receiver and has type T. A name used without a receiver that is a feature of T (one of its own, one of Any’s, or one an extension of T adds) denotes that feature of this. So that this is never ambiguous, a parameter or local of the routine may not have the name of such a feature, just as a local of a method may not have the name of a field of its class.
• The routine may not be deferred, and may not have the name of a feature T or Any already has, whatever its number of parameters. Two extensions may not add the same feature to T.
• A generic T is extended with its own parameter names (extend Array [T]). A constraint on one, extend Array [T -> Comparable], makes the routines available only on receivers whose corresponding type argument satisfies it: calling one on an Array [Dog] whose Dog does not conform to Comparable is a compile-time error.
• Conformance among the scalar types is unchanged. An Integer is converted where a Real is expected (Section 4.3), not a kind of Real, so an extension of Real adds nothing to Integer.
• A class may not declare a feature, by name and number of parameters, that an extension of Any or Comparable adds. Such a feature belongs to every value (to every comparable one), and is not redefinable.

Extensions of host classes

An extension of a host class or interface H adds routines to H by the rules for built-in types above, with this of type H and the public methods of H as the features a body may call without a receiver. In addition:

• A call e.f(…) whose receiver’s static type is a host class reaches f when it is added to that class or to the nearest of its host supertypes that has it: its superclasses first, nearest first, then the interfaces of each.
• A feature, by name and number of parameters, may be added to only one class or interface of a host hierarchy. Adding it to both H and a host subtype of H is a compile-time error, so that the choice above never depends on more than one of them.
• The routine may not have the name and number of parameters of a public method of H, inherited ones included.
• The host classes that are the run-time form of built-in values (those of arrays, maps, sets, strings and the scalar types) may not be extended; the built-in type is extended instead. Nor may the root of the host hierarchy, since every value is an instance of it; Any is extended instead.
• The extension takes no generic parameters.

A program all of whose phrases elaborate, and all of whose classes are well formed, is statically valid. The dynamic semantics of the next chapter is defined only for statically valid programs.