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 formalize basic notions of dimensional analysis: those of dimension function, physical quantity, homomorphic measurement, the covariance principle and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.

翻译：数学物理与建模语言拥有丰富的“维度语法”，而编程语言的常见抽象未能有效表达这一语法。我们提出一种依赖类型的领域特定语言（嵌入于Idris中），用以捕捉这种语法。我们运用它形式化维度分析的基本概念：维度函数、物理量、同态测量、协变性原理以及白金汉Pi定理。我们希望该语言能使数学物理更易于计算机科学家理解，并使函数式编程更易为建模者与物理学家所接受。