Updates
5/25/2026
PyPie is here! We invite feedback and criticism at hi@pypie.dev.
Type safety for tensor shapes, at compile time
PyPie is powered by a mini, fully functioning, and seasoned dependent type checker.
It's mini, since there's only one universe (e.g. type does not have a type) and no user-defined datatypes. That's probably good enough for writing tensor programs. It's fully functioning in the sense that typing judgements, normalization by evaluation, and bi-directional type checking are up and running. It's seasoned with rank-polymorphism (so people don't need to write map everywhere) and some arithmetic rewriting (so people don't need to prove commutativity).
We have intentionally left out some checks for the time being. For xs[n] as an example, PyPie does not require a proof like n < len(xs), since we'd like to keep authoring as Pythonic as possible.
Tutorial
To help people think in PyPie, we've drafted a hands-on tutorial to build three models: a linear regression model, a CNN, and a transformer. The chapters are written in the style of The Little Learner. (The idea of PyPie came from "What if The Little Learner were typed and Pythonic?")
Optimization and backends
PyPie currently compiles to JAX, which optimizes for fusion, parallelization, etc. PyPie has a few rewrite rules to help JAX recognize special patterns, like dot products and sliding windows.
So, in theory, PyPie is supposed to work on any backend supported by JAX. We have tested Linux with CUDA and Apple Silicon.
AI slop
It turns out that not every PL person is a professional web designer, a VS Code plugin author, or even a good parser writer. So we've offloaded the following components to Codex and Claude.
In the compiler code, we've vibe-coded the syntax translation from Ruff AST to PyPie IR and from PyPie IR to JAX code. They seem to be working under hundreds of (AI-generated) test cases. So we don't have plans to revamp them yet.
This website is made by Codex. We like its aesthetics after a few iterations and will probably keep most of it. One thing we need to change is the ASTs of code snippets. Now Codex has an AST grammar defined in TypeScript and "makes" an AST object out of a piece of Python code. Initially we thought it was funny, but now it has become unmanageable; e.g. it often generates the wrong type annotations. We are now exploring running PyPie in WebAssembly so that the type annotations are generated correctly.
Codex also wrote the VS Code plugin, which seems to be small and harmless.