Type system reference

Chelis records tensor shape and element dtype in types. It does not implicitly broadcast tensors or promote numeric operands. Dimension names preserve axis identity: distinct names do not unify, while a literal extent can satisfy a named dimension at a call site.

Primitive types

The numeric primitive types are:

Type	Meaning
f32	32-bit float
f64	64-bit float
bf16	bfloat16
f16	IEEE 754 binary16
i8	8-bit signed integer
i16	16-bit signed integer
i32	32-bit signed integer
i64	64-bit signed integer

There are no unsigned integer types. The other primitive types are bool, string, and key; unit is the unit type and () its value. Strings support host work and cannot be tensor elements.

key is the non-numeric type of a random key: key_from_seed(42i64) makes one, and tensor[n, key] holds n of them. A key has no arithmetic and no cast, and each key is used at most once on every path; see Effects.

Tensor types

A tensor type is written tensor[dimensions..., element_type]: the last entry is the element type and each earlier entry is a dimension. Supported elements include numeric types, bool, and key, but each operation has its own element type rules. A tensor with no dimensions is a rank-zero tensor, such as tensor[f32].

tensor[f32]                 -- scalar
tensor[n, f32]              -- one named dimension
tensor[batch, seq, f32]     -- two named dimensions
tensor[64, 64, f32]         -- two literal dimensions
tensor[batch, bool]         -- boolean elements
tensor[batch, key]          -- random keys

A dimension position holds one of five forms. This signature uses all of them; chelis deep prints the Deep node for each:

def f[n, r](a: tensor[n, f32], b: tensor[batch, 4, f32], c: tensor[*, f32], d: tensor[..r, f32]) -> tensor[n, f32] = a

Surf	Deep	Meaning
n, listed in [...]	(d-var {} n)	A dimension variable. Each call binds it to the caller's extent.
batch, not listed in [...]	(d-name {} batch)	A named dimension. It needs no declaration; it matches the same name or a literal extent.
4	(d-lit {} 4)	A literal extent.
*	(d-name {} *)	The wildcard: an extent not known statically.
..r, with r listed in [...]	(d-rank {} r)	A spread: a run of dimensions in a rank-polymorphic signature.

Named dimensions and polymorphism

Dimension lists match in order. batch does not unify with seq, and two different literal extents do not unify. A named dimension can unify with a literal extent at a call site; the literal supplies a concrete size, while the name remains available in the function's type. A dimension variable unifies with a compatible dimension and binds.

A function generic over shape uses dimension variables. There are no explicit dimension arguments; call sites instantiate the variables by unification.

def transpose[a, b](x: tensor[a, b, f32]) -> tensor[b, a, f32] = permute(x, 1, 0)

Declared dimension parameters are rigid inside the function body: the body must type-check for every instantiation, so it cannot couple a result dimension to an unrelated input dimension.

A wildcard dimension * marks a size that is not statically known, for example an axis produced by a concat whose length depends on runtime data. It can unify with another dimension but is never generalized. A declared result dimension can restore a named shape claim, with a runtime equality check when the size cannot be proved statically.

A rank spread carries an ordered row of dimensions. A rank-polymorphic function can call another checked helper. The checker must establish that the helper's complete body preserves those names under the call's uniquely determined row relation.

The helper keeps its dtype bounds, effects, and ownership requirements. A matching function signature alone supplies no body evidence. Local or computed callable values cannot borrow evidence from a declaration with the same spelling. See the helper composition example.

Dtype bounds

A binder in the [...] clause may carry a dtype bound, which restricts every dtype it can be instantiated at. A bound is written either as a family name or as an explicit dtype set.

The families are Float (the four floating dtypes), Int (the four signed integer dtypes), and Numeric (their union). bool and string belong to no family.

def add_ints[p: Int](x: p, y: p) -> p = add(x, y)
def add_floats[p: Float](x: p, y: p) -> p = add(x, y)
def add_wide[p: {f32, f64}](x: p, y: p) -> p = add(x, y)

