3 ms·

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 er

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 3y ago
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).

V1ndaar 3y ago

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