Static Semantics

The static semantics describes what can be known about a program before it runs: the type of every expression, the conformance of every class to its parents, and the well-formedness of every contract. A program that passes these checks is elaborated; one that fails is rejected, and never reaches the dynamic semantics of Chapter 5.

We proceed in this manner: first the semantic objects—the types and bindings the rules manipulate; then the relations among them—conformance and lookup; then the inference rules that assign types to phrases.

4.1Types

A type is one of the following.

Here \(A\) ranges over class names. A class type with no arguments is written \(A\) rather than \(A[\,]\).

The scalar types, \(\mathsf{Any}\), \(\mathsf{Function}\), and the collection classes are not primitive in any deep sense. They are ordinary classes of the standard environment (Appendix B), and \(\texttt{Integer}\) and the rest are just abbreviations for particular class types. We keep them syntactically distinct only because the lexer does.

\(\mathsf{Any}\) is the type that every other type is a subtype of; it is the elaborated form of the root class Any.

\(\mathsf{Void}\) is the type assigned to a statement, and to a routine with no declared return type. It is not a value type, so it may not be the type of a field or parameter.

\(\mathsf{Nil}\) is the type of the constant nil. It is a subtype of every optional type, and of no other.

4.2The Static Environment

Elaboration takes place against a static environment, written \(C\), comprising three components:

• a class bindings \(\Sigma\), mapping each class name \(A\) in scope to its class signature — its generic parameters and their constraints, its modifiers (deferred, sealed), its parents, the typed fields it declares, and the typed signatures of its routines and constructors;
• a variable bindings \(\Gamma\), mapping each identifier in scope (parameters, locals, fields of the current object) to its type;
• a set \(\Delta\) of type variables currently in scope, introduced by the generic parameters of the enclosing class or routine.

We write \(C(x) = \tau\) for the lookup of an ordinary variable, and \(C \oplus \{x : \tau\}\) for the environment \(C\) extended with the binding \(x:\tau\) (shadowing any earlier binding of \(x\)). We write \(C(A)\) for the signature of class \(A\).

The functions \(\mathit{fields}(C, A)\) and \(\mathit{routine}(C, A, m)\) collect the fields, and the named routine \(m\), visible in \(A\) — those declared in \(A\) itself, together with those inherited from its parents. \(A\)’s own declarations override any inherited one of the same name.

4.2.1Qualified Names and Ambiguity

\(\Sigma\) is built 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 entered under both its bare and its qualified name (Section 3.6.1).

The current unit’s own declarations take precedence over anything interned. If the unit itself declares a class \(A\), \(\Sigma(A)\) is that declaration — regardless of what any interned unit also declares under the bare name \(A\).

A qualified name is always well-defined in \(\Sigma\), and always denotes the one declaration it names, however many other units happen to share its bare spelling.

Two intern declarations that name the same underlying compilation unit — directly, or transitively through what each in turn interns — contribute one declaration to \(\Sigma\), not two. The elaboration procedure of Section 7.2 visits each compilation unit at most once, so this is never a source of ambiguity.

A bare name \(A\) that the current unit does not declare itself is well-defined in \(\Sigma\) only when at most one interned unit declares a class of that name. When more than one does, \(A\) is an ambiguous reference: \(C(A)\) is undefined by ambiguity rather than by absence.

A program is rejected wherever such an \(A\) is written, unqualified, in a \(\mathit{ty}\), \(\mathit{parent}\), \(\mathit{createexp}\), or \(\mathit{pattern}\) — before any of the conditions of the rules below that read \(C(A)\) are even checked.

Writing the class in its qualified form always sidesteps the problem. So does renaming the interned unit with as (Section 3.6), provided the renamed intern is itself path-qualified: an alias of a bare, unpathed intern has no qualified spelling to fall back on, and merely renames access to whichever single class that bare name already denotes.

4.3Conformance

