Remix.run Logo
Remix clone Hacker News
new | show | ask | jobsGithub
▲ cosmic_quanta 5 days ago

> ... not as types, but as special numerical values, more or less (values that you can multiply/divide by any other unit, but can only add/subtract with themselves).

What's so cool about `dimensional` is that the types work the way you describe!

Normally, in Haskell, the addition and multiplication functions are typed like so:

    (+) :: Double -> Double -> Double
    (*) :: Double -> Double -> Double
With `dimensional`, addition looks like:

    (+) :: Quantity d Double -> Quantity d Double -> Quantity d Double
which means you can't add quantities with incompatible dimensions, so far so good. But multiplication looks like:

    (*) :: Quantity d1 Double -> Quantity d2 Double -> Quantity (d1 * d2) Double
That is, the dimensions of the result of multiplication (d1 * d2) follow the physics meaning of multiplication. What can look confusing is that (d1 * d2) is a type-level calculation which is run at compile-time.

This means that `dimensional` isn't only about 'statically checking' dimensions and units, but also inferring them.

You can see this interactively. What is the type of 1 meter divided by 1 second:

    ghci> :t (1 *~ meter) / (1 *~ second)
    Quantity (Dim Pos1 Zero Neg1 Zero Zero Zero Zero) Double
where (Dim Pos1 Zero Neg1 Zero Zero Zero Zero) is a synonym for the dimension of velocity, which is not checked -- it is inferred at compile time.
▲simiones 4 days ago | parent [-]

Nice, I didn't realize this! Thank you for going into this level of detail.