Types

Nexus uses a strict type system with Hindley-Milner inference, structural records, algebraic data types, and linear types for resource tracking.

Primitive Types

Type	Description
i32	32-bit signed integer
i64	64-bit signed integer
f32	32-bit floating-point
f64	64-bit floating-point
float	Alias of f64
bool	Boolean (true / false)
char	Single Unicode character ('a', '\n', '\x41', '\u{1F600}')
string	Immutable UTF-8 string
unit	The unit type, written () as a value

Numeric literals default to i64 (integers) and f64 (floats) unless constrained by type annotations.

Compound Types

Records

Structural record types. Defined with type or used inline:

export type User = { id: i64, name: string }



let u = { id: 1, name: "Alice" }

ADTs (Sum Types)

Algebraic data types with labeled constructor arguments:

export type Result<T, E> = Ok(val: T) | Err(err: E)

export type Option<T> = Some(val: T) | None

Opaque Types

The opaque modifier hides constructors from importers. The type name is visible but construction and pattern matching are only possible inside the defining module:

export opaque type Set = Set(id: i64)

Importers see Set as a type but cannot use Set(id: ...) to construct or destructure it. The module must provide functions for creation and access.

Lists

Immutable singly-linked lists:

let xs: [i64] = [1, 2, 3]

Lists cannot contain mutable references.

Arrays

Linear mutable arrays. Arrays are inherently linear to ensure unique ownership:

let %arr: [| i64 |] = [| 1, 2, 3 |]

%arr[0] <- 42

let val = (&%arr)[0]

Arrays cannot contain mutable references.

Generics

User-defined types can be parameterized:

export type Pair<A, B> = Pair(left: A, right: B)

Linear Types (%)

Linear types make resource lifecycle visible in syntax (see Design). The % sigil marks a binding that must be consumed exactly once.

Rules

Rule	Enforcement
Must consume exactly once	Compile error if unused or used twice
Cannot discard with _	Wildcard on composite linear value is rejected
Branch consistency	All branches must consume the same linear bindings
Closure capture	Capturing %x makes the closure itself linear
No mutable ref	~ binding cannot hold a linear type

Primitive Auto-Drop

Primitive linear values (i64, f64, bool, string, unit) are automatically released at scope end. Using % on primitives is valid but unnecessary.

Composite Consumption

Composite linear values (records, ADTs, arrays) must be explicitly consumed via:

• Function call (passing the linear binding as an argument)
• Pattern matching (destructuring extracts the value)
• Return (propagating ownership to the caller)

Linearity Weakening

A plain T value can be passed to a function expecting %T. The value is treated as linear for the duration of the call.

Linear Closures

If a closure captures a linear binding, the closure itself becomes linear and can only be invoked once:

let %resource = acquire()

let f = fn () -> unit do

  consume(r: %resource)

  return ()

end

f()  // ok -- consumes the closure

f()  // error -- closure already consumed

Borrowing (&)

The & sigil creates an immutable, non-consuming view of a value (see Design).

Syntax

& works both as a prefix operator and as a let-binding sigil:

let borrowed = &arr  // prefix operator on immutable binding

let &b = ~x          // let-binding sigil

let b2 = &%resource  // prefix operator on linear binding

Coercion

&T coerces to T for reading. The original binding remains live and unconsumed.

Patterns

Borrow patterns bind without consuming:

  // x is &i64, original not consumed

  return ()



fn peek(x: &i64) -> unit do

Properties

• Multiple borrows of the same binding are allowed simultaneously
• Borrow lifetime is tied to the scope of the source binding
• Borrowing a linear value does not consume it

Mutable References (~)

The ~ sigil creates a stack-confined mutable binding:

let ~count = 0

~count <- ~count + 1

Gravity Rule

Mutable references cannot escape the defining function:

• Cannot be returned from functions
• Cannot be stored in heap-allocated structures (records, ADTs, lists)
• Cannot be captured by closures or concurrent tasks

This ensures mutation remains localized and predictable.

Restrictions

• Cannot hold linear types (~ on %T is forbidden)
• Cannot be captured by lambdas
• Cannot cross conc task boundaries

Sigil Compatibility Matrix

Operation	Immutable	~ Mutable	% Linear	& Borrow
Read	yes	yes	yes (consumes)	yes
Assign (<-)	no	yes	no	no
Pass to function	yes (copy)	yes (copy)	yes (move)	yes (view)
Return from function	yes	no	yes	no
Store in record/ADT	yes	no	yes	yes
Capture in closure	yes	no	yes (makes closure linear)	yes
Borrow with &	yes	yes	yes	yes
Discard with _	yes	yes	no (composites)	yes

Function Types

Functions are first-class values with labeled parameters and optional throws/coeffect annotations:

(label: T) -> R                                 // pure function

(a: i64, b: i64) -> i64                         // multiple params

() -> unit throws { Exn }                       // with throws

() -> string require { Net }                    // with coeffect

(x: T) -> R require { C | r } throws { E | e }  // open rows

Closures

Lambdas capture immutable bindings from their lexical scope:

let f = fn (x: i64) -> i64 do

  return x + 1

end

Closure constraints:

• Cannot capture mutable (~) bindings
• Capturing a linear (%) binding makes the closure linear
• A recursive local lambda requires an immutable let binding with an explicit type annotation

Row Types

Effect and coeffect annotations use row types:

{ Exn }          // single entry

{ Net, Fs }      // multiple entries

{ Console | e }  // open row with tail variable

Empty row (omitted or {}) means no effects/requirements.