In this post I’d like to shortly discuss an idea I’ve had a long time ago about type systems and units of measure. The usual pitch about having units in the type system of a programming language starts with a sad story about some space craft crash because different teams used different measures of distance. The competing systems are usually Imperial vs RebelsMetric. Then units in the type system are introduced, which is a way to check that only numbers of the exact same unit are used in a...
