07:07 <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.

12:12 <cfbolz> BarrensZeppelin: I'm at a conference this week, feel like pinging me again on monday? should I look at your branch already?

12:13 <BarrensZeppelin> I'll do that. 👍 Yep, I think I've done the necessary changes to the tokenizer.

12:13 <cfbolz> amazing

14:12 <BarrensZeppelin> Are you there to present the pydrofoil paper? Gz on getting that published btw. 👏

18:34 <Julian> Hi hi.

18:35 <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

18:36 <Julian> Ah right, I'm not am I (allowed to modify a global).

18:37 <Julian> So I have to define a function and call it immediately if I just want some global r_dict? /me tries...

18:59 <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*)

19:00 <Julian> My r_dict would have had 4 things in it so some if/elif will do (https://github.com/Julian/rpylean/commit/37dd52ae5912ef5c775216a5d46c530a0fd5d6c6)

19:17 <mjacob> Julian: Is there a reason you chose RPython specifically for writing a type checker?

19:20 <Julian> mjacob: No :) -- or maybe? I dunno I wanted to see if a JIT would help at all.

19:20 <Julian> Which clearly I haven't answered yet as we only have it half implemented.

19:22 <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.

19:28 <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.

19:29 <Julian> Though I guess incrementally slurping in the things we type check will eventually be nice.

19:30 <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.

19:31 <Julian> Yes that sounds right.

20:19 <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.