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
Presuming you know Davies-Pfenning "A modal analysis of staged computation"?
1
3
Yeah! I think I forgot how these were related! I have a feeling I'd got my head around this before, and then forgot?
Quote Tweet
Replying to @haskell_cat and @davewripley
Yeah, that seems right! I guess that interpretation could match up with staged programming, in terms of being able to splice/run `Code A`s, to get an `A`? That *does* actually feel like constexpr the more I think about it! 
1
1
I think Andras was also trying to tell me this here:
Quote Tweet
Replying to @brendanzab
`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.
`Code` is something I struggle to get my head around for some reason – maybe I just need to use it more in practice. It just feels like something that happens ‘afterwards’…? I don't know why `constexpr`/`const fn`/`static`/`comptime` feels easier to wrap my head around… 😳
2