A tour of the type system
Each stop shows a rule, the code it accepts, and what it prevents.
Every elementwise operand has the same shape
Nothing is stretched to fit. A change of rank is written out with insert, expand, reshape or permute, so the shape in the signature is the shape in the arithmetic.
Side by side
numpy runs and returns the wrong portfolio return Chelis rejects the multiply at chelis check
broadcasting.py numpy 2.4.6
w = np.array([0.2, 0.3, 0.5])
r = np.array([[0.01], [0.02], [0.03]])
(w * r).sum() # 0.06, not 0.0230.060000 intended 0.023000
Three weights times returns shaped 3 by 1 broadcast to a 3 by 3 grid, and its sum comes back as the portfolio return.
broadcast.ch exit 2
def portfolio_return(w: tensor[3, f64], r: tensor[3, 1, f64]) -> tensor[f64] = {
weighted = mul(w, r)
weighted |> sum(0)
}DimensionMismatch: `mul` argument 2: expected rank-1 tensor, got rank-2 tensor --> broadcast.ch:2:14
| 2 | weighted = mul(w, r) | ^^^^^^^^^
With jaxtyping
portfolio_jaxtyping.py jaxtyping 0.3.11 · beartype 0.22.9
import numpy as np
from beartype import beartype
from jaxtyping import Float64, jaxtyped
@jaxtyped(typechecker=beartype)
def portfolio_return(
w: Float64[np.ndarray, "asset"],
r: Float64[np.ndarray, "asset 1"],
) -> float:
return float((w * r).sum())
w = np.array([0.2, 0.3, 0.5])
r = np.array([[0.01], [0.02], [0.03]])
print(portfolio_return(w, r)) # 0.06python portfolio_jaxtyping.py
0.06
jaxtyping and beartype check the arguments at the call. The annotation says r is a column, so the call passes and the multiply inside still broadcasts. Chelis checks every expression in the body too.
The fix
The fix: the returns arrive as a vector of three, and the check passes.
clean.ch check: exit 0
def portfolio_return(w: tensor[3, f64], r: tensor[3, f64]) -> tensor[f64] = {
weighted = mul(w, r)
weighted |> sum(0)
}Precision changes only through cast
Every operand of an arithmetic operation has the same precision, and cast is the one conversion. A wider running sum is written in the call, as an accumulator precision on matmul or sum.
Side by side
numpy quietly widens the result to f64 Chelis rejects the mixed add at chelis check
precision.py numpy 2.4.6
a = np.array([0.1, 0.2, 0.3], np.float32)
b = np.array([1.0, 2.0, 3.0], np.float64)
(a + b).dtype # float64dtype('float64')
Adding an f32 array to an f64 array quietly returns f64.
precision.ch exit 2
def add_mixed(a: tensor[3, f32], b: tensor[3, f64]) -> tensor[3, f64] = add(a, b)PrecisionMismatch: `add` arguments; tensor precision mismatch: f32 vs f64 --> precision.ch:1:73
| 1 | def add_mixed(a: tensor[3, f32], b: tensor[3, f64]) -> tensor[3, f64] = add(a, b) | ^^^^^^^^^
| 1 | ...f64]) -> tensor[3, f64] = add(a, b) | ^^^^^^^^^
= suggestion: Insert explicit cast The fix
The fix: the f32 operand is cast to f64 before the add.
precision_cast.ch check: exit 0
def add_mixed(a: tensor[3, f32], b: tensor[3, f64]) -> tensor[3, f64] = add(cast(a, f64), b)Dimensions match by name
Two named dimensions match when their names match. batch never matches seq, whatever their sizes.
Side by side
numpy with a jaxtyping annotation still accepts the swapped axes Chelis rejects the call at chelis check
axes.py numpy 2.4.6
@jaxtyped(typechecker=beartype)
def score(
x: Float32[np.ndarray, "batch seq"],
) -> Float32[np.ndarray, "batch seq"]:
return np.maximum(x, 0)
# laid out (seq, batch)
y = np.zeros((128, 128), dtype=np.float32)
score(y).shape # (128, 128)(128, 128)
With both sizes at 128, a (seq, batch) array passes a jaxtyping annotation of "batch seq".
axes.ch exit 2
def score(x: tensor[batch, seq, f32]) -> tensor[batch, seq, f32] = relu(x)
def caller(y: tensor[seq, batch, f32]) -> tensor[batch, seq, f32] = score(y)DimensionMismatch: `score` argument 1, axis 0: expected batch, got seq --> axes.ch:2:69
| 2 | def caller(y: tensor[seq, batch, f32]) -> tensor[batch, seq, f32] = score(y) | ^^^^^^^^
| 2 | ...tensor[batch, seq, f32] = score(y) | ^^^^^^^^
The fix
The fix: the caller puts the axes in order with permute.
axes_permute.ch check: exit 0
def score(x: tensor[batch, seq, f32]) -> tensor[batch, seq, f32] = relu(x)
def caller(y: tensor[seq, batch, f32]) -> tensor[batch, seq, f32] = score(permute(y, 1, 0))A negative index stops the program
Lengths, indices, offsets and counts are exact i64. The index is a value, so the check passes this program and the evaluator stops it at the read.
Side by side
Python returns the last price Chelis stops the program at the read
negative_index.py Python 3.12.14
px = [101.0, 102.5, 99.0]
i = 1
px[i - 2] # 99.0, the last element99.0
At i = 1, px[i - 2] counts from the end and returns the last price.
negative_index.ch exit 1
def previous(px: List[f64], i: i64) -> f64 = index(px, (i - 2i64))
def main() -> f64 = previous([101.0f64, 102.5f64, 99.0f64], 1i64)error: index requires non-negative index, got -1
The fix
The fix: the read starts at i = 2, the first index with two prices behind it.
negative_index_start.ch check: exit 0
def previous(px: List[f64], i: i64) -> f64 = index(px, (i - 2i64))
def main() -> f64 = previous([101.0f64, 102.5f64, 99.0f64], 2i64)chelis eval --file negative_index_start.ch
main = 101.0
Random draws take explicit keys
The checker rejects uniform_like without a key. In the corrected program, shock accepts a key parameter and main creates that key from a seed.
Side by side
numpy draws from hidden global state Chelis rejects the draw at chelis check until it gets a key
randomness.py numpy 2.4.6
def shock(px):
noise = np.random.uniform(-0.5, 0.5, 3)
return px + noiserepeated calls return different values
The function draws from the global random state, and nothing in its signature says so.
randomness.ch exit 2
def shock(px: tensor[3, f32]) -> tensor[3, f32] = {
noise = uniform_like(px, -0.5f32, 0.5f32)
add(px, noise)
}ArityMismatch: call `uniform_like`: expected 4 arguments, got 3 arguments; `uniform_like(t, low, high)` is the retired counter-stream spelling: a random draw takes an explicit key first, `uniform_like(k, t, low, high)` (spec/05-risc-primitives.md section 2.7) --> randomness.ch:2:11
| 2 | noise = uniform_like(px, -0.5f32, 0.5f32) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= suggestion: Pass a key first: make one with `key_from_seed(seed)` and derive more with `split_key`, `split_keys` or `fold_in`, as in `uniform_like(k, t, low, high)` The fix
The fix: main passes the key to shock; two captured evaluations return the same tensor.
randomness_seeded.ch check: exit 0
def shock(k: key, px: tensor[3, f32]) -> tensor[3, f32] = {
noise = uniform_like(k, px, -0.5f32, 0.5f32)
add(px, noise)
}
def main() -> tensor[3, f32] = {
px = to_tensor([101.0f32, 102.5f32, 99.0f32])
seed_key = key_from_seed(7i64)
shock(seed_key, px)
}chelis eval --file randomness_seeded.ch
main = tensor(shape=[3], data=[100.62655, 102.8372, 99.17318])
A borrow stays borrowed
A tensor value has one logical owner. &T permits read-only use without transferring that owner. Passing a borrow to an owned parameter requires copy(x). The NumPy snippet demonstrates shared-view mutation; the Chelis snippet demonstrates this ownership check.
Side by side
numpy changes the parent array through the view Chelis rejects a borrow passed to an owned parameter
aliasing.py numpy 2.4.6
m = np.array([[1.0, 2.0],
[3.0, 4.0],
[5.0, 6.0]])
col = m[:, 0]
col *= 2
m[:, 0] # [2., 6., 10.]array([ 2., 6., 10.])
A slice is a view, so doubling the slice doubles the parent's column.
aliasing.ch exit 2
def update(x: tensor[3, f32]) -> tensor[3, f32] = relu(x)
def reader(x: &tensor[3, f32]) -> tensor[3, f32] = update(x)TypeMismatch: type mismatch: tensor[3, f32] vs &tensor[3, f32] --> aliasing.ch:2:52
| 2 | def reader(x: &tensor[3, f32]) -> tensor[3, f32] = update(x) | ^^^^^^^^^
| 2 | ...f32]) -> tensor[3, f32] = update(x) | ^^^^^^^^^
The fix
The fix: reader copies its borrowed input to satisfy update's owned parameter. update computes a new tensor; it does not mutate a view of the caller's tensor.
aliasing_copy.ch check: exit 0
def update(x: tensor[3, f32]) -> tensor[3, f32] = relu(x)
def reader(x: &tensor[3, f32]) -> tensor[3, f32] = update(copy(x))