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?
Replying to
I use that 'later' point of view. The reason it fits is that you can't access the future until it actually happens. So once something is "code", it's opaque to you now. That helps motivate why abstract-interpretation-influenced annotations matter a lot.
1
3
Accessing the past from 'now' is also possible, if the past cooperates and leaves enough information around. [Type erasure is the exact opposite of that.]
1
4
Show replies
Replying to
I suspect this'd correspond to monadic ('later') vs. comonadic ('earlier') modalities. Neel Krishnaswami & co. had a paper on a comonadic modality for purity in an impure language (I think you've seen it?), maybe something like that? Dunno if it'd work out for staging.
1
1
Ahhh, I think I had it in Zotreo I think… was it “Recovering purity with comonads and capabilities”? Seems interesting, I can't remember having saved it tbh!
1
1
Show replies
Replying to
`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
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?
1
Show replies
Replying to
and I recently submitted a paper on this, trying to clarify what type of Code comes later and what type of Code is available now within guarded (cubical) type theory.
1
1
Here is the link to the preprint, btw josh-hs-ko.github.io/#publication-0
1