A Type System with Physical Units Checked Using Bidirectional Type Inference

Abstract

Physical units are essential to scientific and engineering models. They give meaning to quantities such as time, mass, and frequency, and valid results depend on combining them consistently. However, most programming languages do not enforce unit correctness; units are often treated as informal annotations or external checks. As a result, subtle but serious errors can appear in code when mathematical models are implemented. For instance, a program may mistakenly add a distance to a time variable or mix quantities measured in incompatible frames of reference. Such invalid operations are physically meaningless, yet they are often accepted silently by compilers. Previous type systems for checking physical units have mainly relied on unification, a method that often produces long and confusing error messages. This thesis introduces a type system based on bidirectional type checking. Unlike unification-based systems which attempt to infer all types globally, our approach requires explicit type annotations for function declarations. This design choice transforms the global constraint-solving problem into a series of local verification tasks, resulting in clearer and more localized feedback. This approach makes type errors easier to understand while preserving formal correctness. The system extends ordinary dimensional analysis by distinguishing scalars, vectors, affine points, and displacement vectors, each tied to a frame of reference that may represent a base coordinate system, a uniformly sampled grid, or its dual. By encoding both frames and units into the type system, it ensures that only physically meaningful operations are allowed. A prototype implementation in Elm demonstrates the approach, supporting type simplification, frame normalization, and detailed diagnostic messages that guide users toward resolving errors. A case study in Magnetic Resonance Imaging (MRI) shows how the system enforces valid transformations between spatial and frequency domains and prevents common modeling mistakes. This work shows that embedding physical units and frames of reference directly into a bidirectional type system improves the reliability and transparency of scientific software. It helps catch invalid operations at compile time and provides feedback that is understandable to developers and scientists alike.