Foundations

Types & Generics

How Leviathan spells types, and the rules that keep them precise: type expressions and inference markers, primitives that behave like objects, unions with compiler-enforced narrowing, reference vs value semantics, and generics that reach all the way to higher-kinded type parameters.

Type expressions

A type is one of four shapes. var and let are not types at all — they are inference markers, valid only at a declaration site.

TypeName                      // int, string, MyClass
TypeName<T1, T2>              // generic instantiation; nested types allowed,
                               // e.g. Array<Pair<T, U>>
T1 | T2                       // union type
(T1, T2) => R                 // function type

var and let are both pure inference markers: the declared type is whatever the initializer's type is. They differ only in mutability — let is sugar for const var, a single-assignment inferred binding, while var stays freely reassignable. Neither ever appears in a type position beyond the declaration site.

var  count = 0;       // inferred int, freely reassignable
let  name  = "Ada";    // inferred string, single-assignment

count = 1;              // fine
name  = "Grace";         // error: name is const var

Primitives (the object mask)

int, string, bool, float, and char are value types with a method shape: stored unboxed, literals type through them, and methods dispatch through the same member machinery as classes — this inside a primitive method is the raw value. void is the absence of a value; it is only usable as a return type.

int n = -5;
int a = n.abs();          // methods dispatch like any other member

void log(string s) => print(s);   // void only valid as a return type

char

char holds one Unicode scalar (0..0x10FFFF, surrogates excluded), unboxed, default '\0'. Literals are target-typed — a bare 'x' only becomes char when the surrounding context expects one. Comparisons (== != < <= > >=) are by scalar value; there is deliberately no arithmetic on char — use code() instead, which avoids C's integer-promotion pitfalls.

char c    = 'a';
int  code = c.code();     // no c + 1 — go through code()
bool eq   = (c == 'a');

char ships on the oracle, IR, emit-C++, and LLVM engines engines (the LV_CHAR ABI addendum landed 2026-07-10); there is no ELF backend yet.

Unions & optionality

int | string is a closed tagged union. Assignability follows directly: a value of type T is assignable to any union containing T.

int | string id = 42;
id = "abc-123";     // still valid: string is a member of the union

T? is sugar for T | None — None is the unit absence type; there is no null, and a None value is just its union tag with no payload. Optional fields default to None; a general union defaults to its first member's default. None never compares equal to a present value, so absent / present-empty / present-full stay distinguishable.

string? name = None;   // T? is sugar for T | None
name = "Ada";

?? supplies a default when the left side is None, and types as the None-stripped union (the default's type must match). ?. is optional chaining: it short-circuits to None without evaluating its arguments, and types the whole expression as R | None.

string? host = None;
string  h    = host ?? "localhost";   // None-stripped union

User? u    = findUser(id);
int?  len  = u?.name?.length();       // short-circuits to None; args unevaluated

Flow-typing & narrowing

Member access or a call on a union is a compile error until it has been narrowed. x != None / x == None and x is T narrow by flow typing — across if/else branches, while bodies, ternary arms, and through &&. Paths narrow too (req.host != None narrows req.host), but assigning to a path — or its base — invalidates that narrowing. Conditions must be bool; there is no truthiness, and ! negates the narrowed fact.

string? name = load();
if (name != None) {
  print(name.length());   // narrowed to string here
} else {
  print("no name");        // still None here
}

string? s = load();
if (s != None && s.length() > 0) {
  print(s);   // narrowed across &&
}

int | string val = pick();
if (val is string) {
  print(val.length());   // narrowed to string
}

Reference vs value semantics

Objects are references: assignment and parameter passing share the same instance. Primitives and arrays are values (arrays are pure — see Collections & Iteration).

class Box { public int v; }

Box a = new Box();
a.v = 1;
Box b = a;        // b aliases a — same instance
b.v = 2;
print(a.v);         // 2 — the write is shared

Array<int> xs = [1, 2, 3];
Array<int> ys = xs;   // arrays are values — no shared mutable state

Mutation control is one general rule, not three special cases: three orthogonal axes, each already principled.

The slot axis has three points, distinguished by when the fixed value becomes known: var — never fixed; const — fixed at compile time (a local/global/param/for-in initializer may be any runtime expression, but a field's const initializer must be a compile-time constant); readonly — fixed at construction time (instance fields only, written by the initializer or any declaring-class constructor, exactly once).

var count      = 0;      // never fixed — reassignable at any time
const int max  = 100;    // fixed at compile time

class Widget {
  public readonly string id;   // fixed once, at construction time

  new(string id) { this.id = id; }
}

Generics

Any scope-opening entity may declare type parameters: class C<T>, R f<R>(R x), and methods U m<U>(...). Inference tries, in order: constructor or call argument types (including through containers — Array<U> unifies with Array<int>), then the target type of the enclosing initializer or return. An explicit Name<T1,...> is always available. Generics are invariant; the raw form (Array) is compatible with any instantiation of the same head.

class Box<T> {
  public T value;
  new(T value) { this.value = value; }
}
var b = new Box(42);          // T inferred as int from the constructor argument

R first<R>(Array<R> xs) => xs[0];
var x = first([1, 2, 3]);      // R inferred as int

Array<int> ai = [1, 2, 3];
Array raw      = ai;             // raw Array is compatible with any instantiation

Singleton scopes — namespaces and class static sides — may use type parameters in member signatures (bound per call), but may not declare state typed by them.

Higher-kinded types

A type parameter may itself be a type constructor — F of kind * -> * — applied as F<A>. Inference binds the constructor head by unification: F<A> against Array<int> binds F = Array, A = int, and the head flows into the return type, so container-preserving generic functions type precisely.

F<B> mapIt<F, A, B>(F<A> c, (A) => B fn) => c.map(fn);

Array<int> doubled = mapIt([1, 2, 3], (n) => n * 2);   // F=Array preserved

Bodies are duck-typed at instantiation, like C++ templates: c.map(fn) is checked leniently and resolved at the call site. When a result type argument can't be bound — for example from an opaque lambda — the result is the raw head, which is compatible with any instantiation.

T::member

Inside a generic callable body, the left operand of :: may be one of that callable's ordinary (*-kinded) type parameters. T::member is checked duck-style at the definition and resolved separately for every concrete instantiation; labeled constructors, immediately-called members, and callable members used as function values all follow the same rule.

A decode<A>(A witness, int n) => A::FromInt(n);

The compiler emits one deduplicated concrete body per whole-program type tuple, so the operation has the same runtime cost as an equivalent hand-written concrete function. If an instantiating type lacks the selected member, the compile error names the concrete type and points to both the T::member use and the call that instantiated it.

specialization depth

bounded at 32

eligible parameters

T:: is permitted only for callable-level, *-kinded type parameters — a class-level type parameter is rejected, since raw generic-class widening erases the tuple needed to select a copy

overrides

a generic instance method using T:: is supported only when it neither overrides nor is overridden; override-dispatched specialization is deferred