Remix clone Hacker News

That's a great question.

Haskell has arrays and matrices of homogeneous types, so it wouldn't work by default.

If you needed this kind of functionality, you would have to create your own Matrix type which would look very similar to a 9-tuple, and then define matrix multiplication. It would then be possible to encode the dimensional constraints in the type signature, but it's already quite involved for 2x2 matrices:

    data Mat2 a b c d 
        = MkMatrix a b c d
    
    matmul :: ???? -- good luck writing this type signature
    matmul (MkMatrix a11 a12 a21 a22) (MkMatrix b11 b12 b21 b22)
        = MkMatrix ((a11 * b11) + (a12 * b21))
                   ((a11 * b12) + (a12 * b22))
                   ((a21 * b11) + (a22 * b21))
                   ((a21 * b12) + (a22 * b22))

I can't imagine for 3x3.

▲ simiones 5 days ago | parent [-]

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 5 days ago | parent [-]

> ... 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.