Open Manual

<!-- nytrix-doc: {"audience":"user","featured":true,"group":"spec","order":20,"summary":"Values, type annotations, inference, mutability, and the boundaries between static and dynamic data."} -->

Types

Types describe the values a binding, parameter, return value, or container may

hold. Start with the concrete type you expect; use ?T only when absence is a

real result, and use any only at a deliberately dynamic boundary.

Everyday forms

WriteMeaningCommon use
int, str, bool, f64A concrete value type.Bindings and function signatures.
list<T>, dict<K, V>, set<T>A typed collection.Data kept within Nytrix.
?TT or nil.Optional input or lookup result.
T<A>A generic type.Option<int>, Result<T, E>.
struct NameA Nytrix record value.Ordinary program data.
enum NameA finite set of variants.State and alternatives.
layout NameAn ABI-shaped record.FFI and raw memory only.

Pointers (*T), handle, and fnptr are distinct. Use layout for a

record whose field order and representation are part of an ABI; use struct

for an ordinary Nytrix value. Do not use a handle as a pointer unless the

foreign API documents that conversion.

layout Pixel {
   u8 r,
   u8 g,
   u8 b,
   u8 a
}

The full boundary contract-headers, ownership, strings, packing, and

alignment-is in Native.

Proof and refinement types

Fin<N> is the bounded integer type whose values satisfy 0 <= value < N.

N must normalize to a positive compile-time integer. It uses the integer ABI,

so passing a Fin<N> to an int parameter is representation-preserving, but

constructing or passing an integer as Fin<N> requires a proven bound.

fn load_slot(Fin<4> index) int {
   def values = [10, 20, 30, 40]
   values[index]
}

def Fin<4> selected = 2
assert(load_slot(selected) == 30, "bounded index")

Different bounds remain different static types: Fin<4> is not silently

reinterpreted as Fin<8>. Literal and immutable compile-time bounds may be

used in generic specialization keys. The current value-indexed core is

deliberately bounded to Fin<N>; user-defined value-indexed constructors and

dependent result types are not yet accepted.

proof<P> is erased compile-time evidence that proposition P was proved.

It is not a runtime boolean and ordinary values cannot stand in for it.

fn require_positive(proof<5 > 0> evidence) int {
   5
}

def proof positive = prove(5 > 0, "positive constant")
require_positive(positive)

fn lemma declares a named proposition for use with prove. A lemma body is

one proposition and may use A → B implication syntax:

fn lemma positive_sum(int x, int y) {
  x > 0 && y > 0 → x + y > 0
}

def proof sum_is_positive = prove(positive_sum(3, 4))

The application is checked at compile time and the resulting witness is

erased, like any other proof<P> value.

Proposition matching is structural: equivalent equality/order spellings are

normalized, while unrelated propositions are rejected. prove accepts only a

condition the compiler can establish; false and unknown conditions fail.

This is refinement-proof support, not full dependent typing. Some

parameter-dependent propositions cannot yet be resolved through calls, and

proofs do not survive mutation of their referenced values. Unsupported forms

are rejected rather than accepted as evidence. See Comptime for

compile-time assertions and proof construction rules.

Related