Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types

Takashi Suwa, Atsushi Igarashi

When writing programs involving matrices or tensors in general, it is desirable to rule out the inconsistency of tensor shapes (i.e., the generalization of matrix sizes) before act…