Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Show HN: Numbat – A programming language with physical dimensions as types

numbat.dev

Post reply on HN
Print view View original

111–120 of 122 posts

Re: Show HN: Numbat – A programming language with physical dimensions as types

#111

Post by kragen »

V1ndaar wrote: post #104
kragen wrote: post #84

Earlier quoted context omitted.

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

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,…

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

Re: Show HN: Numbat – A programming language with physical dimensions as types

#112

Post by kragen »

adastra22 wrote: post #100
spott wrote: post #97

Earlier quoted context omitted.

One way to think of this is that there are always multiple ways to break up the units when moving a system of equations into matrix form. What I’m trying to say is that there is always one way to break up the units that leads to matrices and vectors with a consistent unit. 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. > Als…

I don't understand the point you are making. These systems are intrinsically non-homogeneous in their typing. 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…

being implicitly non-homogeneous doesn't mean they're logically intractable

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'

Re: Show HN: Numbat – A programming language with physical dimensions as types

#113

Post by techdragon »

joshuanapoli wrote: post #106
techdragon wrote: post #99

Earlier quoted context omitted.

Ok so I did some reading and I like what I see, its important however to properly disambiguate between the two kinds of time units. 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 an…

The entire type system needs to be parameterized by the inertial frame of reference, too.

Some people may think you’re tossing out a sarcastic joke here… but unambiguously fuck yes … because doing this kind of preemptive typing, the forward thinking to “frame of reference” is basically the next step after overhauling everything to disambiguate between calendrical and chronological timekeeping and units…

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.

Re: Show HN: Numbat – A programming language with physical dimensions as types

#114

Post by runamuck »

bertil wrote: post #110
runamuck wrote: post #109

Earlier quoted context omitted.

The latter. FYI - Han Solo makes that mistake in the Original Star Wars (A New Hope).

Han Solo’s quote makes sense if you understand it as a unit of distance, optimized by the onboard computer to be as short as possible, by dodging black holes, and therefore fast.

Aha, Lucas claims he meant distance too.

Re: Show HN: Numbat – A programming language with physical dimensions as types

#115

Post by V1ndaar »

kragen wrote: post #111
V1ndaar wrote: post #104

Earlier quoted context omitted.

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,…

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

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

Re: Show HN: Numbat – A programming language with physical dimensions as types

#116

Post by kragen »

spott wrote: post #97
adastra22 wrote: post #73

Earlier quoted context omitted.

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.

One way to think of this is that there are always multiple ways to break up the units when moving a system of equations into matrix form. What I’m trying to say is that there is always one way to break up the units that leads to matrices and vectors with a consistent unit. 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. > Als…

> there is always one way to break up the units that leads to matrices and vectors with a consistent unit.

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

Re: Show HN: Numbat – A programming language with physical dimensions as types

#117

Post by kragen »

V1ndaar wrote: post #115
kragen wrote: post #111

Earlier quoted context omitted.

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

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

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

Re: Show HN: Numbat – A programming language with physical dimensions as types

#118

Post by adastra22 »

kragen wrote: post #112
adastra22 wrote: post #100

Earlier quoted context omitted.

I don't understand the point you are making. These systems are intrinsically non-homogeneous in their typing. 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…

being implicitly non-homogeneous doesn't mean they're logically intractable 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…

Yes, ok I agree with this.

Re: Show HN: Numbat – A programming language with physical dimensions as types

#119

Post by joshuanapoli »

techdragon wrote: post #113
joshuanapoli wrote: post #106

Earlier quoted context omitted.

The entire type system needs to be parameterized by the inertial frame of reference, too.

Some people may think you’re tossing out a sarcastic joke here… but unambiguously fuck yes … because doing this kind of preemptive typing, the forward thinking to “frame of reference” is basically the next step after overhauling everything to disambiguate between calendrical and chronological timekeeping and units… Because fundamentally you can’t correct for the reference frame if you can’t work out if your dealing w…

It would be fun to play an interstellar mashup of Sid Meyer’s Civilization and Kerbal Space Program.

Re: Show HN: Numbat – A programming language with physical dimensions as types

#120

Post by thriftwy »

joshuanapoli wrote: post #119
techdragon wrote: post #113

Earlier quoted context omitted.

Some people may think you’re tossing out a sarcastic joke here… but unambiguously fuck yes … because doing this kind of preemptive typing, the forward thinking to “frame of reference” is basically the next step after overhauling everything to disambiguate between calendrical and chronological timekeeping and units… Because fundamentally you can’t correct for the reference frame if you can’t work out if your dealing w…

It would be fun to play an interstellar mashup of Sid Meyer’s Civilization and Kerbal Space Program.

Isn't that Sid Meyer's Alpha Centauri?
Post reply on HN