An explicit set admits exactly the dtypes it lists. A family can admit new members if the language adds dtypes; an explicit set stays fixed. Use a set to exclude a member a family would admit. A bound's literals must be valid at every admissible instantiation. Under p: Float, cast(1000000.0, p) is rejected, because Float admits f16 and the literal rounds to infinity there; under p: {f32, f64} the same literal is fine.

A one-member bound is written {f64}. There is no bare-dtype spelling: p: f64 is a syntax error, because a binder restricted to one dtype is a set of one rather than a type ascription. The formatter prints a set's members in the order the active dtype set declares them, not the order you wrote them.

Calling add_ints at f32, or add_floats at i32, is a PrecisionMismatch naming the required family. The bound is part of the function's type, not a check on the callee name, so it survives aliases, wrappers, higher-order values, and imports. Two bounded variables that unify keep the intersection of their families; Float and Int share nothing, so identifying one with the other is an error.

A binder with no dtype-family bound can stand for a general type, subject to the other type rules. In particular, a function's generic type parameter cannot be instantiated with a key-carrying type: pass key or tensor[n, key] through an explicitly typed parameter instead. Put a dtype-family bound on a declaration's sig when it has one, or on its def otherwise, never both.

Rank polymorphism

A rank variable ..r is a name-preserving spread over a run of dimensions, so one definition covers tensors of every rank. Its name is listed in the declaration's complete binder list; a spread name may not repeat in a single shape.

def relu_any_rank[r](x: &tensor[..r, f32]) -> tensor[..r, f32] = relu(x)

Spreads can surround named axes, letting a definition reduce or insert an axis while preserving the others. To reduce a named seq axis:

def reduce_seq[pre, post](x: &tensor[..pre, seq, ..post, f32]) -> tensor[..pre, ..post, f32] = sum(x, seq)

Rank-polymorphic bodies admit operations whose shape effect can be tracked by name, including elementwise operations, named-axis reductions such as sum and count, and named-axis insert. Named-axis insert requires a compile-time constant i64 size. Positional rewriters such as permute, reshape, and matmul are rejected inside a ..r body.

No broadcasting

Chelis does not broadcast. Operands of an elementwise operation must have identical dimension lists. Use insert to add a dimension explicitly before combining tensors of different rank, and expand to broadcast an existing size-1 axis.

def add_bias(x: tensor[2, 3, f32], bias: tensor[3, f32]) -> tensor[2, 3, f32] = add(x, insert(bias, 0i32, 2i64))

Calling add(x, bias) directly is a dimension mismatch. insert adds the leading axis explicitly; expand, reshape, and permute provide other explicit shape changes.

Precision rules

Precision never changes implicitly. Both operands of an arithmetic operation must have the same precision; the compiler never inserts a cast for you.

-- add(tensor[d, f32], tensor[d, bf16]) is a type error.
result = add(x, cast(y, f32))

cast(e, p) explicitly converts a scalar or tensor to the named dtype; a tensor keeps its dimensions. Casts can cross numeric kinds and can target bool. An integer-to-float cast may round. A float-to-integer cast is checked: it requires a finite, integral value in the target's range, and cast(2.5f32, i32) stops evaluation with numeric trap: domain in cast at i32.

To narrow on purpose, use one of three named conversions. Each takes a scalar or a tensor (cast_x(source, target)), keeps the tensor's dimensions, has a signed-integer target, and is not differentiable: grad rejects a path through it.

Conversion	Source	Finite value	NaN	Infinity
cast_trunc(x, T)	float	Truncates toward zero; a result outside T traps overflow.	Traps domain.	Traps domain.
cast_saturate(x, T)	float or signed integer	Truncates a float toward zero, then clamps to T's minimum and maximum.	Traps domain.	Returns T's minimum or maximum.
cast_wrap(x, T)	signed integer	Keeps the low bits: the result is congruent to x modulo 2^width(T).	Not applicable.	Not applicable.

