A Nex program is more than a block of statements. It is a collection of classes—each bundling data, behaviour, and the contracts that govern them—together with free functions, module links, and the top-level statements that set the whole in motion. This chapter gives the grammar of that larger structure.
3.1Programs and Compilation Units
A program is a sequence of top-level items: import and intern declarations, class declarations, union declarations, function declarations and definitions, type declarations, and statements.
| program | ::= | topitem* | |
| topitem | ::= | import | intern | — module links |
| | | classdec | — class declaration | |
| | | uniondec | — union declaration | |
| | | fundec | funsig | — function definition / declaration | |
| | | tydec | — type alias / refinement | |
| | | stmt | — top-level statement |
Although the items may be written in any order, they do not all take effect at once. The grammar’s order is not the order of execution.
The declarations — classes, functions, and type aliases — constitute the static world of the program. They are elaborated first, as a whole, so that they may refer to one another regardless of textual position.
The top-level statements constitute the dynamic world. They are executed afterwards, in source order, against the static world so established. This separation is made precise in Chapter 7.
3.2Class Declarations
A class declaration introduces a class: a named family of objects sharing a set of features and obeying a set of invariants.
| classdec | ::= | ⟨sealed⟩ ⟨deferred⟩ class id ⟨gen⟩ |
| ⟨note⟩ ⟨inherit⟩ | ||
| classbody | ||
| ⟨invariant⟩ end | ||
| inherit | ::= | inherit parent (, parent)* |
| parent | ::= | qid ⟨tyargs⟩ |
| classbody | ::= | (featuresec | createsec)* |
| invariant | ::= | invariant assertion+ |
| note | ::= | note string |
The two modifiers control instantiation and extension. A
deferred class may not be instantiated; it serves as an interface
or partial implementation, to be completed by its heirs. A sealed
class closes its hierarchy: only classes declared in the same program may
inherit from it, and so the complete set of its descendants is known statically.
A sealed class must also be deferred (Section 4.9), which is why the two
modifiers so often appear together.
A parent named in inherit is ordinarily another class declared in the program, but it need not be. The grammar admits no distinction, so an identifier naming an imported class from the host platform (Section 3.6), rather than a Nex class, is a parent like any other — subject to the further conditions of Section 4.9 and Section 5.8.
A parent may also be named by its qualified name (Section 3.6.1). This matters only when the bare name would otherwise be ambiguous between two interned classes.
3.2.1Generic Parameters
A class or routine may be parameterised by one or more type variables, given
in square brackets after the name. A parameter may carry a single constraint,
written with ->, naming a class that any actual type argument must
conform to; and it may be marked with a leading ? to admit
nil as an argument.
| gen | ::= | [ genparam (, genparam)* ] | |
| genparam | ::= | ⟨?⟩ id ⟨-> id⟩ | — name, optional constraint |
| tyargs | ::= | [ ty (, ty)* ] |
Generics are ordinary types, not a notational convenience layered over an untyped core; their elaboration is given in Section 4.7.
3.2.2Union Declarations
A union declaration introduces a closed set of data variants under a common type. It is a concise notation for a sealed hierarchy: the value of a union type is exactly one of its named variants, each of which may carry a list of named fields.
| uniondec | ::= | ⟨enum⟩ union id ⟨gen⟩ ⟨note⟩ variant+ end | |
| variant | ::= | id ⟨( paramlist )⟩ | — tag and optional named payload |
A union declaration is a derived form: it abbreviates declarations
that could be written by hand. A declaration union P⟨gen⟩
with variants V1…Vn
elaborates to a sealed deferred class P, together with one class
Vi inherit P for each variant. Each such
class's fields are the variant’s payload, and its sole constructor
make takes one parameter per field, in declaration order, and
assigns it. The exact translation is given in Appendix C.
Because the elaboration produces ordinary sealed classes, construction
(create V.make(…)), generic arguments, matching, and the
exhaustiveness guarantee of Section 4.4 all apply to a union with no
further rules.
The union word is a soft keyword: it introduces a
declaration only in top-level position, and remains usable as a built-in member name (as
in the union method of a set).
union Order
Draft
Placed(id: String, total: Real)
Shipped(tracking: String, at: Date)
end
A union names data only: it synthesises no methods, invariants, or
contracts on its variants. A variant that needs a constructor precondition, an
invariant, or per-variant behaviour is written in the explicit
sealed deferred class form of Section 3.2, which the union form
does not replace.
When every variant is payload-free and P is non-generic,
the declaration may be prefixed with the reserved word enum, making it
an enumeration: a closed set of named, ordered, canonical values.
The enum form still elaborates to the sealed hierarchy above,
but with three additions: the parent becomes Comparable,
ordered by declaration order; each member is exposed as an interned class
constant on the type (P.Vi, one canonical value per
variant); and P.values is an array of all members in order. The
full translation is in Appendix C.
Because the enrichment occupies the names ordinal,
compare, and values, no variant may re-declare
them. A plain union is not enriched like the enum.
enum union Color
Red
Green
Blue
end
3.3Features
The body of a class is a sequence of feature sections and
creation sections. A feature section introduces fields and routines; it
may be marked private, in which case its members are accessible
only from within the class.
| featuresec | ::= | ⟨private⟩ feature member+ | |
| member | ::= | field | constant | method | |
| field | ::= | ⟨once⟩ id : ty ⟨note⟩ | |
| constant | ::= | id ⟨: ty⟩ = exp ⟨note⟩ | — class constant |
A field declares an attribute of every instance. A field carries no
initialiser: in a freshly created object, a scalar field holds its zero value
and an optional field holds nil. Every constructor must assign
each non-optional reference field before it returns (Sections 4.9
and 5.5). A field marked once may be assigned within a
constructor but never afterwards; an attempt to assign it elsewhere is
rejected statically (Section 4.4).
A constant, written with = rather than the
assignment symbol :=, does not declare an attribute. It names a
value belonging to the class itself, fixed when the class is elaborated and
immutable thereafter — an assignment to it is rejected statically.
Within the class text a constant is referred to by its bare name, like a
field; outside, it is accessed on the class, C.x, never on an
instance. When the type annotation is omitted, the type is inferred from the
initialising expression.
The initialising expression is unrestricted: besides a scalar, it may be
an object (create …) or a collection literal. The
constant is fixed once, when the class is elaborated, so such a value is
evaluated a single time and shared by every use. An object- or
collection-valued constant is therefore one canonical value:
C.x == C.x holds.
An initialiser may name an earlier constant of the same class, or one inherited from a parent. A forward or cyclic reference among constants is rejected statically.
3.4Routines and Contracts
A routine is a method, a constructor, or a free function. All three share one anatomy: an optional parameter list, an optional return type, an optional precondition, a body, an optional postcondition, and an optional rescue clause.
| method | ::= | id ⟨( ⟨params⟩ )⟩ ⟨: ty⟩ ⟨alias⟩ ⟨note⟩ | |
| ⟨require⟩ do block ⟨ensure⟩ ⟨rescue⟩ end | |||
| | | id ( ⟨params⟩ ) ⟨: ty⟩ ⟨alias⟩ ⟨note⟩ ⟨deferred⟩ | — deferred signature | |
| alias | ::= | alias opsym | — binds an operator to this routine |
| opsym | ::= | "+" | "-" | "*" | "/" | "%" | "^" | — a closed set |
| createsec | ::= | create constructor+ | |
| constructor | ::= | id ⟨( ⟨params⟩ )⟩ ⟨require⟩ do block ⟨ensure⟩ ⟨rescue⟩ end | |
| fundec | ::= | function id ⟨gen⟩ ( ⟨params⟩ ) ⟨: ty⟩ ⟨note⟩ | |
| ⟨require⟩ do block ⟨ensure⟩ ⟨rescue⟩ end | |||
| funsig | ::= | declare function id ⟨gen⟩ ( ⟨params⟩ ) ⟨: ty⟩ ⟨note⟩ | |
| params | ::= | param (, param)* | |
| param | ::= | id (, id)* ⟨: ty⟩ | — several names may share one type |
| require | ::= | require assertion+ | |
| ensure | ::= | ensure assertion+ | |
| rescue | ::= | rescue block | |
| assertion | ::= | id : exp | — a named boolean condition |
An assertion is a named boolean expression. The name has no
effect on meaning; it is the label by which a violation is reported. The same
form was already introduced in Section 2.8 as the operand of the
assert statement, which checks a condition at an arbitrary point
within a body (there, a bare, unnamed expression is allowed too).
Here it appears in three further positions. A require clause
states a precondition: an obligation on the caller, checked on
entry. An ensure clause states a postcondition: a
guarantee to the caller, checked on exit. A class invariant
states a condition every instance must satisfy whenever it is observable
from outside (Section 5.6). Together, these three are Nex’s
realisation of Design by Contract.
Within a postcondition, the form old e denotes the value that
e had when the routine was entered, letting a guarantee relate
the final state to the initial one, as in
money = old money - amount. The operand may be a bare field or
an expression over the fields — old items.length is the
length the collection had on entry — but nothing outside the
object’s fields is in scope beneath old
(Section 2.9).
A routine that declares a return type delivers its result through the
cell result, whose value when the body finishes is the value of
the call.
A one-argument routine may bind itself to an arithmetic operator with an
alias clause. The operator is then exactly sugar for
the call: a - b is a.minus(b), so the
routine’s precondition and postcondition hold at the operator the same
way they do for an explicit call. This is what makes the example above,
money = old money - amount, meaningful for a user-defined
class, just like for the built-in numbers.
class Money
feature
once amount: Integer
once currency: String
minus(other: Money): Money
alias "-"
require
same_currency: currency = other.currency
do
result := create Money.make(amount - other.amount, currency)
end
create
make(a: Integer, c: String) do amount := a currency := c end
end
Three restrictions keep the notation closed:
- The set of aliasable operators is fixed —
+ - * / % ^and no others — so no program can introduce a symbol a reader has never met. - Only arithmetic may be aliased. Ordering is obtained by inheriting
Comparableand definingcompare, and value equality by definingequals(Section 5.3), not by aliasing. - An alias is consulted only where the operands are not already numeric
(or, for
+, a string), so no class can alter the meaning of+onIntegerorReal.
An alias is inherited: a routine aliased in a deferred class gives the operator to every heir, dispatching to the heir’s implementation.
The word alias is contextual, not reserved (Section 2.1): it
has this meaning only in the position shown, and a program may still name a field,
parameter, or routine alias.
method above — a signature followed
by deferred and no do…end
— declares a routine whose implementation is supplied by heirs. It
may appear only in a deferred class. The declare function form
plays the analogous role for free functions: it announces a signature whose
definition follows later. Mutual recursion among free functions needs no
such announcement, since every function in a program is elaborated against
every other’s signature regardless of textual order
(Section 4.8); declare function instead pins a signature
explicitly where a reader wants to see it early, and checks the later
definition against it exactly.
3.5Type Expressions
A type expression denotes a type. The built-in scalar types and
Function are reserved names; a class name, bare or qualified
(Section 3.6.1) and possibly applied to type arguments, denotes the
corresponding class type; a leading ? forms the optional
type that additionally admits nil.
| ty | ::= | Integer | Real | |
| | | Char | Boolean | String | ||
| | | qid ⟨tyargs⟩ | — class type, possibly generic, bare or qualified (Section 3.6.1) | |
| | | ? ty | — optional (nilable) type | |
| | | funty | — function type | |
| funty | ::= | Function ⟨( ⟨funtyparams⟩ ) ⟨: ty⟩⟩ | |
| funtyparams | ::= | funtyparam (, funtyparam)* | |
| funtyparam | ::= | id : ty | ty | — named or positional |
| tydec | ::= | declare type id = ty ⟨refine⟩ | — type alias or refinement |
| refine | ::= | where id : exp | — binder and predicate |
The bare type Function, written without a signature, is the
unconstrained function type, compatible with any function value. A
declare type declaration binds a name to a type expression; the name
is thereafter interchangeable with that expression. Type aliases are most often
used to name a function signature, but any type may be aliased, as in
declare type Matrix = Array[Array[Real]].
3.5.1Refinement Types
When a declare type carries a where clause, it
declares not an alias but a refinement type: the named base type
narrowed by a predicate. The clause where n: e binds the value under
test to n and gives a boolean expression e that every
value of the refinement must satisfy.
declare type Quantity = Integer where n: n > 0
declare type Percentage = Real where p: p >= 0.0 and p <= 100.0
A refinement is not a class: it carries no fields, no constructor, and no
boxing. A value of the refinement is a value of the base type —
the refinement is a checked brand erased to the base representation. So a
Quantity may be used wherever an Integer is wanted,
and arithmetic on it yields the base type.
The predicate is a contract: it is checked where a base value is
narrowed into the refinement, and elided under
skip-contracts like any other contract. The subtyping rule
(narrowing checked, widening free) is given in Section 4.3, and the
placement and evaluation of the check in Section 5.6.
where is contextual (Section 2.1): it is recognised as
the refinement clause only immediately after declare type id =
ty, and remains available everywhere else as the name of a variable,
field, parameter, or routine. This differs from union
(Section 3.2.2), which is contextual only as a built-in member name.
3.6Modules
Nex keeps its core grammar small and pushes growth into libraries. Two declarations connect a program to code outside it.
An intern declaration loads another Nex source unit,
identified by a slash-separated path, optionally renaming it with
as. The named unit’s declarations become available to the
current program.
An import declaration brings in a class from the host platform — as of now, only the Java virtual machine — named by a dotted path and an optional source string.
| intern | ::= | intern id (/ id)* ⟨as id⟩ |
| import | ::= | import id (. id)* ⟨from string⟩ |
The intern mechanism is what allows the vocabulary of Nex to grow
without the grammar growing: new operations and conveniences live in library
units loaded by intern, not in new keywords. The meaning of these
declarations—which is, in essence, the elaboration of the named unit in the
current environment—is given in Chapter 7.
3.6.1Qualified Names and Ambiguous References
The path segments preceding the class name in an intern
declaration are not merely a means of locating a file. Taken together with
the class’s own name, they form its qualified name: a
second, always-unambiguous spelling by which the class may be named wherever
a bare class name may — a parent (Section 3.2), a
class ty (Section 3.5), a createexp
(Appendix A.5), or a pattern (Section 2.8).
We write qid for a class name in either spelling:
| qid | ::= | id (/ id)* | — bare (zero segments) or path-qualified |
Every ty, parent, createexp, and
pattern production that named a bare class id in
earlier sections in fact names a qid; those sections write
id for readability where no unit interns a colliding name, which
is the ordinary case.
Two source units, interned into the same program, may each declare a class under the same bare name — nothing in the grammar of either unit, read on its own, can detect this. Section 4.2 gives the resulting static rule: a bare class name that denotes more than one class, once both units are elaborated together, is an ambiguous reference, rejected wherever it is written unqualified in the program that interned both.
Writing the class in its qualified form resolves the reference
unambiguously, regardless of how many other units also declare a class of
that bare name. So does giving one of the colliding interns a local name
with as, provided the renamed intern is itself
path-qualified. (An as on 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.)
A class declared directly in the current unit is never part of such an ambiguity: it shadows an interned class of the same bare name outright, the same way a local variable shadows a global (Section 7.4).
An imported class is not confined to the role of a value manufactured and
called. It may also be named in a class declaration’s
inherit clause (Section 3.2), so that a Nex class
implements a host interface or extends a host class. The conditions this
places on the inheriting class are given in Section 4.9; the dispatch
semantics that follow from it are given in Section 5.4, and the
constructor-forwarding semantics in Section 5.5.
3.6.2Qualified Calls to Free Functions
A unit’s free functions are carried into the current program by
intern exactly as its classes are: the declaration loads the
whole named unit, not merely the one name written after its path, so a
function sharing a file with the interned class arrives alongside it under
its own bare name.
A free function has no qid spelling and no
path-qualified as: as renames a class only, never
a function (Section 3.6). Two units interned into the same program may
nonetheless each declare a function under the same bare name. A bare
application of that name is then an ambiguous reference,
rejected wherever it is written. Section 4.8.1 gives the static rule,
which mirrors 3.6.1’s class rule in substance but not in form: there is
no qid to fall back on directly at the syntax
level.
The escape from such a collision is instead a qualified
call: path.m(e1,…,en),
written in the ordinary member-access/call form of the expression grammar
(Section 2.7) — syntactically indistinguishable from a real
method call on a variable named path.
It is elaborated as naming the free function whose unit path and own
name, joined by ., spell path.m, but only when
path’s leading identifier has no ordinary binding at that
point in the program. An existing local, parameter, field, or class of that
name always takes precedence; the qualified reading is tried only once
ordinary elaboration of the leading name has already failed
(Section 4.8.1).
This differs from a class’s qid in spelling
because it must. qid separates path segments with
/, which works there only because a ty,
parent, createexp, and pattern are
never exp positions — so / never has to be
told apart from the division operator (Section 2.6). A function call is
an exp, though, and division is written there too. So a
qualified call instead reuses ., already the member-access
operator, resolved by this special case of elaboration rather than by a new
grammar production.
3.7Syntactic Restrictions
- A
sealedclass must also bedeferred(Section 4.9 explains why this is required rather than merely advised). - A field declared
oncemust give an explicit type; the inferred-type form offieldmay not be markedonce. - A deferred routine signature, and the
declare functionform, may not carryrequire,ensure, or a body. - A class may not inherit from itself, directly or through a cycle of parents; the inheritance relation must be a partial order (Section 4.5).
- The body of a constructor named in a
createsection may assign theoncefields of its class; no other routine may. - A later
functiondefinition must match its earlierdeclare functionsignature exactly in name, generic parameters, parameter types, and return type. - Free function names are intended to be unique: a free function, unlike a method, may not be overloaded by arity. A second definition of a name is rejected rather than silently superseding the earlier one.