(About a pre-print by Nicola Botta & Patrik Jansson)

Specialization in the physical sciences has widened the gap between the languages of mathematical physics and those of functional programming (FP). While computer-based modelling critically needs precise specifications, dependently typed languages are not yet well-equipped to encode the "grammar of dimensions" that rules physics (Dimensional Analysis, DA).

In our new pre-print, Types, equations, dimensions and the Pi theorem (arXiv:2308.09481), we take a step toward bridging this gap.

The Grammar of Dimensions

We analyzed dimension functions, physical quantities, and units of measurement through the lens of Programming Languages. Based on this, we propose a small Domain-Specific Language (DSL) in Idris (or Agda). This DSL leverages the host type system to enforce dimensional consistency and assess dimensional dependence and independence.

Formalizing Covariance

Beyond simple unit checking, we formalized the covariance principle: the requirement that physical laws must be independent of the chosen system of units. We define this as a homomorphism between the algebra of physical quantities and the algebra of real numbers.

By proving that elementary arithmetic operations preserve this property, we explain the type-theoretic foundation for dimensionally consistent programming.

A Constructive Pi Theorem

Classically, Buckingham's Pi theorem is formulated non-constructively. In our work, we add a constructive direction.

This allows us to go beyond merely checking existing equations. It enables the definition of functions that fulfil the covariance principle by construction. Consequently, dependently typed languages can support DA-driven program derivation, where the type checker actually assists modellers in identifying valid physical laws from empirical data constraints.

Looking Ahead

We view this work as a contribution toward understanding relativity principles through formalization. While these principles are well understood in engineering and physics, it is unclear how they apply to economics, biology, or climate science. We believe that Type Theory and FP can contribute significantly to answering this question.

Full pre-print: https://arxiv.org/abs/2308.09481

Associated code: PIK-Potsdam GitLab Repository