5 ms·

Thanks for the sample! I was asking because it seems to me this is always an interesting example of a very common and very well defined formal operation where n

Thanks for the sample! I was asking because it seems to me this is always an interesting example of a very common and very well defined formal operation where nevertheless type systems are extremely cumbersome to use, but I'm always curious if there is some solution that I'm missing. I wonder if there is any plausible approach that would work closer to how units are treated in physics calculations - 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).

cosmic_quanta 2y 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 2y ago
  Nice, I didn't realize this! Thank you for going into this level of detail.

cosmic_quanta 2y 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 2y ago
Nice, I didn't realize this! Thank you for going into this level of detail.