xs = to_tensor([-2.7, 2.7, 300.5], f32)
truncated = cast_trunc(xs, i16)
saturated = cast_saturate(xs, i8)
wrapped = cast_wrap(300i32, i8)
checked = cast(2.0f32, i32)

xs = tensor(shape=[3], data=[-2.7, 2.7, 300.5])
truncated = tensor(shape=[3], data=[-2, 2, 300])
saturated = tensor(shape=[3], data=[-2, 2, 127])
wrapped = 44
checked = 2

300 wraps to 300 - 256 = 44 in i8. There is no rounding conversion: write cast(round(x), T), where round rounds half to even and the cast checks the result.

Ordinary integer literals default to i32 and float literals to f32. These constructs state a dtype directly:

1. A suffix binds a literal to its stated dtype.
2. A binding or function result with a declared numeric type states the dtype of its literal initializer or body. A declared tensor type states the dtype of literal elements in the bracket literal that makes it a tensor.
3. A direct cast binds an unsuffixed literal operand at a numeric target its kind admits; a cast to a primitive target then denotes the literal itself. A float literal admits float targets, while an integer literal admits any numeric target.
4. A dtype argument in to_tensor([1.1, 2.2], f64) states the dtype of the bracket literal's numeric elements.

A bracket literal is a List. It becomes a tensor through to_tensor or where its own binding or function result declares a tensor type. No default applies to numeric literal elements inside to_tensor: write a dtype argument or suffix every numeric literal element. to_tensor([1.1, 2.2]) is rejected; to_tensor([1.1, 2.2], f64) and to_tensor([1.1f64, 2.2f64]) are accepted. This applies recursively to nested bracket literals and to negative literals.

A dtype argument never converts an already-typed element. A named list such as xs = [1.1, 2.2] has f32 elements, and to_tensor(xs) keeps that dtype; to_tensor(xs, f64) is a type error. Use cast(to_tensor(xs), f64) to widen those values. A tensor parameter or a cast never converts a bracket literal to a tensor. A list literal and a bare scalar passed to an ordinary function do not adopt a callee's dtype. Structural lists such as reshape sizes therefore spell their i64 elements explicitly.

For an empty list, its declared element type or a dtype argument determines the result dtype: to_tensor([], f64) has shape [0] and dtype f64. An unconstrained to_tensor([]) is rejected. to_tensor is reserved and cannot be rebound in any scope, including by parameters or imports.

-- explicit tensor conversion
a = cast(x, bf16)
-- suffix binds f64
b = 1.0f64
-- suffix binds i64; cast(3000000000, i64) binds the same literal the same way
c = 3000000000i64
-- the cast is the literal `1.1f64`, never `1.1f32` widened
d = cast(1.1, f64)
-- the dtype argument binds the elements at f64
e = to_tensor([1.1, 2.2], f64)

Arithmetic operands must have the same numeric dtype and dimensions, with each operation's own dtype domain. Ordered comparisons such as cmplt take equal numeric types; eq and neq also compare booleans, strings, unit, and two List, tuple, Dict, Option, or data-type values of one type, structurally, when no part of the value is a function, key, or resource handle. Tensor comparisons produce a boolean tensor. Logical operations (and, or, not) take bool; transcendental operations such as exp, log, and sqrt take float types.

matmul, sum, and einsum accept an optional final argument accumulator=p, as in sum(x, 0i32, accumulator=f64); any other call that supplies it is a type error. Omitted, the compiler resolves the default from the operand dtype. For bf16 and f16, the default accumulator is f32; their result returns to the operand dtype. sum and einsum default to i32 accumulation and an i32 result for i8 and i16 inputs; integer matmul is rejected. For f32 and signed integer reductions, an explicitly wider permitted accumulator also widens the result. The requested accumulator must have the same numeric kind and be no narrower than either the operands or their default.

