Named dimensions
Tensor axes carry semantic names. A batch by feature matrix and a feature by batch matrix are different types, so a wrong multiply fails before it reaches data.
A functional tensor language for model-written code
A language for programs machines write.
Chelis is a statically typed functional language for numerical code that agents can generate and people can audit. Surf stays readable. Deep gives tools a typed program tree. The compiler checks shapes, precision, effects, ownership, and differentiability before anything runs.
hidden = matmul(norm1, ff1) |> relu |> matmul(ff2)
residual = add(norm1, hidden)
out = layer_norm(residual, gamma2, beta2)
outWhy it exists
The author changed.
Python was designed for careful humans writing code directly. Chelis starts from a different workflow: models generate code at high volume, and people supervise the result. That puts the compiler inside the authoring loop.
Every program has a readable surface and a typed machine form. A model can search and rewrite the program as data. A person can review the Surf. The compiler gives structured feedback that both can use.
Type system
Checked before runtime.
Precision
Numeric precision is part of the signature. An f32 path cannot quietly absorb an f64 value and keep going.
Effects
Randomness, device resources, and differentiable regions are visible to the compiler instead of buried in library calls.
Linearity
Values that must be used once are checked that way. In-place reuse and resource movement have a type-level contract.
Surf and Deep
Readable for people. Structured for tools.
Surf is the syntax people read, write, and review. Deep is the canonical typed tree that the compiler and agent tooling manipulate. Surf lowers to Deep and can be decompiled back, so the human view and machine view stay tied to the same program.
This is the practical reason Chelis can serve both adoption paths: humans get a compact functional language, while tools get a program representation they can inspect, mutate, and score.
Numerical computing
The proving ground is real code.
Bundled runtime
chelis-std
Tensor operations and reductions shipped inside the compiler.
Numerics
nautilus
Scientific computing routines implemented in Chelis and composed through the same tensor graph.
Dataframes
coral
Typed tables whose numeric columns participate in tensor and AD workflows.
Math bridge
octant
Mathematical LaTeX lowered into Chelis with provenance back to the source formula.
Install
Download a compiler binary.
Chelis ships prebuilt release archives. Put the compiler on your path, check a program, then build C, HIP, or Metal output for the environment that will run it.
gh release download --repo Chelis-Lang/chelis --pattern '*-linux-x86_64.tar.gz'
tar xzf chelis-*-linux-x86_64.tar.gz
export PATH="$PWD/chelis/bin:$PATH"
chelis check examples/vmap_relu.ch
chelis build examples/vmap_relu.ch --target cResearch
The language has a proof beneath it.
The Lean 4 formalization mechanizes the calculus behind Chelis. The core type-system guarantees rest on machine-checked theorems.
- type soundness well-typed programs do not get stuck
- dimension safety named tensor shapes line up
- effect correctness effects occur only where allowed
- linearity soundness linear values keep their usage discipline
- AD correctness differentiation follows the formal specification