Algebraic structure for numbers with units of measure

Using Coq
1

Dear Coq Enthusiasts,

I want to define a type for “real numbers with unit of measure” so that I can use this type with e.g. the field and lra tactics. The main problem with this is that “numbers with unit of measure” do not form a field because addition applies only to instances with the same unit of measure. E.g. one can multiply “1 m/s” with “1 kg” to get “1 kg*m/s” (the unit of inertia) but one cannot add “1 m/s” and “1 kg”. So the type is not closed under addition. An interesting point though is that terms which are valid always remain valid under field manipulations.

Any thoughts how one could come up with an elegant solution for this? Should I try to hack it to be a field e.g. by using an undefined element (still no so easy) or should I just close it under addition by allowing sums of elements with different type as element of the type - which wouldn’t make any sense - or is there some elegant appropriate algebraic structure for this or can one think of making it a field by some dependent type restrictions on addition?

Thanks for sharing your thoughts!

Best regards,

Michael

1 Like
2

Have you looked at Andrew Kennedy’s formalization of units of measure for the F# language? It basically gives an equational theory of units and a unification algorithm. To me, it seems like a necessary comparison point for any other solution. Kennedy’s 1996 PhD thesis further explores the theory for adding measure types to an ML-like language.

1 Like
3

It sounds like you want to define the notion of… fieldoid? Less speculatively, you can focus on the group structure of addition, recall that groups are one-object categories where all morphisms are invertible, and drop the restriction to one object to get to the notion of groupoid. In this application, each unit of measure is an object of the groupoid, and each value-with-unit (say, 1m/s) is an arrow from that unit to itself, representing the group action of that value. Here, 1m/s is an endomorphism on m/s adding one 1m/s to its argument.
https://ncatlab.org/nlab/show/horizontal+categorification

2 Likes
4

@palmskog, @Blaisorblade : thanks for the pointers, both are very helpful. It took me a while to study the papers by Andrew Kennedy - which give a lot of insight in both the theoretical and practical aspects - as well as to look into groupoids, fieldoids, …

I am still unsure if there is a way to put this into a field so that the field tactic would work on it - I am still thinking about it but I guess probably not. One might have to extend it to fieldoids. But I didn’t conclude on this as yet.

1 Like
5

The best resource on units of measure for PL is likely the old MSR website of Andrew Kennedy: https://web.archive.org/web/20150915212319/http://research.microsoft.com/en-us/um/people/akenn/units/

The Coq wiki states that Andrew was at some point working on formalizing his POPL '97 paper in Coq.