Sirius

Sirius is a small, imperative, total, polynomially bounded language for pointful array programming.

Having been stung too many times massaging PyTorch tensors, I set off to create a type system that handles tensor shape bookkeeping. In the process, I explored a new part of PL design space and stumbled on an interesting feature set.

It turns out we can avoid runtime shape errors and bounds checks -- without the ergonomic strain of full-blown refinement types like Liquid Haskell -- provided we surrender shape dynamism. In exchange, we reject more bad programs and expose more complete function contracts. The Sirius type system will also unlock a bit of witchcraft in the backend.

I embedded a prototype compiler frontend in this page. Here's a hello world: dot product and matrix multiplication.

# typevars, representing natural numbers, come in curly brackets after function name
# "a.len == b.len" is proven at call sites
fn dot{N}(a: f32[N], b: f32[N]) -> f32:
    let mut sum = 0.0
    for i from 0 to N:
        # i is proven valid index into a and b
        sum += a[i] * b[i]
    return sum

fn matmul{I, J, K}(a: f32[I, J], b: f32[J, K]) -> f32[I, K]:
    for i from 0 to I:
        for k from 0 to K:
            # i is proven valid index into a
            # k valid into b' (b transpose)
            # dot_product requires a[i].len == b'[k].len
            # total yield count is proven I*K
            # yield populates the return array in column-major order
            yield dot(a[i], b'[k])

That program doesn't seem very interesting until you try to change it. The compiler rejects accessing a[i+1] in dot, adding an extra yield in matmul, or modifying any of the typevar constraints in the function signatures. Here are some more examples:

# polynomial expressions in typevars are valid types
# "return.len == A + B" is proven in function body
fn concat{A, B}(a: f32[A], b: f32[B]) -> f32[A + B]:
    yield from a
    yield from b

# N + 1 for typevar N is also valid type
fn push{N}(arr: f32[N], item: f32) -> f32[N + 1]:
    yield from arr
    yield item

fn fill{N}(val: f32) -> f32[N]:
    for i from 0 to N:
        yield val

fn test():
    let x = [1.0, 2.0, 3.0]
    
    # fill(2) must be fill{7}(2)
    let y = concat{3, 7}(x, fill(2))

    # concat(...) must be concat{3, 19}(...) and z must be f32[22]
    let z = concat(x, fill{19}(2))

    # let annotation
    let zeros: f32[5] = fill(0.0)

Signatures provide shape bounds, accesses are statically checked, and yields are statically counted. In short, we're using value-dependent types with built-in polynomial (Poly) refinement. Since the type system is constrained, the annotation burden stays low.^[1]

Why make an imperative array language? In my opinion, the humble C-style for loop has gotten a bad rap. Some problems are easier to solve in an imperative, looping style, with mutable state and transparent locality. Sirius static analysis keeps most of its power and ameliorates the downsides.

That said, I plan to build functional and array-oriented facilities over the imperative core, like map and filter, broadcasting, fancy indexing, and a checked einops primitive integrated like regexes in Perl.

What do polynomials have to do with arrays? For one thing, multidimensional array access desugars to a polynomial.

The desugared expression is a strategy for accessing an element given array coordinates, and it is polynomial in array dimensions. This is a polynomial integer ring, $\mathbb{Z}[x_1,x_2 \dots x_i]$. Add two Polys together, multiply them, or substitute a variable for a new one, and you'll always get a Poly back.

The Sirius type system permits the programmer to freely express array dimensions and accesses in terms of Polys, as long as the resulting system satisfies the constraint solver.^[2]

Now you might object: why can't the programmer write a function that yields an array of super-polynomial size? This is simple in most languages using a while loop or recursion; both are inexpressible in Sirius. Only for-iteration between Poly bounds is permitted.

Dynamic values and shapes cannot mix without blowing up the type system. However, some navigation along their boundary is necessary to write useful programs.

Control flow is dictated by for-loops and if-statements. Loop iterators are fresh typevars with FROM <= N < TO constraints. Facts in if conditions are available to the constraint solver inside their scopes. Every yield is counted symbolically.

# a challenge for the yield counting engine
# inner for-body is invoked N(N-1)/2 times
fn triangle{N}() -> f32[N^2 - N + 1]:
    for i from 0 to N:
        for j from 0 to i:
            yield 0.0
            yield 1.0
    yield 2.0

# some non-linear systems can also be solved
fn nest3d{A, B, C}(arr: f32[A*B*C]) -> f32[A, B, C]:
    for i from 0 to A:
        for j from 0 to B:
            for k from 0 to C:
                yield arr[i*B*C + j*C + k]

Sirius supports Dex-style finite index sets over Polys with Ind.^[3] Inds may pass through function boundaries and skolemize into the Poly algebra via 0 <= Ind(N) < N.

fn find{N}(needle: f32, haystack: f32[N]) -> Ind(N)?:
    for i from 0 to N:
        if needle == haystack[i]:
            # 'Ind(N)' constraint is proven here
            return i
    # Ind(N)? is nullable Ind(N)
    return null

fn test():
    let mut arr = [1.0, 2.0, 3.0]
    let k = find(2.0, arr)
    if k != null:
        # find() constraint is available at call sites
        # so this access is proven safe
        arr[k] += 1.0
        if k > 0:
            # k has a fresh name
            # so this is also proven safe 
            arr[k - 1] = 0.0

The return type of functions like filter cannot be expressed using sizes available at the call site, so Sirius also supports existential sizes. The all-clause constraints are proven at call sites and given in the function body; the ex-clause constraints are proven in the function body and given at call sites.

# read "for all N, there exists a B such that B <= N"
fn filter_greater{all N}{ex B st B <= N}(val: f32, arr: f32[N]) -> f32[B]:
    # the yield counter finds the bounds [0, N) for this loop
    for i from 0 to N:
        if arr[i] > val:
            yield arr[i]

fn find_all{all N}{ex B st B <= N}(needle: f32, haystack: f32[N]) -> Ind(N)[B]:
    for i from 0 to N:
        if needle == haystack[i]:
            yield i

fn test():
    let a = [1.0, 2.0, 3.0, 3.0, 4.0]
    let found = find_all(3.0, a)
    for i from 0 to found.len:
        # proven safe since found[i] has type Ind(5)
        let x = a[found[i]]

What I've described so far is a toy language. It wouldn't be suitable for use in anger, even if it had a fast backend. However, I believe a type system like that of Sirius will transform parallel programming in the coming years.

As I mentioned earlier, this project was borne of my frustration with PyTorch. Zooming out, the GPU is a young technology and it shows in the immaturity of its software ecosystem. The 2026 stack is heavy, fragmented, over-abstracted, and sometimes not even free.

ROCm is closing the gap with CUDA. AI accelerators are shipping novel architectures. CPU core counts are increasing. As single-core performance progress slows, parallelism increases. Programmers need better software to harness this new hardware. We are entering the golden age of array languages. Meanwhile, advanced static analysis will become increasingly fashionable as LLM-assisted programming techniques mature.

I envision a high-level language that leverages types to drastically streamline optimization on highly parallel hardware. With Poly bounds on all memory and compute, the compiler can build tiling, rolling, and fusion strategies -- monomorphizing on shape. Optimizing compilers already try to do this, but they must be conservative in the absence of statically guaranteed constraints.

Sirius, or at least its affine fragment, is polyhedral by construction, using the same familiar Poly abstraction, making it uniquely suited to an MLIR toolchain. The compiler can surface everything from memory layout (perhaps using CuTe-style hierarchical layout algebra^[4]) to runtime complexity, providing detailed performance diagnostics at compile time.

There are several tools that already accomplish many of Sirius's goals. Triton is an ergonomic Python DSL for GPU kernels with a streamlined backend. Futhark is a functional GPGPU language with shape types (index functions) and an algebra including addition. Sirius will continue to draw inspiration from these projects and academic literature as I hammer out the 1.0 roadmap. Ideas and PRs are very welcome at the repo.

[1] Low-ish. Annotation may be lessened in some cases, à la lifetime elision in the Rust borrow checker. I will refrain from any kind of global inference because I mostly agree with Fernando Borretti on the topic. Inference and solving strictly go per-function. []

[2] Solving arbitrary Poly constraints is impossible, courtesy of Matiyasevich et al. For now, I'm sticking with Z3's linear integer arithmetic and a final pass to search for bounded-degree Handelman representations. Although Z3 could safely check more sophisticated constraints, the checker will inevitably return some false negatives. Happily, most constraints are trivial and obtain representationally without invoking Z3 at all. []

[3] The Dex paper (p. 11) remarks, “This captures one of the most common uses for the reshape operation... [while] not requiring the type system to solve systems of Diophantine equations to check which reshapes are valid.” Yeah, but what if we do? []

[4] Cris Cecka exhibited the Tao of Sirius when, asked about compilation time, he said “I make absolutely sure that I never lose track of any static information, ever, because that's the Death of runtime.” []