Small-integer sums widen to i32, because a total of N values needs more bits than its elements. Stored i8 and i16 tensors stay i8 and i16; only the aggregate an operation returns widens:

Operation	What it sums	Result for an i8 or i16 operand	Result for any other operand
sum	the selected axes	i32	the operand dtype
cumsum	every prefix along the axis	i32	the operand dtype
trace	the selected diagonal	i32	the operand dtype
einsum	every contracted label	i32	the operand dtype

A declared result, or a downstream operation, that expects the operand dtype is a type error that names this rule. Declare the result as i32, or narrow it explicitly with cast(total, i8), which traps Overflow when the total does not fit. sum and einsum also take accumulator=i64 for an i64 total. A function generic over a precision variable must bound it to dtypes that share one result, such as Float, {i32, i64}, or {i8, i16} with an i32 result.

Function types

A function type can be written A -> B -> C: A and B are the two argument types, and C is the return type. Calls still supply both arguments together as f(a, b); the arrow chain does not make a function implicitly curried. Parenthesize an argument that is itself a function type.

tensor[n, f32] -> tensor[n, f32] -> tensor[f32]   -- two args, scalar result
(tensor[n, f32] -> tensor[f32]) -> tensor[f32]    -- a function-typed argument

Aggregate types

• Tuples: (f32, f32) as a type, (a, b) as a value, projected with .0, .1.
• Algebraic data types: type Option[a] = | None | Some(a) has a positional payload, and type Shape = | Circle { radius: f32 } | Square { side: f32 } has record-field payloads. Recursive types refer to themselves by name.
• Records: constructed with Foo { x: e1, y: e2 } (punning allowed), read with e.field.
• Type aliases: a type without variants is transparent and expanded at desugaring.
• Lists: List[T] holds elements of one type; a list of tensors fixes one rank for every element. The list builtins are below.
• Dictionaries: Dict[K, V] maps keys of one type K (string, bool, or a signed integer; float keys are a type error) to values of one type V. Build one from a list of pairs with dict_of; a later pair wins over an earlier one with the same key. dict_get(d, k) returns Option[V], and dict_insert, dict_remove, and dict_merge (right side wins) return a new Dict. dict_contains, dict_keys, dict_values, dict_entries, and len read it.

vocab: Dict[string, i64] = dict_of([("alpha", 1i64), ("beta", 2i64)])
extended = dict_insert(vocab, "gamma", 3i64)
beta_id = dict_get(extended, "beta")
missing = dict_get(extended, "delta")

vocab = dict(alpha: 1, beta: 2)
extended = dict(alpha: 1, beta: 2, gamma: 3)
beta_id = Some(2)
missing = None

List builtins

Counts and indices are i64, and indices start at zero.

Builtin	Signature	Result and failure
len(xs)	List[T] -> i64 (also takes a Dict)	Number of elements.
index(xs, i)	List[T], i64 -> T	Element i. A negative or out-of-range i stops evaluation (index 9 out of bounds for list of len 5).
append(xs, x)	List[T], T -> List[T]	xs with x at the end.
concat(xs, ys)	List[T], List[T] -> List[T]	xs followed by ys. With an i32 axis as the second argument, concat is the tensor operation instead.
take(xs, n), skip(xs, n)	List[T], i64 -> List[T]	The first n elements, or all but the first n. A count above the length takes everything or leaves nothing; a negative count stops evaluation.
chunk(xs, n)	List[T], i64 -> List[List[T]]	Consecutive groups of n; the last may be shorter. n must be positive.
range(start, end)	i64, i64 -> List[i64]	start up to but excluding end; empty when end <= start.
map(f, xs)	(T -> U), List[T] -> List[U]	f applied to each element in order.
filter(f, xs)	(T -> bool), List[T] -> List[T]	Elements where f is true, in order. partition(f, xs) returns the kept and rejected lists.
fold(f, init, xs)	((A, T) -> A), A, List[T] -> A	The final accumulator.
scan(f, init, xs)	((A, T) -> A), A, List[T] -> List[A]	The accumulator after each element, not including init.
flat_map(f, xs), flatten(xss)	(T -> List[U]), List[T] -> List[U]; List[List[T]] -> List[T]	Results joined in order; one level of nesting removed.
zip(xs, ys)	List[T], List[U] -> List[(T, U)]	Pairs, stopping at the shorter list.
enumerate(xs)	List[T] -> List[(i64, T)]	Each element with its index.

