By Shape, Not by Name: Types and Numbers in Neander

Last time covered failure, in the program and in the envelope. This is the second encore and the last entry in the series, and it takes that closer look at the type system: structural, recursive, and reaching down to integers and decimals of arbitrary precision.

As we saw, every type error in Neander is a Flaw. There is no such thing as a type error at runtime, because by the time a program runs there is no question left about the type of anything in it. The interpreter still has runtime errors to report, division by zero and an index past the end of a list, but none of them are about types.

That is the arrangement the whole type system is built around, and most of what follows is a consequence of it.

The whole type universe

Neander has five base types: string, int, decimal(S, R), bool, and null. There are three composites: records, lists [T], and maps map<V> with string keys. And any type can carry two wrappers: T? for a value that may be absent, and T! for one that may be an error. That is the complete inventory.

Absent are classes, interfaces, inheritance, generics beyond a list's element type and a map's value type, enums, user-defined unions, a void type, and functions as values.

The size of the inventory matters for a reason specific to this language beyond general simplicity. The Reference the runtime hands back on a cold start has to describe all of it in-band, next to the actual task, inside a context window. A type system that needs a book is a type system the agent will read a summary of.

A word on values

Every value in a Neander program is immutable. A list cannot grow, a map cannot take a new entry, a record field cannot be reassigned, and a name cannot be rebound. Values are constructed and then read. The cost of this approach is real: combining two lists means building a third. That is what the spread operator is for, in list and map literals alike, and map { ..defaults, ..overrides } is the shape that motivated it.

The cost is worth paying, and the null rules below are where the return shows up. The type checker also gets to stay small, because it never has to track who else is holding a reference to what.

Shape, not name

Record compatibility in Neander is structural. A record value fits a target record type if it has all the fields the target declares, with compatible types. Extra fields are ignored. The names of the two types are not consulted at all.

types {
  FullOrder {
    id: int
    total: decimal(2, half_away)
    status: string
  }
  OrderSummary {
    id: int
    total: decimal(2, half_away)
  }
}

main -> OrderSummary {
  let o: FullOrder = { id: 1, total: 9.99, status: "new" }
  return o
}

One rule, applied at every boundary where a record meets a target type: let bindings, call parameters, call return values, return, yield, and record field assignment.

Two things follow immediately. The agent declares only the fields it actually intends to use, so a program that needs an order's total does not have to restate the eleven other fields the API returns. And a program does not break when the API adds a twelfth.

The deeper reason is about what an agent can verify. Field shapes come back from discover, and the validator checks the program against the manifest before anything runs, so a wrong shape is caught with a line and a column. A type name the agent invented has no authority behind it whatsoever. Under nominal typing that invented name still has to match something; under structural typing there is no site left where a name has to be right at all. The error class is not reduced, it is deleted. That is a bet about where agent-written code goes wrong, and it is a cheap bet, because nothing is lost if it turns out to be the wrong one.

Recursive by coinduction

A record type may reference itself, directly or through a cycle. During a single compatibility check, encountering the same ordered pair of source and target record types again satisfies that recursive obligation. The check fails only if it finds a concrete mismatch in a field, a wrapper, or a base type.

types {
  Comment {
    id: int
    author: string
    body: string
    replies: [Comment]
  }
  CommentText {
    body: string
    replies: [CommentText]
  }
}

Checking a Comment against CommentText starts with body, which matches, and then reaches replies, which sends the check into Comment against CommentText a second time. That pair is already open, so the obligation is discharged there and the check succeeds. Without the rule it would descend forever, on two types small enough to verify at a glance.

That is a coinductive definition: assume the types are compatible and look for a contradiction, rather than assemble compatibility out of proven parts.

Literals have no names either

Record, list, and map literals are anonymous. No literal names a type. Each one is typed entirely by its context, meaning the declared type at the position where it appears.

let tags: map<string> = map { "env": "prod", "region": "us-east-1" }
let ids: [int] = []
let quote: Quote = { unitPrice: 9.99, inStock: true }

An empty [] or map {} takes its element type from that context too. Because let requires an annotation, and parameters and fields are always typed, every position where a literal can appear has a declared type, so a literal never lacks a context to be typed by.

Names do not appear in compatibility checks, and now they do not appear at construction sites either. A program can be wrong about a type's shape, and the validator will say so precisely. It cannot be wrong about a type's name, because it never writes one.

The types with no shape

Three types complement this design: Namespace, Function, and Document, the handles discovery produces. They are a peer category to records rather than a special kind of record, and they have no program-observable structure at all. A program cannot build one with a literal, read a field off one, or convert one to a string. It can bind one, store it, pass it back to discover, and return it.

So the structural question never arises for them. Their compatibility is by type identity, because there is nothing to match structurally in the first place.

