The Definition of Nex
Chapter 4

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.

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.

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).

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

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 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. This rule is recorded with the arithmetic operators in Appendix B.

Optional types

An optional type ?T has the values of T together with nil.

?T does not conform to T. A value of an optional type can be used where a non-optional 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.

Why contravariant, and why it is sound Contravariance is what makes conformance a local guarantee. A value that conforms to Function(a: Animal) really does accept every Animal, so a call through that type cannot go wrong, and there is no “catcall” to track down later. This is the opposite of the Eiffel tradition, which makes parameters covariant. That allows unsound conformances, which must then be caught by a separate whole-program analysis. Nex instead rejects the unsafe direction at the point of conformance, with an error at the offending value. The same rule governs overriding (Section 4.9): an overriding method may widen a parameter type and narrow its return type, but not the reverse. It also matches the Design by Contract principle the language follows elsewhere: an heir may weaken what it demands and strengthen what it guarantees.

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

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

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

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 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 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).

Overloading by number of arguments A class may declare several methods with the same name if they take different numbers of parameters. A call selects among them by the number of arguments it passes. There is no overloading by parameter type, and free functions may not be overloaded at all.

The safe access e?.f may be applied to a receiver of optional 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 optional type is a compile-time error.

Object creation

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

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:

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.

Object tests

An object test ? e as x requires e to have an optional 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-optional 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.

A REPL implementation limitation, not a language one The exception concerns elaboration, not execution, and it holds wherever a whole program or a single interactive input is checked as one unit: a let naming a nested closure, an entire file, or one multi-statement REPL input. There is one known gap in the current implementation: a mutually recursive pair defined together in one REPL input, then called from a later, separate one. The interactive session keeps the two closures’ run-time values and compiled metadata in ways that can disagree once a later input re-runs one of them, so the call fails there, even though the definition was accepted. A closure that only calls itself is unaffected. Ordinary function definitions (Section 4.8), including ones using declare function, are unaffected in every case: define mutually recursive routines with function instead of let when they must be called across separate REPL inputs.

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 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:

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 narrows nothing, 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 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:

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.

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.

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 elaborated with only the fields of the current object in scope: not the parameters, not local variables, and not result. Any expression that is well typed there is allowed, and old e has the same type as e. Writing old outside an ensure clause, or applying it to a parameter, 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, since every name it reads is a field, and its value is the length the collection had 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 optional: 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.

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.

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.