Types, equations, dimensions and the Pi theorem

TL;DR

This paper introduces a dependently typed language embedded in Idris to formalize the grammar of dimensions in physics, enabling precise modeling of dimensional analysis and Buckingham's Pi theorem.

Contribution

It presents a novel dependently typed domain-specific language that captures the grammar of dimensions in mathematical physics, formalizing key concepts and theorems.

Findings

Formalization of dimensional analysis concepts

Implementation of Buckingham's Pi theorem in the language

Enhanced accessibility for physicists and computer scientists

Abstract

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.