Half-cooked thoughts about a proper module system for Lean 4
Conversation
Seeing as you were talking about metaprograms and Racket's phases, perhaps Klister's approach to 'stuck macros' would be interesting to look at, if you haven't seen it already. Not sure if it handles cross-module stuff though:
2
1
We have something like that, I think it's mentioned in their related work :) . No direct relation with phases though (afaik), this is about ordering expansion steps within a phase.
1
1
Ah sorry! Yeah, still getting my head around all of this stuff!
1
Btw, when you say 'module' do you mean a '.lean file'? ie. is there a 1:1 mapping between them?
Replying to
Oh yes, that is correct. I should have clarified that. Between existing support for namespaces and typeclasses and the unlikeliness of adding modules to the kernel, I don't see any place for finer-grained modules in Lean.
2
Yeah, I assumed that was the case - makes me a bit sad if I'm honest, but I understand!