Reading Nex

A.1 Comments, Values, and Names

Comments begin with -- and run to the end of the line. A local variable is introduced with let, given a type after a colon, and assigned with :=. Plain assignment also uses :=. Equality is =, and inequality is /=.

-- a line comment
let total: Integer := 3 + 4          -- declare with a type, assign with :=
let greeting: String := "hello"
total := total + 1                   -- reassignment

Booleans combine with the words and, or, and not; comparisons are the usual <, <=, >, >=.

A.2 Classes: create and feature

A class groups data and behavior. Constructors live under create and are named (there is no single unnamed constructor); fields and methods live under feature. You build an instance with the keyword create followed by the class and constructor name. Inside a method, this refers to the current object, and the return value is assigned to the special name result.

class Counter
  create
    make(start: Integer) do value := start end
  feature
    value: Integer
    increment() do value := value + 1 end
    current(): Integer do result := value end     -- 'result' is the return value
end

let c: Counter := create Counter.make(0)           -- construct with 'create'
c.increment()
let n: Integer := c.current                          -- a no-argument call needs no ()

A method that takes no arguments may be called without parentheses — c.current rather than c.current() — which is why field-like reads in the book often have no trailing ().

A.3 Generics, Arrays, and Maps

Type parameters go in square brackets: class Box[T], and a concrete instance is create Box[Integer].make(...). The two built-in collections the book uses are Array[T] and Map[K, V].

let xs: Array[Integer] := [1, 2, 3]        -- array literal
xs.add(4)                                   -- append
let first: Integer := xs.get(0)             -- read by index
let count: Integer := xs.length             -- size

let prices: Map[String, Integer] := {}      -- empty map
prices.put("apple", 150)
let p: Integer := prices.get("apple")
if prices.contains_key("pear") then ... end

The empty-map literal is {}; a populated one is {"apple": 150, "pear": 120}. Any is the top type every value inherits, used where the book deliberately steps outside static typing (Chapter 9 onward).

A.4 Sum Types: union and match

A sum type — a value that is exactly one of a fixed set of shapes — is written with union: the name of the whole, then one line per shape naming the data that shape carries.

union Shape
  Circle(radius: Real)
  Square(side: Real)
end

This is a closed set: the compiler knows every shape, so it can check that code handles them all. Each variant becomes a distinct type you build by name — create Circle.make(2.0) — and read as ordinary fields. Under the surface union expands to a sealed deferred parent class (a parent that cannot be instantiated and whose subclasses are closed) with one inheriting subclass per shape; you can write that longhand yourself, and the book does so for the one type — the order state — whose variants also carry contracts, which union does not synthesize.

You take a sum type apart with match, which dispatches on the runtime shape. Because Shape is closed, the compiler requires every case to be handled — a missing one is a compile error.

function area(s: Shape): Real
  do
    match s of
      when Circle(radius) then result := 3.14159 * radius * radius   -- destructure the field
      when Square(side) then result := side * side
    end
  end

A when pattern both selects a shape and reads into it: Circle(radius) binds the radius field to a local of the same name. You can rename a field (Circle(radius: r)), ignore one (_), require it to equal a literal, add a Boolean guard that falls through when false (when Circle(radius) if radius > 0 then …), and nest a pattern inside a field. Binding the whole value instead is still available as when Circle as c then … c.radius …. An else branch may cover the rest, but it switches off the exhaustiveness check, so the book uses it sparingly. A non-sealed deferred class is instead an open interface — new subclasses may be added anywhere — which is how the combinator and generic-operation chapters keep their vocabularies extensible.

Two sum types are common enough that the standard library ships them, brought in with intern: Result[T, E] — Ok(value: T) or Err(error: E), for a value or an error — and Option[T] — Some(value: T) or None. Their combinators (result_map, result_and_then, result_map_err, and the option_* pair) let a fallible pipeline be threaded without a match at every step.

A.5 Refinement Types: a Base Type With a Rule

A refinement type is an existing type narrowed by a predicate, declared in one line with declare type … where. It is not a new class and carries no wrapper: at runtime the value is its base type.

declare type Quantity = Integer where n: n > 0        -- a positive integer
declare type Percentage = Real where p: p >= 0.0 and p <= 100.0

The where n: … binds the value under test to n and gives a Boolean rule over it. The rule is checked wherever a plain value is narrowed into the refinement — a typed let, a parameter, a returned value — and never again; a Quantity flows back into any Integer slot for free, because it already is one. So a routine that asks for a Quantity can trust it is positive without re-checking, exactly as with a constrained class but with no .value to unwrap. The check is a contract, and strips out of production builds like every other contract.

A.6 Contracts: the Heart of the Book

Contracts are ordinary syntax in Nex, not a library. There are four forms, and Chapter 2 develops them in full; here is just enough to read them.

• require — a precondition: what the caller must ensure before calling. Each clause has a name.
• ensure — a postcondition: what the routine guarantees on return. old e refers to the value of e on entry.
• invariant — a property of an object that holds before and after every method (written at the end of the class), or a property preserved across a loop.
• variant — an integer that strictly decreases each loop iteration, proving the loop ends.

withdraw(amount: Money)
  require
    positive: amount > Money.zero
    sufficient: amount <= balance
  do
    balance := balance - amount
  ensure
    reduced: balance = old balance - amount
  end

The clause names (positive, sufficient, reduced) are part of the design: a violated contract reports which named promise broke.

A.7 Functions, Loops, and Type Conversion

A free-standing function is written with function. The loop form is from … until … do … end, with optional invariant and variant clauses; the from block initializes, the loop runs until its condition holds. A for-each over a collection is across xs as x do … end.

function sum(xs: Array[Integer]): Integer
  do
    from
      let i: Integer := 0
      result := 0
    invariant
      in_range: 0 <= i and i <= xs.length
    variant
      xs.length - i                     -- proves termination
    until
      i >= xs.length
    do
      result := result + xs.get(i)
      i := i + 1
    end
  end

Finally, convert value to name: Type attempts a runtime downcast: on success name is bound to the converted value, on failure to nil. The book uses it at the points where an open, table-dispatched design has to recover a concrete type the compiler no longer tracks (Chapter 9). A leading ? on a type, as in ?T, marks it detachable — it may hold nil.

That is the whole vocabulary. With it, every listing in the book should read straightforwardly; where a construct does something subtle, the surrounding chapter explains it in place.