SPy: an interpreter and a compiler for a statically typed variant of Python
8 points by shalabh
8 points by shalabh
I always hate when someone lists pro's or con's and then don't provide evidence. For example the top of the readme it literally says:
It consists of:
- an interpreter (so that you can have the usual nice "development experience" that you have in Python)
- a compiler (for speed)
And then nowhere in the readme do we get a compaison of the speed of the compiler against the interpreter. If you say 'for speed' I'd quite like to know what sort of increase we are talking about, single digit percent? double digit? Order of magnitude?
SPy is early in its life so not sure speed benchmarks are that useful at this point. But comparing Python+numpy to SPy, this demo shows roughly 2 orders or magnitude: https://youtu.be/W-8tgZDgYmw?si=SQiUNRvLxdM3kk8D&t=706
I believe the SPy interpreter is slower than Python at this time but the goal is to be roughly the same as Python.
they mention a point in the pipeline where “redshifting” is performed on the AST. does anyone know what redshift means in this context? it seems to be something about specializing generic types, but i can’t say for sure.
It is explained in https://antocuni.eu/2026/03/25/inside-spy-part-2-language-semantics/
They talk about it in terms of partial evaluation, but it’s strongly reminiscent of Zig’s comptime. The red/blue analogy is cute but I’m not sure the @blue annotation for comptime functions is the best spelling they could have chosen.
SPy is another dependently typed language that doesn’t want to get involved in type theory.
The videos have some great examples. For eg at this point in the video it shows how one closure can produce one, two or any number of "red" functions: https://youtu.be/W-8tgZDgYmw?si=t7ODsXlfvuQ8YqpZ&t=1869
This is a powerful way of metaprogramming (the interpreter is fully available at build time) that subsumes generics and various other PL features like macros. As fanf's comment says, I do think it is equivalent to dependently typed languages (maybe more powerful?). But I find this idea quite refreshing and much more approachable. I can follow the code without having to learn complex type system evaluation rules and syntax. The metaprogramming language and runtime language are the same. (Not surprising that I like Zig as well.)
Importantly, people have programmed Python with this style for a long time, it just evaluates everything at runtime.
A really nice property is the type checking happens after redshifting. So it fully checks the "generated program" so to speak and the type system itself is pretty simple.