A callback runs once per element in order, and an effect it carries (such as IO) becomes an effect of the call.

xs = range(1i64, 6i64)
doubled = map(fn (x) -> (x * 2i64), xs)
evens = filter(fn (x) -> ((floor_div(x, 2i64) * 2i64) == x), xs)
total = fold(fn (acc, x) -> (acc + x), 0i64, xs)
running = scan(fn (acc, x) -> (acc + x), 0i64, xs)
head = take(xs, 2i64)
rest = skip(xs, 2i64)
groups = chunk(xs, 2i64)
third = index(xs, 2i64)
size = len(xs)

xs = [1, 2, 3, 4, 5]
doubled = [2, 4, 6, 8, 10]
evens = [2, 4]
total = 15
running = [1, 3, 6, 10, 15]
head = [1, 2]
rest = [3, 4, 5]
groups = [[1, 2], [3, 4], [5]]
third = 3
size = 5

A top-level definition cannot reuse a builtin's name: count = len(xs) is rejected because count is the boolean-count reduction.

Effects in types

A function type can declare an effect set. In Surf, write it as ! { ... } on a sig or def; an omitted clause leaves effects inferred, while ! {} declares a pure upper bound.

sig report[n]: tensor[n, f32] -> unit ! { IO }

Effect inference runs after type inference. Host operations such as print and file reads contribute IO. Random draws take a key and contribute no effect. with device(...) introduces a resource region checked against the build target. See Effects for the effect vocabulary.

Linearity and borrowing

Tensor values are owned by default. A call with an owned parameter consumes its argument; read-only calls can borrow it. If an owned tensor feeds several consuming calls, the compiler inserts copies for the earlier uses, so this checks and evaluates with no copy:

def total[n](x: tensor[n, f32]) -> tensor[f32] = sum(x, 0i32)
x = to_tensor([1.0, 2.0], f32)
a = total(x)
b = total(x)

Write copy(x) yourself on the earlier use in these cases, where no copy is inserted and the later use fails chelis check with a UseAfterConsume error that names the earlier call:

• the later use is a call through a transform, such as grad(total)(x) after total(x);
• x is a component bound by a destructuring let, such as (a, b) = ...;
• x carries a random key, which can never be copied;
• the earlier use was drop(x), a match on x, or a closure that consumes x.

The linear regression example passes copies to loss for the first reason. An explicit drop(x) ends access through that owner. The compiler also drops an unused owner after its last use when it can establish that point. Keys are different: a key-carrying value can be used at most once on a path and cannot be copied or borrowed.

A read-only borrow is a reference type, written &T in a signature and &x at a use site. A borrow leaves the owned binding live and is the idiomatic way to pass a tensor to a read-only operation.

def relu_forward[r](x: &tensor[..r, f32]) -> tensor[..r, f32] = relu(x)

Passing an owned value where a borrow is expected auto-borrows. Passing a borrow where an owned value is expected is an error unless you write copy(x) for a copyable value. Borrows cannot be stored in aggregates, returned, or captured by closures. The borrow target must be a tensor or a tensor-carrying value, including tuples or data types with tensor fields.

Inference

The checker infers many types and checks annotations you supply. A generic declaration must still list its type, dimension, dtype, or rank binders in [...]. A cast names its target dtype; a literal outside its default dtype range needs a suffix or direct cast; and a claimed dimension may need an annotation and a runtime equality check.

The pipeline order is parse, desugar, type inference and checking, effect inference and checking, linearity checking, then lowering.