Modeling units of measure with phantom types

[Max Goldstein]

As John Kelly pointed out to me in another thread, there's a trick called a "phantom type" that's possible in Elm. It's where a union type has a type variable that's not used on the right side. If you don't expose the constructor, you can use the type to only allow values that have come through other functions. Here's an example:

-- the Phantom Type

type Measurement a

    = M Float

-- "dummy" types

type Length = Length

type Width = Width

type Area = Area

add : Measurement a -> Measurement a -> Measurement a

add (M a) (M b) =

    M (a + b)

multiply : Measurement Length -> Measurement Width -> Measurement Area

multiply (M a) (M b) =

    M (a * b)

I've been thinking about how to make these guarantees, there was a recent ThoughtBots post on it, and I'm not sure anyone has seen this before. Building out a whole system of measurement this way seems really tedious, but for a smaller and more specific problem, it might be a valuable technique to know about.

Note that this only works if it's impossible to create a polymorphic type, e.g. Measurement a, because that will get unified with whatever type is expected by the annotation. If every Measurement value is concrete, it can't be passed in the wrong place.

As I've been thinking about this, I've seen multiple orthogonal pieces of information that we sometimes sloppily roll up into the type:

• The representation, the storage of bits in memory, such as IEEE floating point or 64-bit integer.
• The dimension, in the physics sense, such as length*mass.
• The interpretation. Is it length or width or height? Is length*mass torque or momentum?
• The units, such as meter*kilograms.

When dealing with a discrete case -- the classic example is not mixing up rows and columns in a grid/table -- we need the representation and the interpretation (rows or columns), but units and dimensions seem not to apply. Similarly, if we want to distinguish between strings (URLs, IDs, escaped and unescaped HTML, and so on), we seem to want the same things.

It might be interesting to have a wrapped String library that would perform the typical operations on strings with type-level identifiers, so when you require an ID (aliased to WrapedString IDType) you can only get one that's been through your validator. Or you could build URL-specific abstractions like Url.join : Url -> List String -> Url.

So, just a neat idea not everyone is aware of, hopefully someone finds it interesting or useful.

[Nick H]

Here:

Is length*mass torque or momentum?

I think the quantities you meant to compare are torque and energy (both of which have units of force*length).

The only reason I bring it up is because it points to some interesting design problems. Energy is always a scalar (one numeric component). Torque, although sometimes expressed as a scalar or a vector, is actually best represented as a bivector (two components per spatial dimension in whatever system we are looking at).

This is a case where we can reduce the risk of a wrong interpretation by choosing a good representation. We're used to this idea as programmers, but I think sometimes it goes unappreciated in physics.

(It's also a situation where introducing redundancy into our representation is a good idea. Bivectors (like quaternions) can be equal even if their components are unequal. Adding redundant information to the data structure actually makes the calculation easier and interpretation clearer!)

The idea of representing units with phantom types is new to me. I will definitely be playing with this!

~Nick

--
You received this message because you are subscribed to the Google Groups "Elm Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to elm-discuss+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Max Goldstein]

I think the quantities you meant to compare are torque and energy (both of which have units of force*length).

Yup, sorry.

 

Torque, although sometimes expressed as a scalar or a vector, is actually best represented as a bivector (two components per spatial dimension in whatever system we are looking at).

How so? I know that the force and length are orthogonal, but that would still be one component per spatial dimension. 

[Nick H]

In the same way that a vector is usually represented by a line segment, a bivector can be represented by a parallelogram where the component vectors form the sides. I was imagining a naive representation where you just store the component vectors.

type alias Bivector = { a : Vector, b : Vector }

So if force and position are 3D vectors, then the torque bivector is 6D. (But you could come up with more efficient representations that use fewer components.)

--

[Nick H]

(Two bivectors are equal when their parallelograms have equal areas and are in the same plane. That's where the redundancy comes in.)