Show HN: Sirius – A type system for array programming Developer lorentzj released Sirius, a small imperative, total, polynomially bounded language for pointful array programming, published on GitHub on September 10, 2026. Sirius uses value-dependent types with built-in polynomial PolyDependent ML to statically check array shapes, index bounds, and yield counts, rejecting programs that access a[i+1] in a dot product or add an extra yield in matmul without requiring full refinement types such as Liquid Haskell. The project ships with a live editor embedding a prototype compiler frontend and aims to eliminate runtime shape errors and bounds checks while keeping annotation burden low. September 10, 2026 Sirius https://github.com/lorentzj/sirius is a small, imperative, total https://en.wikipedia.org/wiki/Total functional programming , polynomially bounded language for pointful array programming. Having been stung too many times massaging PyTorch tensors https://docs.pytorch.org/docs/stable/generated/torch.nn.Conv3d.html , 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 https://ucsd-progsys.github.io/liquidhaskell/ -- provided we sharply restrict 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 live editor with 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 requires a i .len == b' k .len total yield count is proven I K yield populates the return array in row-major order yield dot a i , b' k fn test : let arr1 = 1.0, 2.0, 3.0 , 4.0, 5.0, 6.0 let arr2 = 7.0, 8.0 , 9.0, 1.0 , 2.0, 3.0 arr1.shape.1 == arr2.shape.0 is proven annotation is checked let res: f32 2, 2 = matmul arr1, arr2 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 , changing the annotation of res , or modifying any of the typevar constraints in the function signatures. The typechecker is engineered to break comprehensibly. Diagnostics provide trivial disproofs or counterexamples when possible. Here's some more code: 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.0 must be fill{7} 2.0 print concat{3, 7} x, fill 2.0 concat ... must be concat{3, 19} ... print concat x, fill{19} 2.0 let annotation let zeros: f32 5 = fill 0.0 Signatures provide shape bounds, accesses are statically checked, and yield s are statically counted. In short, we're using value-dependent types with built-in polynomial Poly /api/doc/sirius/solver/poly/struct.Poly.html Dependent ML https://dl.acm.org/doi/10.1145/277650.277732 . Since the type system is constrained, the annotation burden stays low. \ 1\ footnote 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. What do polynomials have to do with arrays? For one thing, multidimensional array access desugars to a polynomial. | Array | Access | Desugar | |---|---|---| A N A i deref A + i A N, M A i, j deref A + i M + j A N, M, P A i, j, k deref A + i M P + j P + k A N, M, M deref A + i M^2 + j M + k 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 https://en.wikipedia.org/wiki/Polynomial ring , $\mathbb{Z} x 1,x 2 \dots x i $. Add two Poly s together, multiply them, or substitute a variable for a new one, and you'll always get a Poly back. A N, M + 1 deref A + i M + i + j A N, 2 M deref A + 2 i M + j A 3 i + 2, j + 5 deref A + 3 i M + 2 M + j + 5 The Sirius type system permits the programmer to freely express array dimensions and accesses in terms of Poly s, as long as the resulting system satisfies the constraint solver /api/doc/sirius/solver/index.html . \ 2\ footnote 2 Now you might object: why can't the programmer write a function that yield s 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 /api/doc/sirius/solver/count/struct.Count.html . 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 https://arxiv.org/abs/2104.05372 -style finite index sets over Poly s with Ind . \ 3\ footnote 3 Ind s may pass through function boundaries and skolemize into the Poly algebra via 0 <= Ind N < N . php 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 flow type sheds ? from k 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 print a found i I have argued for imperative array programming, but I plan to build functional and array-oriented facilities over the imperative core, like map and filter, broadcasting, fancy indexing https://numpy.org/doc/stable/user/basics.indexing.html advanced-indexing , and a checked einops https://iclr.cc/virtual/2022/oral/6603 primitive integrated like regexes in Perl. The current scalar types are f32 , f64 , i64 , and bool ; abstracting over numerical types is another motivation for more general parametric polymorphism. The matmul example glossed over the question of array memory layout. The type system will ultimately track that information, perhaps allowing @noalias , @dense , and other obligations in signatures. There is no need for yield to favor row-major ordering; alternate bijective maps could be supported with other yield modes for FFI or layout obligation purposes. The short-circuit ? operator, loop break s, and array slices are near-term design problems. Structs are a simple extension of the existing tuple type. Named tensors https://nlp.seas.harvard.edu/NamedTensor then slot in nicely, where arr.shape becomes a struct rather than a tuple. Sum types and exhaustive pattern matching are table stakes. The Poly algebra may be extended with integer division with quasi-polynomials https://en.wikipedia.org/wiki/Quasi-polynomial , but only at a steep complexity and runtime cost. The Alexis King-esque https://lexi-lambda.github.io/blog/2020/08/13/types-as-axioms-or-playing-god-with-static-types/ construction for strides is arr I J , obviating its main use case anyway. Values should be liftable into Poly -space using, for instance, val % N , allowing implementation of data structures like hashmaps. Since the counting engine can't express sublinear bounds, Sirius should expose builtins like binary search and $\mathcal{O} n \log n $ sort. Some true Poly systems will always elude the constraint solver one example today is the perfect square $A^2 - 2AB + B^2 \geq 0$ , so solver development must be guided by systems from practical code for specific applications. Runtime constraint assert s can offer an escape hatch. What I've described so far is a toy language, an ergonomics experiment more than anything else. It wouldn't be suitable for use in anger even if it had a fast backend. 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 https://developer.nvidia.com/cuda-llvm-compiler . ROCm is closing the performance gap with CUDA as both platforms evolve. AI accelerators are shipping with novel architectures. CPU core counts are rising. As single-core performance progress slows, parallelism increases. Programmers need new tools 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. Sirius has no defined scope yet, but its ambitions lean more towards a kernel DSL than a Mojo https://mojolang.org/ -scale behemoth. 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 shapes and eliding guards. Optimizing compilers already https://godbolt.org/z/6xEz3Pan5 try to do this, but they must be conservative in the absence of statically guaranteed constraints. I'll try not to overclaim here as I am not yet initiated in the dark arts of automatic scheduling https://arxiv.org/abs/1505.07716 . Sirius, or at least its affine fragment, is polyhedral https://dl.acm.org/doi/full/10.1145/3674735 by construction, making it uniquely suited to an MLIR https://mlir.llvm.org/docs/Dialects/Affine/ toolchain. The compiler can surface everything from memory layout perhaps using CuTe https://arxiv.org/abs/2603.02298 -style hierarchical layout algebra