[V1ndaar]

Or you could just use Nim [0], where this sort of thing can be implemented in Nim's macro system. Then you have a regular programming language combined with CT safe units. :)

It even pretty much looks identical to those Numbat snippets!

    import unchained
    
    let earth_mass = 5.972168e24.kg
    let solar_mass = 1.9885e30.kg
    let lunar_mass = 7.342e22.kg
    
    let distance_sun = 1.AU  # astronomical unit
    let distance_moon = 384_400.km
    
    let force_sun = G_Newton * earth_mass * solar_mass / distance_sun
    let force_moon = G_Newton * earth_mass * lunar_mass / distance_moon
    
    echo force_sun / force_moon
    # 69593.6 UnitLess

Sorry for the shameless plug. ;) Numbat looks quite cool though and the article talks about a lot of things to think about when writing such a program / lib / programming language.

[0]: https://github.com/SciNim/Unchained

[kragen]

'can be implemented' is different from 'has been implemented'

how does unchained handle gaussian elimination

[V1ndaar]

Gaussian elimination in what context even? If your LA library supports generic types, it might work. But generally generic math operations are tricky to get right, because math often does things that from a pure physical perspective don't make a whole lot of sense / you run into trouble with too many competing types due to temporary multiplication / divisions etc (which is a big issue in any statically typed language, because your container (vector, matrix, tensor whatever) type is typically a single unit type!

[kragen]

most linear algebra requires vectors of multiple unit types. think of runge-kutta for a second-order system, for example, or just about any multivariate system. see https://yosefk.com/blog/can-your-static-type-system-handle-l... for more information

if your static type system can't handle that, it can't handle unit types for basic linear algebra subroutines

[V1ndaar]

I mean that article of yours highlights the difficulties one encounters fairly well, I would say. I don't disagree that this is (generally) a tricky problem!

Nim allows you to do a lot, e.g. derivatives of a unitful expression with measurement errors [0]. But other aspects run into the reality of dealing with a static type system. For example in Measuremancer [1], the library handling measurements with uncertainties, each `Measurement` is a single generic `Measurement[T]`. Each measurement stores the derivatives for error propagation. Obviously the derivatives have different units. Now, we could make `Measurement` a two-fold generic, `Measurement[T, U]`, but that just makes things more unwieldy in practice, for not much gain.

Without rewriting a majority of existing code you will always run into trouble where your perfect unit type system will either break or you'll need to work around it anyway (e.g. calling into some C library for part of the code).

[0]: https://github.com/SciNim/astGrad#extra-fun

[1]: https://github.com/SciNim/Measuremancer/

[kragen]

just to clarify, i didn't write the article; yossi kreinin did

you seem to be saying that it's impossible to formulate a type system that handles units correctly in contexts like generic linear algebra algorithms

i think you are mistaken about that

[V1ndaar]

I nowhere said impossible! All I say it is tricky and that likely the code you write will have to be adapted in certain cases (compared to current existing implementations of numerical algorithms).

[eviks]

Would you be able to do nice looking syntax like this in Nim?

x²

x÷y

[V1ndaar]

Yeah, unicode characters in Nim code are supported. However, if by `x²` you'd want to square an identifier `x`, that won't work. The Nim lexer parses `x²` as a single identifier.

We do have infix unicode operators though. So `x ÷ y` (spacing required though!) could be implemented easily. I use this for `±` in Measuremancer [0] (which btw also supports Unchained units, for error propagation on unitful measurements).

[0]: https://github.com/SciNim/Measuremancer

[eviks]

Required spacing is a blocker/friction, that's one of the benefits of DSLs, I guess, being able to eschew the conservative syntax of the general-purpose languages (though Unicode support is a good step forward)

[sharkdp]

Thank you for the reference. I hadn't seen Unchained.

You missed the point about this example though. I wanted to show how Numbat can help prevent the exact error that you made in your program. 'G_Newton * earth_mass * solar_mass / distance_sun' is not a force. It's an energy. How would you write type annotations in this Nim example to help you find that same mistake?

[V1ndaar]

Whoops, guilty as charged. I did indeed glance over that (both the text and the equation not actually being 1/r²).

In this case to get compiler help it's pretty much identical to Numbat. Annotating the "force" variables with a `Force` type. There's a few technicalities involved though. Normally the user is supposed to use explicit type annotations for variables. Quantities like `Force`, `Energy` etc. are mainly supported for function arguments (they are "concepts" in Nim lingo, a specific version of generics).

Technically you can abuse these concepts for type checking, by annotating with `Force`, e.g. `let force_sun: Force = ...`. That will correctly raise a CT error about mismatching units in this case. However, the code will /also/ not compile if you type `Energy` due to the underspecified type.

So what you're supposed to do is:

    import unchained
    
    let earth_mass = 5.972168e24.kg
    let solar_mass = 1.9885e30.kg
    let lunar_mass = 7.342e22.kg
    
    let distance_sun = 1.AU  # astronomical unit
    let distance_moon = 384_400.km
    
    let force_sun: N = G_Newton * earth_mass * solar_mass / distance_sun
    let force_moon: N = G_Newton * earth_mass * lunar_mass / distance_moon
    
    echo force_sun / force_moon

which will correctly raise a

    Error: type mismatch: got 'Joule' for '...' but expected 'Newton = Alias'

(or any other unit of force; note that if it was a non SI unit, e.g. `eV` for an energy, you'd need to explicitly convert the RHS expression into `eV` using `.to(eV)`. That will perform the CT check of whether the conversion is valid, and if so, hands you the value in `eV`. Implicit conversions to explicitly given types is not supported)

So I think we more or less do the same things. :)

And just to clarify, I'm always happy to see more libraries / programs etc. that do units as types. But for the same reason you hadn't even heard about Unchained, is the reason I can't stop myself from mentioning it in such a context. :D (niche programming language + niche topic clearly doesn't help).