The languages of mathematical physics and modelling are endowed with a rich "grammar of dimensions" that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to explain basic notions of dimensional analysis and Buckingham's Pi theorem. We argue that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modelers and physicists.

翻译：数学物理与建模语言拥有丰富的“量纲语法”，而编程语言的常见抽象无法体现这一语法。我们提出一种依赖类型的领域特定语言（嵌入于Idris中），以捕捉该语法。我们运用该语言解释量纲分析的基本概念以及白金汉Π定理。我们认为，该语言能让计算机科学家更易理解数学物理，同时使建模者与物理学家更易接受函数式编程。