[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!

[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

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