Comparability is a property of types

A type is comparable if it is a base type, a nullable of a comparable type, or a composite whose parts are all comparable. Failable types are not comparable, discovery handles are not comparable, and neither is any composite that transitively contains one. Applying == to those is a type error, caught at validation.

== and != extend structurally to composites. Lists compare element-wise and by length, maps compare by key set and by value, and nullables compare equal when both are null. Map iteration order is not observable, so equality does not consider it. Records compare field-wise, with one condition: both sides must have the same declared record type. That is the one site in the language where a type's identity is consulted, and a mismatch there is a type error rather than a silent false.

What follows is that == never has to do anything at runtime beyond what the validator already proved safe. There is no case where a structural comparison meets a value it does not know how to compare, so there is no silent false for incomparable operands and no runtime error code for the situation.

Manifest types, by name

Program-declared types and manifest-declared types live in separate scopes, bridged structurally at each call site. Sometimes redeclaring is not worth the lines, so a program can name a manifest type directly with a qualified type name: orders.Order references the type exactly as the manifest declares it, with every field, and no types entry of its own.

The naming convention keeps this unambiguous. Type names are PascalCase and everything else is camelCase, so orders.Order and orders.getOrder are told apart by one character, and no parser has to guess whether the second segment is a function or a type.

The hard wall around null

T? and T are strictly separated. A value whose type is string is never null: there is no widening, no cast, and no runtime path that puts a null there.

Conversion runs in one direction only. A T is assignable wherever a T? is expected, which the spec calls nullable widening, and it applies deep: [int] goes where [int?] is expected, and a record with an int field goes where the target's field is int?. That is sound purely because nothing is mutable. Nothing can reach the widened value through the wider view and write a null into it, because nothing can write at all. The reverse direction stays closed. A T? is never assignable to a T without ?? or =?. In particular there is no flow-sensitive type narrowing:

let name: string? = order.customerName

if name is null {
  return "anonymous"
}

// name is still string? here
let display: string = name ?? "anonymous"

Checking a value against null does not change its type in the other branch. Flow-sensitive narrowing is some of the most intricate machinery in the Kotlin and TypeScript compilers, and Neander's entire type checker is a single validation pass. ?? covers the vast majority of null handling in one expression and =? covers the rest.

There is a second argument for that beyond implementation cost. An agent that has to model the checker's flow analysis in order to predict whether its program validates is an agent that will occasionally predict wrong, and it only finds out one submission later.

There is no failable counterpart for widening. A T is not assignable to a T!, nor a T? to a T?!. Failable values originate only from a call, as the last post laid out, and a widening rule that could manufacture a ! would quietly undo that guarantee.

Two axes, one operator

A value can carry both wrappers. T?! is a value that may be an error, and may otherwise be null. The ! always comes last, and T!? is not a type.

Both =? and ?? are target-driven. The declared type of the binding decides which wrappers come off, and the operation is always a single step.

// Order?! to OrderSummary?, in one =?
let maybeSummary: OrderSummary? =? call orders.findMaybe(id: 42)

Two independent things happen in that line. On the union-layer axis, the binding keeps the ? and drops the !, so an error throws out of the enclosing block while a null flows through untouched. On the structural axis, and underneath the ? that survived, Order narrows to OrderSummary by the ordinary structural rule.

The axes compose, and the composition is still one =?. Peeling T?! down to T is one target type that happens to strip both layers, not two operations written in sequence.

Numbers, exactly

The int type is arbitrary-precision. There is no 32-bit or 64-bit variant, no maximum, and no overflow.

Fixed-width integers behave differently across platforms, and they do it silently. In API orchestration an int is an identifier, a count, or a monetary amount in minor units, and silently wrapping any of those does not produce an approximation, it produces a wrong answer that looks like a right one.

The cost objection answers itself. A Neander program spends its time in API calls measured in milliseconds, and a few hundred bignum operations are microseconds.

Scale belongs to the binding

A decimal is an arbitrary-precision finite decimal number, and its declared type carries two things: a scale S, the number of fractional digits, and a rounding mode R.

decimal(2, half_away)    // commercial rounding
decimal(6, half_even)    // banker's rounding
decimal(0, floor)        // integer-like, toward negative infinity

The decision that shapes everything else is that scale and rounding mode attach to the binding, not to the value. Once a value exists, only its mathematical magnitude is part of its identity.

So 1.50 and 1.5000 are the same number, and == says so. The pitfall where two spellings of the same amount compare unequal, familiar from every decimal library that makes scale part of the value, does not exist here, because scale was never in the value to begin with.

Scale and mode are per binding rather than per program because one program legitimately needs several. Commercial rounding on an invoice total, banker's rounding on accrued interest, floor on an amount withheld. Five modes exist: half_away, half_to_zero, half_even, floor, and ceiling.

