Scientists, engineers, and mathematicians often formulate algorithms using coordinate-independent linear algebra because its tools are composable and harder to misuse. For numerical processing, however, users must translate these ideas into coordinate-dependent array code. Most practitioners do so prematurely because tools such as NumPy lack coordinate-independent representations, while existing languages with such constructs do not model enough linear algebra for the situations where they matter. We propose Grassmann, a small language bridging coordinate-independent linear algebra and coordinate-dependent implementations. It uses dependent types, linear types, and partially (pseudo-)invertible computation to model situations arising in exterior algebra and differential geometry. It targets the linear algebra at a point on a manifold, a prerequisite for many specifications in scientific computing and computer graphics. A language for coordinates lets users move between these representations. We give a denotational semantics assigning meaning without coordinates and an operational semantics translating Grassmann to array code under a choice of coordinates. Our main metatheoretic result shows that operational evaluations agree with the denotational semantics under an arbitrary choice of coordinates. This models how practitioners translate linear algebra for computers and suggests an approach to algorithmic optimization at a high level of abstraction. Our optimized implementation generates code for exterior algebra operations with overheads no more than 10%.

翻译：暂无翻译