Runtime shape and device errors in tensor code can be costly and tiresome. spidr eliminates these problems.

spidr uses the programming language Idris to catch all potential shape errors before the code is run. For example, the compiler will reject this

append : Tensor [m, n] F64 -> Tensor [m, p] F64 -> Tensor [m, n + p] F64
append x y = concat 0 x y

because we're concatenating along the wrong axis (0 not 1).

spidr's not just well-typed, it's fast. Like JAX, it uses OpenXLA, and runs on CPU, GPU etc. We are already working on vectorization and autodiff, and have plans for distributed computing, including static checks that your tensors are on the right device.