Does staged programming correspond to something like a ‘later’ modality? I'm wondering if you could flip things around, and use an ‘earlier’ modality to get something that looks a bit more like `constexpr`/`const fn`/`comptime` in C++, D, Rust, Zig, etc… 🤔
Conversation
I've always found that using a `Code` type for ‘later’ stuff (if that is indeed an acceptable way of looking at it) is a bit of a weird perspective outside of macros… but this is a familiarity thing? Would be kind of cool if both perspectives could interoperate somehow?
4
3
`comptime` and `constexpr`, to their sound & side-effect-free extent, are just a different flavor of `Code`. It's two equivalent presentations of 2LTT, one with explicit lifting and one with implicit lifting and restricted eliminators.
1
1
3
Replying to
I guess as a programmer it seems like an interesting change in perspective/ergonomics, where you are saying “this is computed before the code I am currently writing”. And yeah, you can't inspect the code of that stuff you are depending on, because it has already run… I think?
Yeah. Ux wise you may want user to have “Earlier a”, but in some sense there’s always a corresponding Code a, Later a