Remix.run Logo
simiones 5 days ago

Would this work for something like linear algebra? Could it support multiplying two 3x3 matrices where each cell can have a different dimension, and only work if they are compatible?

antononcube 4 days ago | parent | next [-]

Yes you can do that (easily) with Wolfram Language (aka Mathematica.)

Here is an example:

    mat1 = Table[
       RandomChoice[{
           Quantity[RandomReal[], "Meters"],
           Quantity[RandomReal[], "Seconds"],
           Quantity[RandomReal[], "Meters/Seconds"],
           Quantity[RandomReal[], "Meters/Seconds^2"]
         }] , 3, 3];
    mat1 // MatrixForm
    
    mat1 . Transpose[mat1]
See the corresponding screenshot: https://imgur.com/aP9Ugk2
librasteve 2 days ago | parent [-]

I whipped up this in raku:

  use Physics::Measure :ALL;

  sub infix:<·>(@x1, @x2) {
    die "Incompatible dimensions."
            unless @x1 == @x2[0] && @x1[0] == @x2;

    [for ^@x1 -> $m {
        [for ^@x1 -> $n {
            [+] @x1[$m;*] >>*<< @x2[*;$n]
        }]
    }]
  }

  my @m = [[1m,2m],[3m,4m]]; 

  say @m · [Z] @m;     #[[5m^2 11m^2] [11m^2 25m^2]]
Since Physics::Measure is strong on illegal combinations and since there are not many realistic random combinations of Units (s^2 anyone) I have not gone random for my example.
boscillator 5 days ago | parent | prev | next [-]

This is something I always feel is missing from unit libraries.

cosmic_quanta 5 days ago | parent | prev [-]

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

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