<BarrensZeppelin>
cfbolz: I think it'd make sense to check in now, if you're available and not away for holidays yet. π Any time outside 12-13 (CEST) works for me.
BarrensZeppelin has quit [Quit: BarrensZeppelin]
BarrensZeppelin1 has joined #pypy
BarrensZeppelin1 is now known as BarrensZeppelin
[Arfrever] has quit [Ping timeout: 265 seconds]
[Arfrever] has joined #pypy
<cfbolz>
BarrensZeppelin: I'm at a conference this week, feel like pinging me again on monday? should I look at your branch already?
<BarrensZeppelin>
I'll do that. π Yep, I think I've done the necessary changes to the tokenizer.
<cfbolz>
amazing
BarrensZeppelin has quit [Quit: BarrensZeppelin]
BarrensZeppelin has joined #pypy
<BarrensZeppelin>
Are you there to present the pydrofoil paper? Gz on getting that published btw. π
BarrensZeppelin has quit [Quit: Client closed]
Julian has joined #pypy
Julian has quit [Client Quit]
Julian has joined #pypy
<Julian>
Hi hi.
<Julian>
Am I not allowed to have an r_dict as a global in RPython? Or not allowed to modify one maybe? I have a literally 1 line diff (of course not my whole diff, just what I seem to have minimized to) which triggers a failure on this assertion: https://github.com/pypy/pypy/blob/main/rpython/rtyper/rbuiltin.py#L331
<Julian>
Ah right, I'm not am I (allowed to modify a global).
<Julian>
So I have to define a function and call it immediately if I just want some global r_dict? /me tries...
<Julian>
OK I gave up after I saw that doesn't work either for my case, so clearly I'm not understanding what is happening in that hop/lop translation step -- I can see the wrong type is being inferred but I don't understand why (or perhaps even *where*)
<mjacob>
Julian: Is there a reason you chose RPython specifically for writing a type checker?
<Julian>
mjacob: No :) -- or maybe? I dunno I wanted to see if a JIT would help at all.
<Julian>
Which clearly I haven't answered yet as we only have it half implemented.
<mjacob>
My next question would have been whether you plan to implement an interpreter as well. But it a dependent typed language you probably canβt write a type checker without writing an interpreter first.
<Julian>
mjacob: I don't 100% understand the nuance there in the (unasked :) question -- I'll say though what the thing actually interprets is some simple export format which just has the type checking information rather than actually interpreting the "real" vernacular language someone writes. I don't / haven't / don't plan on implemented any bytecode interpreter either if that's the question.
<Julian>
Though I guess incrementally slurping in the things we type check will eventually be nice.
<mjacob>
Iβm not super familiar with Lean, only with related languages. I would guess that Lean allows arbitrary (at least total) expressions. In that case you would need to evaluate these in order to type check, I think.
<Julian>
Yes that sounds right.
Julian has quit [Ping timeout: 244 seconds]
<korvo>
In case Julian reads logs: a prebuilt dict or r_dict can't change after translation, and r_dict is only useful when customizing equality/hashing. Also I've found that sometimes prebuilt dicts don't do exactly what I expect and usually what I want is to use rlib.unroll.unrolling_iterable on either the keys or items of a dict, *or* to allocate it at runtime as a local/instance instead.
* korvo
currently in the middle of a similar refactor