Skip to content

Instantly share code, notes, and snippets.

@sharkdp
Last active August 24, 2017 19:59
Show Gist options
  • Save sharkdp/5161bf9f46263c70ec91d66692c6864d to your computer and use it in GitHub Desktop.
Save sharkdp/5161bf9f46263c70ec91d66692c6864d to your computer and use it in GitHub Desktop.
Type-safety in physics calculations

Type-safety in physics calculations

This article describes a (loose?) analogy between physical units and data types in programming languages that I thought about while working on Insect, a scientific calculator that supports physical units.

In addition to typical mathematical operators like +, *, ^, %, etc., Insect has a special conversion operator (written as an arrow ->/ or as the word to). It can be used to convert an expression to a particular unit:

≫ 2 ft + 2 in ➞ cm

  = 66.04 cm
  
≫ 6 Mbit/s * 1.5 h ➞ GB

   = 4.05 GB

(you can try out the code examples in the interactive web console)

The conversion operator throws an error if the physical dimensions do not line up:

≫ 2 watts ➞ newton meter

  Conversion error:
    Cannot convert unit W (base units: kg·m²·s⁻³)
                to unit N·m (base units: kg·m²·s⁻²)

We will later see how this can be used to enforce unit-safety. For now, suppose that a user defines a function to compute the kinetic energy of a moving object:

≫ kineticEnergy(mass, speed) = 0.5 * mass * speed^2

The function can be used like this:

≫ kineticEnergy(100 kg, 30 m/s) ➞ kJ

   = 45 kJ

However, there are no guarantees that this function actually returns an energy. If the function is accidentally called with reversed arguments, for example, this happens:

≫ kineticEnergy(30 m/s, 100 kg)

   = 150000 kg²·m/s

While the user could infer his mistake from the wrong unit in the result, this is not very satisfactory. Using the conversion operator, we can force the output to be an energy:

≫ kineticEnergy(mass, speed) = 0.5 * mass * speed^2 ➞ J

If someone now switches the order of the arguments, he will be presented with a (rather confusing) error message:

≫ kineticEnergy(40 m/s, 10 kg)

Conversion error:

  Cannot convert unit kg²·m/s (base units: kg²·m·s⁻¹)
              to unit J (base units: kg·m²·s⁻²)

We can still do better. The fact that the conversion operator can be used in every expression allows us to (type)check the function arguments:

≫ kineticEnergy(mass, speed) = 0.5 * (mass ➞ kg) * (speed ➞ m/s)^2 ➞ J

... turning the error message into:

Conversion error:

  Cannot convert unit m/s (base units: m·s⁻¹)
              to unit kg

which should be a pretty good hint of what went wrong. Note that the new definition does not force the units to be precisely kg and m/s --- it only checks if the physical dimensions are correct (mass and speed):

≫ kineticEnergy(10 ounces, 30 mph) ➞ calories

  = 6.0935 cal

Outlook

Physical units as types?

Instead of thinking of physical units as types, I believe it's more appropriate to think of physical dimensions as being similar to types. In this sense, the quantities 10 m/s and 30 mph would both be of type speed. Currently, Insect does not have an explicit notion of physical dimension, but I think this could be a useful addition.

Static type checking?

The checks above are similar to runtime type-checks in dynamic programming languages, i.e. type(expr) is int in Python or typeof expr === 'number' in JavaScript. However, given how easy the expression language of Insect is, it should be feasible to actually add static "type checking". A possible syntax (borrowed from Haskell-style languages) could look like this:

kineticEnergy ∷ (Mass, Speed) ➞ Energy
kineticEnergy(mass, speed) = 0.5 * mass * speed^2

The explicit type-annotation could then be used to verify both the function definition as well as future function calls.

https://github.com/sharkdp/insect

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment