Types, equations, dimensions and the Pi theorem
This work addresses the gap in programming language abstractions for dimensional analysis, potentially benefiting computer scientists and physicists, though it appears incremental as it builds on existing type theory and domain-specific language techniques.
The authors tackled the problem of representing dimensional analysis in programming languages by creating a dependently typed domain-specific language embedded in Idris, which formalizes concepts like dimension functions and Buckingham's Pi theorem. The result is a language that aims to make mathematical physics more accessible to computer scientists and functional programming more appealing to physicists.
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.