5 ms·

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

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 https://github.com/SciNim/Unchained

deleted 3y ago
[deleted]
kragen 3y ago
'can be implemented' is different from 'has been implemented' how does unchained handle gaussian elimination
- V1ndaar 3y ago
  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 3y ago
    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-linear-algebra.html 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 3y ago
      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 https://github.com/SciNim/astGrad#extra-fun [1]: https://github.com/SciNim/Measuremancer/ https://github.com/SciNim/Measuremancer/
      - kragen 3y ago
        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 3y ago
        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).
        kragen 3y ago
        if you have to adapt it in certain cases because of limitations in the type system, from my point of view that amounts to the type system handling units incorrectly in the same way that pascal's type system handled array sizes 'incorrectly' because you couldn't write a subroutine that could operate on an array of any size, just arrays of one size or another you could say 'yes, well, the code you write will have to be adapted in certain cases (compared to current existing implementations of string algorithms)', like say if your string has more than 20 characters in it, but the reason is that you're doing something the type system can't handle
sharkdp 3y ago
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).
eviks 3y ago
Would you be able to do nice looking syntax like this in Nim? x² x÷y
- V1ndaar 3y ago
  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 https://github.com/SciNim/Measuremancer
  - eviks 3y ago
    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)

deleted 3y ago

[deleted]

kragen 3y ago

'can be implemented' is different from 'has been implemented' how does unchained handle gaussian elimination

V1ndaar 3y ago
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 3y ago
  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-linear-algebra.html 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 3y ago
    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 https://github.com/SciNim/astGrad#extra-fun [1]: https://github.com/SciNim/Measuremancer/ https://github.com/SciNim/Measuremancer/
    - kragen 3y ago
      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 3y ago
        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).
        kragen 3y ago
        if you have to adapt it in certain cases because of limitations in the type system, from my point of view that amounts to the type system handling units incorrectly in the same way that pascal's type system handled array sizes 'incorrectly' because you couldn't write a subroutine that could operate on an array of any size, just arrays of one size or another you could say 'yes, well, the code you write will have to be adapted in certain cases (compared to current existing implementations of string algorithms)', like say if your string has more than 20 characters in it, but the reason is that you're doing something the type system can't handle

sharkdp 3y ago

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

eviks 3y ago

Would you be able to do nice looking syntax like this in Nim? x² x÷y

V1ndaar 3y ago
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 https://github.com/SciNim/Measuremancer
- eviks 3y ago
  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)