Mind is getting blown by multi-stage programming! Does anyone know of any simple examples of it being used as a way of doing offline partial evaluation in compilation? Most of the stuff I see is for run-time code generation. 🤔
Conversation
There's this paper about static staging: cs.utexas.edu/users/mckinley
That said, it isn't clear to me what the difference is between typed macros and static staging -- syntactic flexibility vs rigidity?
2
1
I think there is some correspondence, but I don't know. The annoying thing about full spectrum dependent types is that you lose the phase information that is present in traditional languages, so it's hard to compile things like type parameters and constant parameters efficiently.
2
Replying to
Yeah, I think you need to use something other than the 'use count'. I believe McBride was talking about this in his presentation on 'Worldly Type Systems' - it's taken a long time for me to realise that he was talking about multi-stage programming here:
My other worry is how this would interact with other notions like usage count, sharing count, opaqueness, effects, and other things you want to express for systems programming purposes. 🤔
1
Show replies
Replying to
QTT lets you instantiate the semi ring to e.g. the tropical numbers to describe staging
1
2
Yeah, I wasn't sure if this was still called QTT, or if QTT just referred to the semiring version. Also, can QTT be used for compilation purposes? I seem to remember that there were some limitations claimed by Andreas Abel, but not sure if it is relevant: cse.chalmers.se/~abela/types18
1
Show replies