A Pluggable Type Checker for Representing Kinds of Quantities
摘要
A system of measurement consists of several basic units that represent observable phenomena, and a method for combining them to form compound units. Units provide context to numerical data. In science and engineering, quantities are usually expressed as values paired with units. In software systems, handling these quantities is often the responsibility of the programmer, leading to well-documented failures when not managed correctly. Although numerous tools and libraries exist for validating expressions denoting units of measurement, they do not enable the kind of quantity to be specified. Furthermore, tools that extend the underlying type system of the language limit backwards compatibility, while libraries are both cumbersome and further specialise the code base. In this paper, we address the issue of quantities that, despite having the same units, represent different kinds, such as work and torque. We propose a data type that models compound units using a tree structure instead of a tuple. This structure preserves the compound nature during arithmetic operations, facilitating more thorough static analysis and a comprehensive definition of arithmetic for different kinds of quantities. Finally, we present the system as a lightweight pluggable type checker which integrates smoothly with existing compilers and code bases.