Arithmetic is exact. + and - produce a result at the larger of the two natural scales, * at the sum of them, and no rounding happens in either case. Mixing scales is always allowed, and intermediate results carry their own natural scale and no rounding mode at all.

Integer division truncates toward zero and is unremarkable. Decimal division is the interesting case. 1.0 / 3.0 has no finite decimal expansion, so the language refuses to divide until it knows where to stop. A decimal / must appear in a position whose target type is a known decimal(S, R): the right-hand side of an annotated let, an argument to a typed parameter, the expression of a return when main returns a decimal, or the value expression of a yield under a map form with a decimal element type. Anywhere else it is a type_error Flaw, with the hint "decimal division requires a target scale; bind the result to a typed decimal(S, R)".

Which is the rule this post opened with, reaching arithmetic. An operation whose result is undefined until someone makes a policy decision is not a runtime condition to detect and report. It is a program the validator declines to run.

Rounding therefore happens in exactly two places: at a decimal /, to the target's scale and mode, and at assignment to a typed binding whose scale is smaller than the value's natural scale. Everywhere else the arithmetic is exact. Cross-implementation determinism is nothing more than that fact, because every rounding step in a valid program has a statically known scale and a statically known mode, and two conforming runtimes have nothing left to disagree about.

let subtotal: decimal(4, half_away) = 29.9900
let taxRate:  decimal(4, half_away) = 0.0725

// exact intermediate at natural scale 8, rounded to 2 at the binding
let tax: decimal(2, half_away) = subtotal * taxRate    // 2.17427500 becomes 2.17

There is no implicit conversion between int and decimal. A numeric literal containing a dot is a decimal literal and its natural scale is the number of digits after the dot; a literal without one is an int; mixing the two in a single arithmetic expression is a type error. toDec() exists to parse a string of unknown provenance or to convert an int value, not to write down a constant. A known constant is written as a literal, so order.total > 1000.00 rather than order.total > toDec("1000", 2, half_away).

One last rule holds the rest together. A decimal leaves in the response envelope as a JSON string, "10.50", never as the JSON number 10.5. The exactness above would be undone at the last step by a parser on the other side that reads numbers into a double.

Grotto's take on numbers

Grotto represents an int as a JavaScript bigint, and a decimal as a bigint coefficient plus a natural scale, where the value is the coefficient times ten to the negative scale. Rounding decisions are made by comparing remainders as integers. No Neander number is ever routed through a JavaScript float, not even in the places where doing so would have been convenient.

The choice reaches the response envelope as well. The platform's JSON serializer refuses a bigint outright, so Grotto writes envelopes with its own, which emits integers as raw digit runs. A forty-digit int arrives with forty digits.

Arbitrary precision has a second consequence, and this one lands on the budget system. Everywhere else in the interpreter, computation cost is a reasonable proxy for memory cost. Work is charged in Thalers, and the values that work produces are bounded by operands that were themselves already paid for. Exact decimal arithmetic breaks that relationship. Squaring a decimal doubles its digit count and costs one Thaler. Do it repeatedly and the Thaler count rises by one per step while the memory rises by a factor of two, which is a program that is computationally trivial and enormous at the same time.

So Grotto charges memory in proportion to digit count rather than a flat cost per value. And for the handful of operations whose result size is named by a scale parameter in the source rather than bounded by their operands, meaning toDec to a large scale, a division with a large target scale, and a rounding step that scales upward, it computes the digit count the coefficient is about to have and checks that against the memory budget before the bignum is built. An over-budget scale raises a cooperative memory Abort instead of allocating first and noticing afterward.

That is a budget check and not a precision cap. There is no maximum scale in the language and none in the runtime. Arbitrary precision stays arbitrary, and the memory budget remains the only ceiling, the same one that binds every other allocation the program makes. Thalers are portable and kilobytes are not, and this is what that distinction looks like once it reaches actual code.

Field Notes from the Grotto

The series started with a runtime and ends with rounding modes, which is roughly the right order. The arguments that decide whether an idea is interesting live at the top, and the ones that decide whether it is usable live at the bottom.

Every entry turned out to be about something that is not there. Neander cannot recurse, cannot loop without a bound, and cannot reach a socket, not because a guard turns the attempt away but because there is no way to write the attempt down. Spending and isolation are the two places where something is genuinely enforced, and they are the smaller half of the story. The type system is the cheapest version of the same move, because none of it costs anything at runtime: a name that never has to match, a null that cannot appear where it was not declared, a division that will not happen until someone has said where to round it.

That is the tour. The series ends here, but there is still time to read the Neander spec, embed Grotto in your own app, and let me know what shape it comes back in.