Linear Types, Symmetric Monoidal Categories, and Tensors
- Authors: Jean-Philippe Bernardy, Arnaud Spiwack
- https://doi.org/10.1145/3462282
- Pre-print on arXiv: https://arxiv.org/abs/2312.02664
Tensor calculus uses a terse but effective language for expressing physical laws. It was instrumental already a century ago in the formulation of Einstein’s general relativity, and its usage has spread to many areas of science. We use category theory, linear types, and algebraic simplifications to implement two tensor DSLs embedded in Haskell, and the conversions between them. We also provide helper functions to view the tensors in Einstein index notation and as diagrams. As an example we express Einstein’s General Relativity equation for the curvature of space-time and verify that the Schwarzschild metric tensor is a solution.
@article{BERNARDY_JANSSON_2025,
title = {Domain-specific tensor languages},
author = {Bernardy, Jean-Philippe and Jansson, Patrik},
journal = {Journal of Functional Programming},
volume = {35},
year = {2025},
pages = {e9},
doi = {10.1017/S0956796825000048}
}