In F#, which has measure types, the types are checked at compile time but erased at runtime, so they have no additional runtime cost. Measures are a kind of painted type.
[<Measure>] type degC;
[<Measure>] type K;
let degrees_to_kelvin (degrees : float<degC>) : float<K> =
degrees * 1<K/degC> + 273.15<K>
let d = 10.0<degC>
let k : float<K> = degrees_to_kelvin d
The .NET runtime only sees `float`, as the measures have been erased, and constant folding will remove the `*1` that we used to change the measure. The `degrees_to_kelvin` call may also be inlined by the JIT compiler. We could potentially add `[<MethodImpl(MethodImplOptions.AggressiveInlining)>]` to force it to inline when possible, then constant folding may reduce the whole expression down to its result in the binary.
The downside to adding the SI into the type system is the SI is not a sound type system. For example:
[<Measure>] type m
[<Measure>] type s
[<Measure>] type kg
[<Measure>] type N = kg*m/s^2
[<Measure>] type J = kg*m^2/s^2
[<Measure>] type Nm = N*m
let func_expecting_torque (t : float<Nm>) = ...
let x = 10.0<J>
func_expecting_torque x
The type system will permit this: using torque where energy is expected, and vice-versa, because they have the same SI unit, but they don't represent the same thing, and ideally it should be rejected. A potential improvement is to include Siano's Orientational Analysis[1], which can resolve this particular unsoundness because the orientations of Nm and J would be incompatible.
The downside to adding the SI into the type system is the SI is not a sound type system. For example:
The type system will permit this: using torque where energy is expected, and vice-versa, because they have the same SI unit, but they don't represent the same thing, and ideally it should be rejected. A potential improvement is to include Siano's Orientational Analysis[1], which can resolve this particular unsoundness because the orientations of Nm and J would be incompatible.[1]:https://www.doc88.com/p-9099799188322.html