[HN Gopher] Show HN: Numbat - A programming language with physic...
___________________________________________________________________
Show HN: Numbat - A programming language with physical dimensions
as types
Author : sharkdp
Score : 118 points
Date : 2023-11-15 13:34 UTC (1 days ago)
(HTM) web link (numbat.dev)
(TXT) w3m dump (numbat.dev)
| jqpabc123 wrote:
| _perform computations with physical units._
|
| It has units awareness --- not necessarily only _physical_ units.
|
| For example; light, temperature and time are measured in units
| but they are not _physical_ units --- aka 3 dimensional.
| gus_massa wrote:
| All are physical units. In particular in special relativity
| time is couples with position and you myst use cuadrivectors
| (t, x, y, z).
| jqpabc123 wrote:
| Time exists independent of location and can not be visualized
| in any "physical" way. The same is true for lots of other
| units of measure.
|
| https://phys.org/news/2012-04-physicists-abolish-fourth-
| dime...
| davidcuddeback wrote:
| Physical can be understood to mean "of or relating to
| matter and energy or the sciences dealing with them,
| especially physics." Light, temperature, and time are
| described by physics, so I would consider "physical" to be
| an accurate adjective for those units. You seem to be using
| a more limited definition of physical, closer to the word
| "spatial."
|
| Also, btw, you might want to read the article you linked.
| The article is discussing a fringe idea that some
| scientists have. Scientists are free to explore new ideas,
| and they make for good click bait for science journalists.
| Until those ideas gain traction, they don't provide for
| compelling arguments, though.
| Aspos wrote:
| This is great. I want this as an addon to JS and Python.
| seanos wrote:
| For Python, there is the Pint library:
| https://pint.readthedocs.io/en/stable/
| jsiva wrote:
| Another python alternative that work well with numpy arrays
| is astropy.units (also mentioned on the pint website):
|
| https://docs.astropy.org/en/stable/units/
| evntdrvn wrote:
| I can't resist mentioning F# Units of Measure aka UoM :)
|
| https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref...
| stiiv wrote:
| Thank you for not resisting. F# is very hard to beat for a
| tight domain model.
| openquery wrote:
| And the equivalent uom in Rust.
|
| https://crates.io/crates/uom
| nritchie wrote:
| Or unitful.jl in Julia which evaluates the units at compile
| time resulting in no performance loss at runtime.
| sharkdp wrote:
| F# is the only language I looked at that has a really powerful
| unit system. The author of that unit system wrote his PhD
| thesis on the subject [1]. Numbat's type system is actually
| pretty close to what was suggested in that thesis (in contrast
| to F#'s system, which is based on units -- not dimensions).
|
| [1] https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf
| runamuck wrote:
| So if I try to get the Falcon to do the Kessel run in two
| Parsecs, Numbat will raise an exception.
| bertil wrote:
| Because that's too short (12 parsecs being close to the
| theoretical maximum without being swallowed by a black hole) or
| because it thinks that you confused a unit of distance and
| speed?
| enbugger wrote:
| In theory it can help to compute how many ore belts I need for
| producing full belt of white sciences in Factorio?
| pif wrote:
| You don't need a new programming language for something that C++
| templates with integer constants give you for free.
| antoineMoPa wrote:
| Can you provide examples?
| pif wrote:
| - you define a template class accepting 1 constant integer
| for each dimension you want to consider (length and/or time
| and/or mass and/or temperature);
|
| - you define addition and subtraction between objects of one
| type returning an object of the same type;
|
| - you define multiplication and division as returning an
| object of a type with the dimensions summed or subtracted;
|
| - and you get dimensional correctness via type safety.
| n_plus_1_acc wrote:
| https://crates.io/crates/uom trivially convertable to cpp
| n_plus_1_acc wrote:
| https://www.boost.org/doc/libs/1_82_0/doc/html/boost_units/U.
| ..
| leakim wrote:
| In Scala https://github.com/typelevel/squants
| vlovich123 wrote:
| Some of us don't want to wait until the heat death of the
| universe for the code to compile (not a snipe at boost as a
| whole - boost units is quite bad iirc). There's also
| performance problems if the compiler isn't able to see through
| all the templates although that's true for many things in this
| space. Finally iirc it doesn't let you define your own custom
| units which is a common challenge with dimensional analysis as
| a library.
|
| If rust ever gets more complete const generics, then things
| like tiny-uom might work.
| adamdegas wrote:
| Came here to say this. As soon as I saw the first example on
| the linked web page, I immediately thought of C++. Reinventing
| the wheel.
| jskherman wrote:
| How does Numbat infer the type/unit for operations that involve
| transcendental functions like the trigonometric functions and the
| natural logarithm? How about for exponents that are not integers
| (rational or irrational)?
|
| I've seen from to time some empirical equations that result to
| this. Usually, it's just hand-waved away and the non-integer
| units are ignored or dropped when the transcendental function is
| evaluated. I guess the trivial answer is probably add an extra
| factor with a value of 1 with the reciprocal units to result to
| the said type 1 for dimensionless units?
| iNic wrote:
| Those types of functions are only allowed to take in
| dimensionless (ie scalar) values. Numbat seems to handle this
| correctly, see [1].
|
| [1]: https://numbat.dev
| jskherman wrote:
| I guess that's logical, still a bit tedious in converting
| values to scalars...
| geysersam wrote:
| If the value passed to the function isn't dimensionless
| there's very likely a unit error somewhere.
|
| I can't come up with an example where that would be a
| reasonable thing to do, but haven't thought too much about
| it.
| xigoi wrote:
| If you find yourself wanting to do that, you're probably
| making the exact kind of error that the language is meant
| to prevent.
| marginalia_nu wrote:
| To be fair, thse functions aren't defined for physical
| quantities.
|
| As a physicist, if you ever see units on the parameter to a
| trigonmetric function, you can be fairly certain something
| is wrong.
|
| You can derive this from how e.g. cos(x) can be written as
| a polynomial series, something like 1 - x^2 + whatever; and
| since 1 and x^2 would have different units if x is anything
| but unitless, you've goofed.
|
| That's a big reason why units are used in calculations in
| the first place. They basically act as a sort of checksum
| for your calculations.
| sharkdp wrote:
| > As a physicist, if you ever see units on the parameter
| to a trigonmetric function, you can be fairly certain
| something is wrong.
|
| Exactly. Which is why trigonometric functions in Numbat
| have the signature cos(x: Scalar) ->
| Scalar
|
| and only take quantities as arguments that are implicitly
| convertible to a scalar, like 'cos(pi / 3)', 'cos(30
| deg)' or 'cos(0.5 turn)'.
|
| Whether or not angles should be considered dimensionless
| is actually a matter of academic dispute. If you want to
| know more, take a look at
| https://github.com/sharkdp/numbat/pull/167 and the
| references therein.
| pklausler wrote:
| Radians vs degrees?
| mikewarot wrote:
| Radians, gradians, degrees, minutes, seconds, thirds,
| revolutions are all ways of dividing up a circle
| marginalia_nu wrote:
| For radians, we can note that the length of a circle
| segment is ra, where r is the radius and a is the angle,
| where both the radius and circle segment have dimensions
| length; then we must infer that a is dimensionless.
|
| Degrees follow a similar argument.
| sharkdp wrote:
| You don't have to convert to scalars. Numbers have a type
| of 1 (= Scalar).
|
| You can just call exp(3), for example:
| https://numbat.dev/?q=exp%283%29%E2%8F%8E
|
| Or you could pass an angle quantity, which is convertible
| to a Scalar. Like cos(30 deg): https://numbat.dev/?q=exp%28
| 3%29%E2%8F%8Ecos%2830+deg%29%E2%...
| wwalexander wrote:
| A month cannot be unambiguously represented as a length of time,
| as the length of a month is variable.
| michaelcampbell wrote:
| It looks as if they're defining a month as some amount of days.
| (30.4369, given the following.) >>> 1 day + 1
| month 1 day + 1 month = 31.4369
| day
| aimor wrote:
| >>> 1 month -> seconds = 2_629_746 s [Time]
|
| Just playing around with this and really enjoying it.
| manifoldgeo wrote:
| How does something like `let y: Time = 1 year` work? Does it take
| into consideration the idea of leap years and leap seconds,
| counting a single year as 365.2422 days[0]? Or does it count as
| 365 days?
|
| I got curious and installed the CLI tool[1] and found that it
| does indeed account for leap second / leap years:
|
| >>> let jahr: Time = 1 year
|
| >>> let tage: Time = jahr -> days
|
| >>> tage = 365.243 day [Time]
|
| References:
|
| 0: https://museum.seiko.co.jp/en/knowledge/story_01/
|
| 1: https://numbat.dev/doc/cli-installation.html
| vlovich123 wrote:
| I feel like that's unit confusion. Converting from year to day
| should require you to specify what calendar year you're in to
| resolve the ambiguity. Otherwise I set an alarm for today + 1
| year and things are off by 6 hours.
|
| Time is nasty because there's lots of overloaded concepts and
| bugs hide in the implicit conversions between meanings.
|
| I'm also kinda curious what the underlying type is. Is it a
| double or do they use arbitrary precision math and take the
| perf hit.
| SenAnder wrote:
| > I feel like that's unit confusion. Converting from year to
| day should require you to specify what calendar year you're
| in to resolve the ambiguity.
|
| A year has two meanings - a calendar year, with all the leap
| days and seconds and timezones, or a duration of time. The
| latter is still useful, e.g. when someone states that Proxima
| Centauri is 4.2 light-years away, they don't want to deal
| with leap-days.
|
| Decent time libraries have separate ways to deal with
| durations and dates.
| thriftwy wrote:
| Except there is also
| https://en.m.wikipedia.org/wiki/Sidereal_year So I would
| say they need explicit different years.
| sharkdp wrote:
| So 'year' refers to the Gregorian year and is equal to
| 365.243 days [1]. We also have 'julian_year' which is
| equal to '365.25 days'.
|
| We also have 'sidereal_day' equal to '23.9345 hours', and
| if you believe it is useful, we can also add
| 'sidereal_years'.
|
| [1] https://numbat.dev/doc/list-units.html
| thriftwy wrote:
| Do you have a calendar_year and a calendar_leap_year?
| peheje wrote:
| Just a fun related video from Neil deGrasse Tyson
| https://youtu.be/mKCvqzCrZfA?si=uW4FOXg2nrqic1ZP
| agalunar wrote:
| 365*243 ought to be 365*2425 exactly:
|
| Per 400 years, there is one leap day every 4 years (100 leap
| days), except when the year is divisible by 100 (so we
| overcounted by 4 and there are 100 - 4 = 96 leap days),
| _except_ when the year is divisible by 400 (so we need to add
| that day back and arrive at 100 - 4 + 1 = 97). This gives us 97
| /400 = 0*2425.
|
| The tropical year is about 365*24219 days long, but that's not
| relevant to timekeeping.
| sharkdp wrote:
| > 365*243 ought to be 365*2425 exactly:
|
| Yes. This is also how it is defined: https://github.com/shark
| dp/numbat/blob/ba9e97b1fbf6353d24695...
|
| The calculation above is showing a rounded result (6
| significant digits by default).
| agalunar wrote:
| That's what I figured! but thought the derivation would be
| fun to share with people reading the comments.
| V1ndaar wrote:
| 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 wrote:
| 'can be implemented' is different from 'has been implemented'
|
| how does unchained handle gaussian elimination
| V1ndaar wrote:
| 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 wrote:
| 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
| sharkdp wrote:
| 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 wrote:
| Whoops, guilty as charged. I did indeed glance over that
| (both the text and the equation not actually being 1/r2).
|
| 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).
| indentit wrote:
| Can it be used as a date calculator? I didn't see a way to
| specify "today" or "tomorrow". Like "today" + 14 days etc.
| BasilPH wrote:
| I was also looking into this, and couldn't find a way to do it.
|
| My guess is that it has support for time, but not for
| calendars. The fact that a "month" is a static length points in
| this direction.
|
| Maybe there's going to be a calendar module in the future
| though?
| JNRowe wrote:
| If you're looking for a general solution to that specific type
| of problem, then dateutils1 is really useful. It deals with
| conversions, durations, matching, repeats, etc. It also has a
| clear and well defined date input format, and being a
| collection of command line tools it is easy to mangle it in to
| other tools.
|
| 1 http://www.fresse.org/dateutils
| cosmojg wrote:
| Super cool! I love when programming languages try to do more with
| types.
|
| Julia has a neat little library called Unitful.jl[1] which does
| almost exactly what Numbat does by taking advantage of Julia's
| extremely flexible type system. Extending it to cover all of
| Numbat's functionality could be trivially accomplished in a few
| lines. In fact, fun type magic like this is pretty much my
| primary motivation for using Julia in the first place.
|
| Not that I want to detract from the author's hard work, of
| course, I'm just very excited about Julia! Numbat is obviously an
| awesome project, and I can't wait to see where it leads!
|
| [1] https://painterqubits.github.io/Unitful.jl/stable/
| sharkdp wrote:
| I looked at Julia and Unitful.jl quite a bit when designing
| Numbat. It looks great.
|
| > Extending it to cover all of Numbat's functionality could be
| trivially accomplished in a few lines.
|
| Look, I'm not claiming that Numbat is superior. But I think
| Numbat might have its own little niche. And even if not, it's
| always good to have alternative solutions available.
|
| - Numbat is specifically designed to handle physical dimensions
| and units. It has a special syntax to give developers the best
| experience when dealing with units. You can just type "KiB" and
| have it be parsed as kibibytes. You can use the "->" operator
| to convert to other units. You can directly annotate functions
| with physical dimensions ("fn kinetic_energy(m: Mass, v:
| Velocity) -> Energy = ..."). Other languages and their unit
| libraries might have the same functionality, but it has always
| been added as an afterthought.
|
| - Numbat has a static type system, Julia's is dynamic.
|
| - Numbat can be compiled to Web Assembly and you can run it in
| your browser. I'm not sure if that is possible with Julia?
|
| - Numbat might eventually be able to infer (physical dimension)
| function parameter types with its Hindley-Milner-style type
| system [1]. The only language that I know of that can do this
| is F#. The author of F#'s unit system wrote his PhD thesis on
| the subject [2], and Numbat follows the original approach in
| the thesis quite closely.
|
| [1] https://github.com/sharkdp/numbat/issues/29
|
| [2] https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-391.pdf
| hsfzxjy wrote:
| Remind me of GNU Units https://www.gnu.org/software/units/
| docandrew wrote:
| Ada's type system also allows compile-time checking of units like
| physical dimensions:
|
| https://gcc.gnu.org/onlinedocs/gcc-4.9.4/gnat_ugn_unw/Perfor...
|
| https://blog.adacore.com/uploads/dc.pdf
| praveen9920 wrote:
| It's interesting that they support currency units. Wonder how the
| conversion works. Probably have to provide conversion factor as
| well?
| eminence32 wrote:
| It'll fetch current conversation rates from the internet
| sharkdp wrote:
| Yes. We use up-to-date currency exchange rates from the
| European Central Bank [1].
|
| https://github.com/sharkdp/numbat/blob/786512175b99c195a7d5b.
| ..
| freistil wrote:
| That's one of these things where you can spend quite some
| effort to get that right but it's not going to be useful
| for anything deeper. That's like saying "here, we have
| implemented Newton's mechanics in fundamental types, now
| you can in theory simulate a body up from its atoms!" and
| while that would sound compelling if you don't know much
| about physics, it would quickly become useless once you
| know more about physics.
| joeatwork wrote:
| If I'm reading this correctly, the Frink language has similar
| features (and also seems darn useful!) https://frinklang.org/
| sharkdp wrote:
| I looked at Frink quite a bit and I agree that it looks cool.
| But as far as I can tell, it does not have a static type
| system. At least it's not based on physical dimensions.
|
| And it is not open source.
| thesuperbigfrog wrote:
| Frink (https://frinklang.org/) is an older language with similar
| design goals.
|
| Frink runs on the JVM and is also available on Android.
|
| I use it as a general purpose calculator on my smartphone.
|
| It's really nice that Numbat is written in Rust :) Will have to
| try it out.
| nerdponx wrote:
| There's also Insect for interactive use: https://insect.sh/
| sharkdp wrote:
| Insect is the predecessor project. Numbat is the replacement.
| It also has an interactive version at https://numbat.dev/
| sharkdp wrote:
| Frink is not open source, unfortunately.
| thesuperbigfrog wrote:
| >> Frink is not open source, unfortunately.
|
| True: https://frinklang.org/faq.html#OpenSource
|
| Thanks for sharing Numbat with us.
|
| It looks great!
| exp1orer wrote:
| This is really cool!
|
| If the author is around, I notice in the README you mention the
| GNU units program, which I use quite a bit. I'm curious if you've
| made any notable divergences from it?
| sharkdp wrote:
| Thank you.
|
| I don't think we diverge from units on purpose anywhere, but I
| am probably not very familiar with its syntax, to be honest. I
| did however look at its huge collection of units and checked if
| there were any important units missing. I think we have a
| pretty comprehensive list of units that are supported by now in
| Numbat [1].
|
| [1] https://numbat.dev/doc/list-units.html
| kragen wrote:
| the classic problem for such number systems is linear algebra
| https://yosefk.com/blog/can-your-static-type-system-handle-l...
|
| the issue is that each column and each row of a matrix can have
| different units. worse, gauss-jordan elimination chooses which
| rows to operate on dynamically. there is eventually a solution to
| this problem in c++ far down the comments thread
|
| i don't see anything in https://numbat.dev/doc/type-system.html
| about aggregate types such as vectors, matrices, maps, arrays,
| lists, trees, records, etc., though it does have a suggestively
| named scalar type. i wonder how it handles this sort of thing
| sharkdp wrote:
| No, we do not have aggregate types in Numbat yet. But it is
| definitely something I would like to support.
|
| Note that it is possible to construct a type system solution to
| this problem (vectors/matrices with non-uniform units). A
| colleague of mine has an excellent talk on this:
| https://www.youtube.com/watch?v=SLSTS-EvOx4
|
| By 'Scalar', in the document you referenced, we mean a
| dimensionless quantity. Not a scalar in the scalar-vector-
| matrix-tensor sense. Maybe I should rethink that notation.
| kragen wrote:
| thanks, i'll take a look
|
| i know it's _possible_ (even in c++ apparently) but so far it
| seems _difficult_
| spott wrote:
| Interesting article... though to be honest, I'm not sure I buy
| the premise.
|
| In the article, he states: "Let's call the matrix of all (xi 1)
| `X` and let's call the vector of all yi `Y`", and then states
| that the units of `X` are (m 1).
|
| But if you instead say the units of `X` are just m, the "1" is
| in units "m", then the problem goes away, the whole matrix has
| the same units ("m"), and everything works fine.
|
| I'll be honest in that I've never thought of a matrix having
| multiple units per column... and I can't think of any example
| where you aren't just putting the units in the wrong place. Let
| me know if you have a concrete example that might work.
| adastra22 wrote:
| If you multiply by a transform where the first entry is 1,
| the second entry is d/dx, the third entry is d^2/dx^2, etc.
| You will get a different unit for each entry of the vector.
|
| Also most of economics consists of linear systems with non
| homogeneous units. The first entry could be bushels of wheat,
| the next demand for steel, etc.
| kragen wrote:
| i hadn't thought of it either before auditing an introductory
| numerical methods class, but in retrospect the page i linked
| does explain this, repeatedly, in the comments; i just didn't
| understand it at the time
|
| basically it's very very common
| youssefabdelm wrote:
| > On the other hand, 3 months + 2 lightyears is ill-typed,
| because the right-hand side is of type Length. You can change
| 'years' to 'lightyears' in the example above to see the resulting
| compiler error.
|
| Why not both? Make lightyears both Length and Time
| mlhpdx wrote:
| Modeling compile-time units was one of the memes of c++ 11. One
| of many examples:
|
| https://benjaminjurke.com/content/articles/2015/compile-time...
| nutate wrote:
| First project I've ever seen that made me instantly sponsor it.
| Then to only find out you wrote fd and hexyl and some other
| classics. Great work.
| merelysounds wrote:
| Impressive!
|
| One thing I find unintuitive is the implementation of variable
| length units (like months or years) as an averaged constant. Then
| again, perhaps that's the point - and e.g. working with months
| without specifying a calendar is just unintuitive.
| benhurmarcel wrote:
| Apparently this replaces https://github.com/sharkdp/insect
| sharkdp wrote:
| Yes. If you want to know more, you can read about it here:
| https://github.com/sharkdp/numbat/blob/master/assets/reasons...
___________________________________________________________________
(page generated 2023-11-16 23:01 UTC)