Types, equations, dimensions and the Pi theorem

Botta, Nicola; Jansson, Patrik

doi:10.46298/jfp.17762

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Journal Article

Types, equations, dimensions and the Pi theorem

Authors

/persons/resource/nicola.botta

Botta, Nicola
Potsdam Institute for Climate Impact Research;

Jansson, Patrik
External Organizations;

External Resource

https://arxiv.org/abs/2308.09481
(Preprint)

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

34276oa.pdf
(Publisher version), 478KB

Supplementary Material (public)

There is no public supplementary material available

Citation

Botta, N., Jansson, P. (2026): Types, equations, dimensions and the Pi theorem. - Journal of Functional Programming, 36, 3.
https://doi.org/10.46298/jfp.17762

Cite as: https://publications.pik-potsdam.de/pubman/item/item_34276

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.