The central relation of the static semantics is conformance, written \(\tau \preceq \tau'\) and read “\(\tau\) conforms to \(\tau'\)” or “\(\tau\) is a subtype of \(\tau'\).” A value of a conforming type may be used wherever the wider type is expected.

Conformance is reflexive and transitive, and makes \(\mathsf{Any}\) a top to which every type conforms (rules C-Refl, C-Trans, C-Top in Appendix D).

Its one substantive rule is inheritance: a class type conforms to its parents, with type arguments substituted through the inheritance clause. If \(A\) is declared inherit \(B[\sigma_1,\dots]\) under generic parameters \(\alpha_1,\dots,\alpha_n\), then:

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 binding type-checks because Dog conforms to Animal by (C-Inherit), so a Dog may stand where an Animal is expected; the access a.speak() elaborates to String. (At run time it prints woof: the call dispatches on the object’s actual class, Section 5.4.)

(C-Inherit) makes no distinction between a Nex parent and an imported host interface or class (Section 4.9): the latter is a class type like any other in \(\Sigma\). So a class implementing a host interface conforms to it, and a class extending a host class conforms to that class, exactly as Dog conforms to Animal above.

A value of such a class may therefore be bound to a variable typed by the host interface or class it inherits, whether or not the surrounding code lies within a with "java" block (Section 5.8).

There are exactly five numeric types: \(\texttt{Integer}\), \(\texttt{Real}\), and the three fixed-width integer types \(\texttt{Byte}\), \(\texttt{Integer16}\), and \(\texttt{Integer32}\). (Integer64 is another name for \(\texttt{Integer}\), not a further type.) None of them conforms to another. A widening chain such as \(\texttt{Integer} \preceq \texttt{Real}\) is not assumed here as a conformance — numeric conversions in Nex are explicit, except where the standard environment provides a coercion. The explicit conversions are routines of the classes (to_byte, to_integer16, to_integer32, to_integer, to_real; Appendix B), and each that narrows checks the range of its result.

In particular a numeric constant is never converted to fit its context. The unsuffixed constant 200 has type \(\texttt{Integer}\), which does not conform to \(\texttt{Byte}\), so let b: Byte := 200 is ill-typed; the constant 200u8 has type \(\texttt{Byte}\) (rule 4.1a). Equally, a \(\texttt{Byte}\) is not admitted where an \(\texttt{Integer}\) parameter is declared, nor the reverse. Nor does convert change a number’s type (Section 4.5, Type conversion): two distinct numeric types are related by conformance in neither direction, so a convert from one to another is ill-typed.

The one implicit numeric rule the language relies on belongs to the arithmetic operators, not to conformance. The operands of an arithmetic operator may be of any two numeric types, and the result has the type \(\tau_1 \sqcup \tau_2\) of rule (4.8), where the join of two numeric types is \[ \tau_1 \sqcup \tau_2 \;=\; \begin{cases} \texttt{Real} & \text{if } \tau_1 = \texttt{Real} \text{ or } \tau_2 = \texttt{Real},\\ \texttt{Integer} & \text{otherwise.} \end{cases} \] So an integer operand is admitted where a real is required (\(\texttt{Integer} \sqcup \texttt{Real} = \texttt{Real}\)), and arithmetic on operands of the fixed-width types yields an \(\texttt{Integer}\), never a fixed-width value: \(\texttt{Byte} \sqcup \texttt{Byte} = \texttt{Integer}\). This is recorded with the arithmetic operators in Appendix B, rather than as a conformance.

Optional types

An optional type \(\tau\,?\) is inhabited by the values of \(\tau\) together with nil. Hence \(\tau\) conforms to \(\tau\,?\), and \(\mathsf{Nil}\) conforms to every optional type; but \(\tau\,?\) does not conform to \(\tau\) (rules C-Opt, C-Nil, C-OptMono in Appendix D).

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. Its parameters vary contravariantly and its result covariantly; the unconstrained type \(\mathsf{Fun}\) is a supertype of every function type (rules C-Fun, C-FunTop in Appendix D).

The direction is the crux: for the subtype, each parameter type must be a supertype of the other’s, while the result must be a subtype. So a Function(a: Animal) conforms to a Function(a: Dog) — a handler for any animal may stand in wherever a dog-handler is wanted — but not the reverse.

Refinement types

A refinement type \(R\), declared declare type R = B where n: p (Section 3.5.1), conforms to its base: \(R \preceq B\) (rule C-Refine in Appendix D). Widening is therefore free — an \(R\) flows into any context that expects \(B\).

The reverse direction is not a conformance: a \(B\) does not conform to \(R\), because not every \(B\) satisfies \(p\).

Instead, a base value enters a refinement only at a narrowing site — a binding, parameter, field, or return typed \(R\), or an explicit convert … to. There, elaboration attaches the predicate \(p\) as a contract to be checked at run time (Section 5.6).

The refinement name is not erased during elaboration, so these narrowing sites remain visible to the checker. It is erased only in the value representation, 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 re-checked only if it flows back into a Quantity-typed target.

4.4Elaboration of Expressions

The judgement \(C \vdash e \Rightarrow \tau\) asserts that, in the static environment \(C\), the expression \(e\) is well-typed with type \(\tau\). The rules follow the grammar of Section 2.7.

Constants and variables

A literal takes the type of its scalar class: an integer literal is Integer, a real is Real, and so on for String, Char, and Boolean. nil has the type \(\mathsf{Nil}\), and a variable has whatever type \(C\) records for it (rules 4.1–4.7 in Appendix D).

The auto-declared return variable, result, has the declared return type of the enclosing routine, and is in \(C\) only there (Section 2.9).

The constant this has the type of the current class, available in \(C\) within the body of a routine. The constant super is available there too, with the type of that class’s direct superclass — provided it has exactly one.

A class declaring no inherit clause, or one naming more than one parent (Section 3.2), makes every occurrence of super within it ill-formed. The intended ancestor must then be named explicitly, as in Shape.describe (rule 4.7a in Appendix D).

Writing an ancestor's name explicitly like this — instead of super, or because the current class merely conforms to that ancestor without directly inheriting from it — works as follows.

For routines: the bare name B has its own type in the class environment \(C\) (rule 4.7b). Rule 4.12 then treats B.describe just like a variable of that type: it looks up a routine that B either declares or inherits. So the named ancestor doesn't have to be a direct parent — it just has to be something the current class conforms to.

For constructors: the same explicit form, written before a constructor's name (Shape.make(…)), doesn't create a new object — it delegates to that ancestor's constructor. This isn't rule 4.13 (object creation), but its counterpart, rule 4.13a (constructor delegation), with 5.11a as the matching dynamic rule. One restriction here: B must declare that constructor itself, not just inherit it — a match found further up B's own ancestry doesn't count.

For fields: the same form reaches a field, B.f, the same way rule 4.12 reaches a routine — reading it (via rule 4.11) as B itself would see it, whether B declares or inherits it. This gives you a way to pick out a specific ancestor's copy of a field when repeated inheritance would otherwise create duplicates (see Section 4.9 on ambiguous member resolution and shared ancestors): a plain f can't specify which copy you mean, but B.f can — just as B.describe already disambiguates which copy of an overridden routine runs.

One limit, though: naming an ancestor lets you read through it, but not assign through it. However you write the receiver — f, this.f, super.f, or B.f — assignment is governed by a single rule (4.17a): it only succeeds if the class actually performing the write is the same class that declares the field. So B.f := e still parses as a normal assignment, but only succeeds in the trivial case where B is the class doing the writing. Naming a different ancestor doesn't get you around this.

In short: you can refer to an ancestor by name, but you can't assign to its fields unless you are that class.

Operators

An infix operator denotes a routine of the operand’s class. The arithmetic and comparison operators are elaborated through the signatures recorded in the standard environment; here we just summarise their effect.

For an arithmetic operator \(\odot\) — one of + - * / % ^ — on numeric operands, the result has the type \(\tau_1 \sqcup \tau_2\) of Section 4.3: Real if either operand is, and Integer otherwise. Unary minus on an operand of a fixed-width type likewise yields an Integer. Comparison operators yield Boolean; the ordering operators require operands of the same type, so a Byte is not ordered against an Integer until one of them is converted. The equality operators \(=\), \(/\!=\), \(==\), \(!\!=\) yield Boolean for any operands of conforming type. The logical operators require and yield Boolean.

Formally these are rules 4.8–4.10 of Appendix D, where \(\tau_1 \sqcup \tau_2\) is the join of two numeric types defined in Section 4.3; disjunction and negation are analogous to the conjunction rule.

The claim at the top of this section — that an infix operator denotes a routine of the operand’s class — is meant literally, and a class may make it so for itself. Write \(\mathrm{alias}_\tau(\odot) = m\) when the class \(\tau\), or an ancestor of it, declares a one-argument routine \(m\) bound to \(\odot\) by an alias clause (Section 3.4).

Where the operands of an arithmetic operator are not numeric — so rule 4.8 does not apply — the operator elaborates as the call it abbreviates: the right operand must conform to the parameter of \(m\), and the type of the operator expression is the return type of \(m\). This is rule 4.8a of Appendix D.

The numeric rule is tried first, so an alias can never displace built-in arithmetic. Where neither applies, the expression is ill-typed, as before.

Member access and calls

A member access \(e.f\) requires that the static type of \(e\) be a class type possessing an accessible field or routine named \(f\). If \(f\) is a field, its type is the result; if \(f\) is a nullary routine, its return type is the result; if \(f\) is applied to arguments, the argument types must conform to the parameter types of the routine.

Field access \(e.f\) has the field’s type (rule 4.11 in Appendix D); the call rule is:

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 routine bump takes one Integer and returns one, and the argument 5 conforms; so by (4.12) the call c.bump(5) elaborates to Integer (and evaluates to 5). An argument of the wrong type, or the wrong number of arguments, is rejected here.

The accessibility condition is that \(f\) is not declared in a private feature section of \(A\), unless the access occurs textually within \(A\). A bare call \(m(e_1,\dots,e_n)\) is elaborated as a call on this if \(m\) is a routine of the current class, and otherwise as a call of the free function \(m\) (Section 4.8).

Object creation

The expression create \(A[\bar\tau].k(e_1,\dots,e_n)\) requires that \(A\) be a non-deferred class, that \(k\) be one of its constructors, and that the arguments conform to \(k\)’s parameters; its type is \(A[\bar\tau]\). When the constructor and argument list are omitted, \(A\) must have a constructor taking no arguments, or none at all. The type of the expression is the class type created (rule 4.13 in Appendix D).

A constructor-delegation call — written as \(P.k(e_1,\dots,e_n)\), or super.\(k(e_1,\dots,e_n)\) when rule 4.7a allows super — runs another constructor on the object that's already being built, rather than creating a new object. It can appear anywhere a statement can, but it's most often the first line of a constructor, delegating to its parent's constructor.

It differs from create in two ways:

1. \(P\) must be a proper ancestor. The current class \(A\) must conform to \(P\), but \(P\) can't be \(A\) itself.
2. \(P\) must declare \(k\) directly — not just inherit it. If \(k\) only exists further up \(P\)'s own ancestry chain, that doesn't count. (This is stricter than the ordinary routine-call form, which does accept a match found further up the chain.)

The reason for restriction #2: a constructor's job is to initialise the fields declared alongside it. If you delegated to a constructor two levels removed, you'd skip whatever the intermediate ancestor's constructor was meant to set up for its own fields.

The call itself produces no result and leaves the environment unchanged (rule 4.13a in Appendix D; the corresponding dynamic rule is 5.11a in Section 5.5).

Conditional and anonymous-function expressions

The conditional expression requires a boolean condition and two branches; its type is the join—the least common supertype—of the branch types, written \(\tau_1 \sqcup \tau_2\) and always defined because \(\mathsf{Any}\) is a top. An anonymous function fn… has the function type built from its parameter and result types, its body checked under the parameters (rules 4.14–4.15 in Appendix D).

4.5Elaboration of Statements

Elaborating a statement is a judgement \(C \vdash \mathit{stmt} \Rightarrow C'\): it takes an environment \(C\) and produces a new one, \(C'\), possibly extended with a name the statement binds. A statement that binds nothing just returns \(C\) unchanged.

A block is elaborated by threading the environment through its statements, one after another.

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

In this example, let extends the environment with \(x : \texttt{Integer}\), by rule (4.16). That extended environment is what gets threaded into the if.

Inside the then branch, \(y\) extends it further — but only for that block. It is not visible in the statements after the if.

Assignment requires the value to conform to the variable’s type, and leaves the environment unchanged. The if checks each branch under whatever environment it is given (rules 4.17–4.18 in Appendix D).

Field assignment

A field can be assigned through several spellings: this.f := e', super.f := e', an arbitrary object expression e.f := e', an explicit ancestor name B.f := e', or the bare form f := e' with no receiver written at all. All of these are elaborated by one rule, separate from (4.17), no matter which spelling is used.

That rule makes two demands. First, \(e'\) must conform to \(f\)’s declared type. Second, the assignment must occur textually within the class that declares \(f\) — regardless of the receiver’s static type, what object it denotes at run time, or whether a receiver was written at all (the bare form is just this.f := e' with the receiver token dropped).

So a class may write a field on another instance of its own class (other.f := e', from within a routine of the class that declares \(f\)), but it can never write a field it only inherits — not from a constructor, and not by dropping this. to reach it bare, under any spelling.

One exception: where an enclosing let or parameter binds a name \(f\), rule (4.17) treats it as an ordinary variable instead. That is the only case where a bare assignment to a name shared with a field is governed by something other than this rule.

Inheriting a field gives you no way to write to 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 (4.13a), or call a routine the declaring class exposes for the purpose — the same options any other code outside that class would have.

This is why the derived forms of Appendix C — an enum union’s generated variant constructors, among others — route every such assignment through a routine the parent declares. A plain method dispatches normally and needs no allocation, so it is the ordinary way to expose this without resorting to constructor delegation for a case that is not really about construction at all.

(4.17)’s own once premise applies here exactly as it does there. The corresponding dynamic rule, (5.18) in Section 5.8, carries no restriction of its own: by the time a statically valid program runs, (4.17a) has already ensured every field write in it is one this rule permits.

Self- and mutually recursive closures

Rule (4.16) has one exception, mirroring §4.8’s treatment of free functions. When \(e\) is itself an anonymous function fn…, \(x\) is bound in the environment while \(e\) is elaborated, rather than withheld from it.

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 bound this way can call itself, just as a named function already could under §4.8.

The same widening applies to a run of consecutive closure-literal lets within one block: every name is added to the environment together, before any of the bodies is elaborated. That lets two or more closures call one another regardless of which is written first — the closure-literal version of §4.8’s rule that any function may call any other regardless of textual order. No declare function-style forecast is needed, because the whole run is elaborated 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 widening is withdrawn for any name that is also 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 themselves. In that case, elaboration falls back to the ordinary rule (4.16), under which the name is simply not yet visible.

So a program that relies on self- or mutual reference should give each such closure, and every name it closes over, a name found nowhere else in the enclosing block.

A let with no type annotation takes \(\sigma\) to be the inferred type \(\tau\) of its initialiser.

The premise “\(x\) not a once field outside a constructor” in (4.17) is the static enforcement of immutability: assigning a once field anywhere but in a constructor of its class is rejected.

The loop, case, match, across, and do/rescue statements all elaborate their blocks under the environment extended with whatever variable they introduce — the cursor variable of across, the bound variable of a match clause. Each then produces the original environment back: a block never leaks its locals to the statements that follow it.

Type dispatch and exhaustiveness

A match on an expression of class type \(A\) dispatches on the runtime class. Each clause when \(B\) as \(x\) then \(\mathit{block}\) requires \(B \preceq A\), and elaborates its block with \(x\) bound to \(B\) (rule 4.19 in Appendix D).

A destructuring clause when \(B(\ldots)\) additionally binds each named field of the matched variant in the block, at that field’s declared type. A guard if \(g\) requires \(g\) to elaborate to Boolean, in the scope of those bindings.

When \(A\) is sealed, the clause classes must exhaust \(\mathit{subclasses}(C, A)\), unless an else clause covers the remainder. A missing variant is a compile-time error.

A clause class is identified by the declaration \(C(B)\) it names, not by the spelling \(B\) is written with: naming a variant by its qualified name (Section 4.2.1) covers the same member of \(\mathit{subclasses}(C, A)\) a bare-named clause for it would — never an additional one.

A clause that can fail after its class matches — one carrying a guard, a literal field, or a nested pattern — does not count toward this coverage, since it may fall through. So a variant whose only clause is qualified this way still needs an unguarded 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 form convert \(e\) to \(x{:}\sigma\) is a boolean expression that attempts a downward or upward cast.

It succeeds — binding \(x\) of type \(\sigma\) — when the runtime type of \(e\) is related to \(\sigma\), either as a supertype or a subtype. Otherwise it yields false, with \(x\) bound to nil.

Statically, it requires the type of \(e\) and \(\sigma\) to be related by conformance in one direction or the other. (Distinct numeric types are related in neither direction, Section 4.3, so convert never turns an Integer into a Byte or a Real; the conversion routines do.) The form itself has type Boolean, and binds \(x : \sigma\,?\) (rule 4.20 in Appendix D).

4.6Contract Formation

Every assertion — in a require, an ensure, an invariant, a loop invariant, or an assert — must elaborate to Boolean.

Each kind is elaborated in its own environment. A precondition uses the environment of the routine’s entry (parameters and fields in scope). A postcondition uses that same environment, extended with result and the old forms. An invariant uses the environment of the class’s fields.

An assert is elaborated in whatever environment holds at the point it appears — the environment of an ordinary statement in that body. The bare form, carrying no label, is elaborated exactly as the named one.

This requirement is formalised as rule 4.21 in Appendix D. Its main point is the typing of old, which is admitted only in a postcondition, and whose operand is elaborated over the fields of the current object alone.

Writing \(C^{\mathsf{fields}}\) for the environment holding just those fields — the one an invariant elaborates in — the operand \(e\) may be any expression well-typed there, and old \(e\) carries its type:

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 elaborates because count is a field of the current class, so old count has type Integer by (4.22); the assertion as a whole is Boolean by (4.21). At run time old count is the value held on entry, so after one bump the count is 1 and the postcondition holds.

The operand need not be a bare field: old items.length elaborates 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). Writing old on a parameter, or outside an ensure, is a compile-time error.

Rule (4.22) records the restriction of Section 2.9: beneath old only the fields of the current object are in scope — not the parameters, the locals, or result. And old itself may stand only within a postcondition (the superscript \(\mathsf{ensure}\) marks that environment).

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

4.7Generic Elaboration

A generic class \(A[\alpha_1{\to}K_1,\dots]\) is elaborated once, with its parameters \(\alpha_i\) added to \(\Delta\) and constrained so that any actual argument must conform to \(K_i\).

An application \(A[\tau_1,\dots,\tau_n]\) is well-formed when each \(\tau_i\) conforms to the constraint \(K_i\) of the corresponding parameter. Its fields and routine signatures are those of \(A\), with \(\tau_i\) substituted for \(\alpha_i\) throughout.

A constraint is not merely a gate on the actual argument; it is what the body of the generic may rely on. Within the scope of \(\alpha \to K\), a value of type \(\alpha\) has the features of \(K\): its fields may be read and its routines called, and the call is elaborated against \(K\)’s signature.

A routine deferred in \(K\) may be called on an \(\alpha\) even though no implementation is known statically — the receiver’s dynamic class supplies one (Section 5.5). An unconstrained parameter has no features 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 application Box[Integer] is a well-formed type by (4.23) — the unconstrained parameter G admits any argument — and within it G stands for Integer, so get() returns an Integer. Had G carried a constraint such as [G -> Comparable], the argument would have to conform to it.

A parameter written \(?\alpha\) additionally permits \(\mathsf{Nil}\) as an argument. A generic routine is elaborated the same way, with its type parameters local to the routine.

Because elaboration substitutes rather than erases, the type \(\texttt{Array[Integer]}\) and the type \(\texttt{Array[String]}\) are distinct types with distinct field and routine signatures — a value of one does not conform to the other.

4.8Free Functions and the Static World

The free functions of a program are elaborated together with its classes, so that any function may call any other regardless of textual order. This alone is what admits mutual recursion among them — no forecast of a callee’s signature is needed ahead of its own definition.

A bare application \(m(e_1,\dots,e_n)\), where \(m\) is not a routine of the current class, is elaborated against the signature of the free function \(m\), gathered from wherever in the program \(m\) is defined.

A declare function signature (Section 3.4) is a separate, optional device: it pins \(m\)’s signature explicitly, at the point a reader (or a much later definition) most wants to see it. Its later definition must then match it exactly — a self-check on the declaration, not a precondition for calling \(m\) before that definition is reached.

Free functions, unlike methods, may not be overloaded: each free function name is meant to be unique, and a definition matching an earlier declare function must agree with it in full.

Both rules are enforced: a repeated definition, and a definition whose signature disagrees with its declaration, are each rejected, naming the function.

4.8.1Qualified Calls and Ambiguous References

The collision Section 4.2.1 describes among classes can arise among free functions too: two units interned into the same program may each declare a function under the same bare name.

A bare name \(m\) that no routine of the current class and no function declared directly in the current unit supplies is well-defined only when at most one interned unit declares a free function of that name. When more than one does, \(m\) is an ambiguous reference, and \(m(e_1,\dots,e_n)\) is rejected wherever it is written — before the call rule of Section 4.8 is ever reached.

A function declared directly in the current unit is, like a class, never part of such an ambiguity: it shadows an interned function of the same bare name outright.

Unlike a class, a free function has no qid spelling to fall back on (Section 3.6.2). The escape instead is a qualified call, \(p.m(e_1,\dots,e_n)\), written in the ordinary member-access/call form of Section 2.7 — syntactically the same as a method call on a variable named \(p\).

It is elaborated by this rule, rather than by (4.12), precisely when \(p\)’s leading identifier is undefined in \(\Gamma\) and names no class in \(\Sigma\). An ordinary binding of that name always takes precedence, just as a class declared in the current unit always takes precedence over a same-named interned one (Section 4.2.1).

Only once that binding is confirmed undefined does \(p.m(e_1,\dots,e_n)\) elaborate as a call to the free function whose interned unit path and own name, joined by ., spell \(p.m\). The argument types must conform to that function’s parameters, and the type of the expression is its return type — exactly as for the ordinary call of Section 4.8.

A multi-segment chain (a.b.m(…)) is resolved the same way, against the one dotted name its own .-structure spells: everything before the final, argument-taking step is the unit path. This is unambiguous because the syntax of Section 2.7 allows no other place where a chain's member accesses could split.

4.9Well-Formedness of Classes

Beyond the typing of expressions, a program must satisfy conditions on its class structure. These are checked once, over the whole static world.

• Acyclic inheritance. The relation “\(A\) inherits \(B\)” must be acyclic; its reflexive-transitive closure is the conformance among class types of (C-Inherit).
• Ambiguous member resolution.

  Two parents named in one class’s inherit, or two ancestors reached through them, may themselves share a common ancestor. That can make a member it declares — field, routine, or constructor — reachable by more than one path. This is not itself rejected.

  A bare, unqualified reference to such a member is taken from the copy reached through the first parent named in inherit, tried depth-first through that parent’s own ancestors before the next-named parent is tried at all.

  A member along another path can still be reached deliberately, by naming the ancestor that declares it explicitly (Section 4.4) — a call, for a routine or constructor; a read, for a field. Assignment is the one exception: no explicit-ancestor spelling grants license to write a field it would not already reach (Section 4.4, Field assignment). So a specific path’s copy can only be attached or changed through a routine written on the ancestor that declares it.

  Made precise: for a class \(B\) and a member \(x\) — field, routine, or constructor — \(\mathit{home}(B, x)\) is the path to whichever ancestor actually declares \(x\).

  \[ \mathit{home}(B, x) = \begin{cases} \varepsilon & B \text{ declares } x \text{ directly} \\ P \cdot \mathit{home}(P, x) & \text{otherwise, } P \text{ the first parent of } B \text{ (inherit order) reaching } x \end{cases} \]

  The result is a path of parent names, well-defined because inheritance is acyclic (Acyclic inheritance, above).

  An unqualified reference to \(x\) written in \(B\)’s own text is exactly \(\mathit{home}(B, x)\). An explicit ancestor name \(P\) (or super, which rule 4.7a resolves to a specific \(P\)) instead fixes the first step outright, and continues with \(\mathit{home}(P, x)\) for whatever remains — which is empty, and so contributes nothing further, exactly when \(P\) declares \(x\) directly.

  A related function, \(\mathit{reach}(B, P)\), gives the path to \(B\)’s own nested copy of a named ancestor \(P\) itself (Section 5.3 needs it to evaluate a bare ancestor name as a value): \(\varepsilon\) if \(B = P\), otherwise \(Q \cdot \mathit{reach}(Q, P)\) for the first parent \(Q\) of \(B\) (inherit order) that conforms to \(P\).

• Attachment (void 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 is of an optional type \(\tau\,?\), which admits nil. A constructor that returns with a non-optional reference field still unattached is rejected.

  Scalar fields are attached by their zero value, so need no explicit assignment; optional fields are attached to nil by default. It is this discipline that makes the absence of a rule for nil-dereference (Section 5.3) a guarantee rather than a hazard: a non-optional reference is never observed to be nil.

  “The class’s fields” includes one declared by an ancestor. Inheriting a field carries Attachment’s obligation for it along; it does not exempt it. A subclass cannot discharge that obligation by assigning the field directly, under any spelling — field assignment is confined to the declaring class regardless of receiver (Section 4.4, Field assignment), and inheriting a field is not itself membership in that class.

  The only way a subclass constructor can attach such a field is to delegate to a constructor of the declaring class (4.13a), directly or in turn, or to call a routine the declaring class exposes for the purpose. That is why a class inheriting attachable fields it does not itself redeclare must still route each of its own constructors through one or the other.

• Repeated inheritance and shared ancestors. When a common ancestor reached this way (see Ambiguous member resolution, above) declares a field, the field is not thereby shared: each path to it holds its own copy, attached independently by whichever constructor delegation reaches it along that path (4.13a). A write through one path’s copy is never observed through another’s.
• Conformant overriding.

  When \(A\) inherits \(B\) and redefines a routine \(m\) of \(B\), the signature of \(A\)’s \(m\) must conform to that of \(B\)’s \(m\) under (C-Fun): each parameter may be widened but not narrowed (contravariant), and the return may be narrowed but not widened (covariant). A field of \(B\) may not be redeclared with a non-conforming type.

  This is checked at the override: a routine that narrows a parameter or returns a non-conforming type is rejected there, naming the routine and the offending position.

• Complete deferral. A non-deferred class must supply a body for every routine declared deferred in any of its ancestors; a class with an unimplemented deferred routine is itself deferred and may not be instantiated.
• 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 routine for every member the host type declares without an implementation. That routine is matched by name and parameter count against the host type’s own declaration of it, spelled exactly as the host declares it — no correspondence between Nex’s naming convention and the host’s is assumed.

  This is the host-facing analogue of Complete deferral above, and is checked the same way: a class missing such a routine is rejected, naming the member it fails to supply.

• Single host-class extension.

  At most one parent named in a class’s inherit — counting the whole ancestor chain — may name a concrete (non-interface) host class; a second is rejected.

  A host platform’s object model may permit only single extension of a concrete class, and this condition holds regardless of which platform a given implementation targets.

• Host superclass construction.

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

  The first form must name an argument list the host superclass actually accepts, by argument count. new is reserved for this one purpose when the target is a host superclass; it is otherwise an ordinary identifier (Section 5.8).

• Sealed implies deferred. A sealed class must be deferred. Were a sealed class instantiable, a bare instance of the parent would be a runtime value that an exhaustive match over the parent’s subclasses (4.19) would fail to cover; requiring deferral removes that value and so keeps exhaustiveness meaningful.
• Once discipline. A once field is assigned only in constructors of its class (the premise of (4.17)).

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.