I have done some experiments with type-directed static optimization of geometric algebra, but I didn’t get far enough to find out if it would scale up to real applications. The idea was to represent in the type system which components are known to be zero, so that (for instance) the GA representation of a vector or a rotation is the same size as it would be as a traditional matrix-based linear algebra. And the type system can check that the resulting of an operation is what you expect, eg, two planes intersect in a line. So, similar optimizations to gaigen, but (I hoped) more automatic and less runtime machinery. But as I said, I didn’t get it to work.