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.
https://phys.org/news/2012-04-physicists-abolish-fourth-dime...
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.
I Special Relativity you have many cuadrivectors, for example:
* time-space (t, x, y, z)
* energy-omentum (E, px, py, pz)
* Electromagnetic Potencial (V, Ax, Ay, Az)
and even a few 4x4 matices like the electric and magnetic fields together.
All of them change with the same equations. You can't break (t, x, y, z) and keep all the other.
And there are extensions to particle physics that mix Special Relativity and Quantum Mechanics that use the same equations, and they have an agreement of theory and experiment of 8 digits. You can't break (t, x, y, z) and keep all the other!
Also, the paper is published in a journal I never heard about. It's impossible to be sure, but it has a lot of single author articles that is a big red flag, and the titles of the other articles are too weird (Nobel price or crackpot, nothing in between).
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]
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.
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.
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.
Yes. This is also how it is defined: https://github.com/sharkdp/numbat/blob/ba9e97b1fbf6353d24695...
The calculation above is showing a rounded result (6 significant digits by default).
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?
[1]: https://numbat.dev
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
And it is not open source.
>>> 1 day + 1 month
1 day + 1 month
= 31.4369 day >>> 1 month -> seconds
= 2_629_746 s [Time]
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?
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].
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.
Using averaged constants like this isn't applicable to all use-cases, but has the virtues of being simple and easy to reason about.
IMO they did exactly the right thing by not trying to shoehorn an endless supply of complexity and pain into their language's type system. Users who do need to deal with date math can use a library.
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?
https://github.com/sharkdp/numbat/blob/786512175b99c195a7d5b...
https://benjaminjurke.com/content/articles/2015/compile-time...
Why not both? Make lightyears both Length and Time
https://learn.microsoft.com/en-us/dotnet/fsharp/language-ref...
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!
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
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.
True: https://frinklang.org/faq.html#OpenSource
Thanks for sharing Numbat with us.
It looks great!
https://gcc.gnu.org/onlinedocs/gcc-4.9.4/gnat_ugn_unw/Perfor...
If rust ever gets more complete const generics, then things like tiny-uom might work.
- 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.
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.
i know it's possible (even in c++ apparently) but so far it seems difficult
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.
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.
basically it's very very common
> 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.
It's fine these days. https://tshort.github.io/WebAssemblyCompiler.jl/stable/examp...
I think the biggest issue with unit systems though is that algorithms are not generally unitful. I develop the Julia SciML solvers (https://docs.sciml.ai/Overview/stable/) and there's certain pieces like the initial dt calculation of an ODE solver which are not canonically correct in a unitful sense. So there's certain pieces where you have to opt out of unit checks which gets a bit messy. But other than that Unitful.jl is fine, and that's an algorithmic thing not a unit package thing.
how does unchained handle gaussian elimination
x²
x÷y
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).
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?
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
Error: type mismatch: got 'Joule' for '...' but expected 'Newton = Alias'
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).
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.
Exactly. Which is why trigonometric functions in Numbat have the signature
cos(x: Scalar) -> Scalar
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.
Degrees follow a similar argument.
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.
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%283%29%E2%8F%8Ecos%2830+deg%29%E2%...
We also have 'sidereal_day' equal to '23.9345 hours', and if you believe it is useful, we can also add 'sidereal_years'.
Chronological Time units and Calendrical Time units... These are fundamentally different concepts that overlap a lot in day to day life but when you need to ensure technical accuracy, can be very different.
- Planck time, Stoney time, Second: Unambiguously valid for both chronological and calendrical usage. Since we define everything in terms of the second anyway it's basically the centre of the Venn diagram.
- Sidereal day: It isn't a fixed value over longer periods of time, getting longer at a rate on the order of 1.7 milliseconds per century [1], so a conversion of a short period like 7 sidereal days into seconds is going to be off by something like 3.26×10^-7 seconds which might be ok, particularly if you also track the precision of values to avoid introducing false precision in the output, since you can then truncate the precision to above the error margin for a calculation like this one and treat it unambiguously as valid for both calendrical and chronological purposes.
- It's also worth noting since you mentioned it, the slight difference between Tropical year (seconds the earth takes to do a complete orbit around the sun), and Sidereal Year (seconds for the sun to fully traverse the astronomical ecliptic), the sidereal year is longer due to the precession of the equinoxes.
- Minute, Hour: These can vary in length up to a second if a leap second is accounted for, so while conventionally fine for chronological calculations as fixed multiples, don't have precise chronological values when used with calendar calculations. The exact number of minutes between now and 2030 is fixed, but the number of seconds in those minutes is not.
- Day: In addition to leap seconds, the length of a calendar day also have to deal with the ambiguity of daylight savings time and are where the significant differences in calendrical calculations vs chronological calculations really start to kick in.
- Week, Fortnight: all the problems of days but magnified by 7 and fourteen respectively. Also, theres the concept of standard business weeks and ISO week calendars, where some years wind up with more weeks than others due to the ISO week related calendar rules.
- Month: Obvious problem... "which month?" theres quite a few less seconds in February than in October.
- Julian year, Gregorian year: These are conventionally defined by how many days they have and the leap day rules and then approximated to an average seconds value so you can "pave over" the problem here and a lot of people might not be as surprised as if you average the length of a day or a month.
- Decade, Century, Millennium: are all affected by leap day related rules, and over a given length of time you see the introduction of an unknown but sort of predictable number of leap seconds. So while you can average it down yet again, the problems of anything bigger than a day have reached the point where over a millennium you're dealing approximately 0.017 seconds of change in the rotation of the earth,
Doing this right is basically incompatible with doing this the easy way, I'd at least re-label the averaged time units to make the use of average approximations more obvious, and ideally I'd split the time types into calendrical and chronological, and use more sophisticated (and I'll be the first to admit, annoying to implement) calendar math for the chronological calculations.
[1] - Dennis D. McCarthy; Kenneth P. Seidelmann (18 September 2009). Time: From Earth Rotation to Atomic Physics. John Wiley & Sons. p. 232. ISBN 978-3-527-62795-0.
if your static type system can't handle that, it can't handle unit types for basic linear algebra subroutines
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).
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
Transform vectors like you mentioned can have an implicit 1 with the right units in them in order to make the vector have a consistent unit.
> Also most of economics consists of linear systems with non homogeneous units.
The system of equations needs to have some sort of unit consistency. Which means there is some way to split up the units to keep the matrices and vectors with consistent units or the math doesn’t actually make sense.
In input-output analysis in economics, for example, the elements of a vector represent the amounts of a commodity (coal, steel, electricity, etc.), and the columns of the demand matrix represent how much of each commodity is required to produce one unit of that commodity as output. So the type of row 1 is "kg of coal", the type of row 2 is "kg of steel", the type of row 3 is "kJ of energy", etc. Given this matrix and a vector representing the starting quantities, you can do some linear algebra to get a matrix representing how much of each quantity to allocate to each sector, and a vector representing the resulting output. The type of these vectors are "[kg Coal, kg Steel, kJ electricity, ...]"
I don't now how you can "have an implicit 1 with the right units in them in order to make the vector have a consistent unit" given this setup.
you can still imagine some kind of static analysis that gives you an error if you accidentally write an algorithm that might add kgs of steel to kilojoules, and which is sufficiently powerful to accept at least the commonly-used numerical algorithms; not just matrix multiply but, in your example, probably the simplex algorithm
(we could call that analysis a 'type system', but perhaps obviously, it is significantly different from the type systems we're most familiar with)
i agree that this doesn't end up with vectors of homogeneous types, but it does end up with vectors of the correct type, which might be what was meant by 'consistent'
maybe i don't understand what you're saying but it sounds like you don't understand the problem
it's not that the units are inconsistent in the sense of adding kilograms to kilojoules; they're just inhomogeneous
you have a potentially large matrix in which potentially every cell has different units. so type systems that require the matrix cells to all be of the same type aren't helpful unless that type is something machine-oriented like `real*8`
moreover this is intrinsic to the problem, or at least the decision to use linear algebra on the problem
an additional difficulty for things like *gemm or lu factorization is that you want them to be applicable to matrices of any size with any type of units of measurement, as long as they're consistent; so they're parametrically polymorphic over units of measurement
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
Because fundamentally you can’t correct for the reference frame if you can’t work out if your dealing with chronological or calendrical units. Calendrical units are in a weird liminal space outside of the earth reference frame. We measure the history of most deep space missions by earth reference frame mission elapsed time and do so by keeping a clock on earth and silently keeping records of the vehicle clock.. but on Mars we have a per mission Sol count that brings Mars time into the mix, and I know for a fact a lot of people neglect the barycentric gravity gradient difference between Earth and Mars because for literally 99.9% of things it doesn’t matter… but if you measure a transit of an Astronomical body from instruments on Mars and don’t deal with the relative reference frames your fractions of an arc second are basically pointless false precision.