sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
<achin>
it would be neat if all these examples had a "run" button that could immeditally run them in-browser
<sharkdp>
that's a great idea
<sharkdp>
It would also be cool to have a "godbolt"-like online editor for Numbat. Code on the left, automatically-updated result on the right.
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
sharkdp has quit [Remote host closed the connection]
sharkdp has joined #numbat
<achin>
how annoying would it be for numbat to say "the following variables have the necessary type" when reporting about a type hole? i'm guessing that for some holes, there may be dozens of matching variables in scope
<achin>
maybe there could be repl directives to turn a feature like that on/off
<sharkdp>
not annoying at all. I was just too lazy earlier to implement that feature, but I thought about it (GHC does something similar: "Valid hole fits include …")
<sharkdp>
And if we find no fits for type T, maybe we find some for T^-1 or T^2…
<achin>
in addition to just being a Cool Thing that you can do with numbat's type system, i feel like there's some neat educational uses for this
<achin>
like a student studying ohms law might type in "volts / ? -> ohms" and get a nice hint
<achin>
or maybe as a "formula finding tool", though it's not quite perfect for that. if i wanted to find the formual that relates frequency to wavelenght, i might try something like "Hz / ? -> meters", but the result of 'Length⁻¹ × Time⁻¹' isn't all that useful
<achin>
(seeing a unit with a negative 1 exponent would be a good indication that you should try again with the numerator and denominator flipped)
<sharkdp>
Please come up with more ideas like this! I really think that we can do some powerful things with type inference.
<sharkdp>
for your first use case "volts / ? -> ohms", I was thinking that we could maybe add a "?Type" syntax to add "holes" of a specified type.
<sharkdp>
Then that could also be written as "?Current / ? -> ?Resistance"
<sharkdp>
because it feels a bit weird having to switch between units and dimensions
<sharkdp>
?Type would be like std::declval<Type>() in C++, if anyone is familiar with that
<achin>
i like that idea
<sharkdp>
And as for the "find the formula" idea: I think we need an additional feature for that. We want something like a Buckingham-π-theorem-solver.
<sharkdp>
Something like relate(q1: T1, q2: T2, …), which would solve the equation T1^α1 * T2^α2 * … ~ 1
<sharkdp>
or maybe `construct<Energy>(mass, velocity)`. which would give you `mass velocity^2`
<achin>
hmm
<sharkdp>
both of these are not really definable (even as FFI function) in Numbat right now
<achin>
i guess my first two immediate thoughts are: 1) that sounds very useful, and 2) how can we pacakge this feature up in a way that doesn't get bogged down in confusing sytax
<sharkdp>
maybe we could support something like "mass^? * velocity^? -> joule"
<sharkdp>
or "… -> ?Energy"
<achin>
to me, there's something pleasent in re-using the arrow syntax to mean "help me take the thing on the left and turn it into the thing on the right"
<sharkdp>
agreed
<achin>
(which your two 'relate' and 'construct' examples don't quite have)
<sharkdp>
Using typed-hole syntax for the exponents might actually work. The type of these would be scalar. But we should be able to infer the *values* as well
<sharkdp>
(which might contain free variables, since there can be infinite solutions)
sharkdp has quit [Remote host closed the connection]