isnt this how scheme work? 'composable and compilable macro - you want it when?'
This Tweet was deleted by the Tweet author. Learn more
Conversation
This Tweet was deleted by the Tweet author. Learn more
yes, there are several examples of that in old work of Walid Taha and Tim Sheard for instance dl.acm.org/doi/abs/10.114. probably doesn't match what you want, but there was quite a lot of work then
1
1
As far as I know, their work did not go quite far enough. Sheard (2001) mentions the remaining challenges; in particular, the analysis of quoted code.
2
1
The most relevant work in my opinion f starts with and Pfenning on S4 (2001), then Nanevski, Pfenning, and Pientka on CMTT (2007), then Pientka and friends on Beluga, and most recently, Pientka and friends on Moebius.
Quote Tweet
Replying to @jjcarett2 and @TaliaRinger
Still hoping to solve this with a beautiful language that contains arbitrarily many metalevels. Unless someone else solves it first. Have you seen Moebius? arxiv.org/abs/2111.08099
1
2
This Tweet was deleted by the Tweet author. Learn more
Indeed. To my mind, the stratification is orthogonal to other type system features, as long as they remain predicative. I have been trying to build a simply typed system first, but having dependent types may actually simplify some things, and would be desirable anyway.
2
2
This Tweet was deleted by the Tweet author. Learn more
What is sad about de bruijn + nbe? Not sure how it works in the metatheory, but for implementations it seems to be pretty great!
This Tweet was deleted by the Tweet author. Learn more
Ahh gotcha. Yeah I've never played with lemmas about this stuff because my brain is like, a grain of sand.
Key to making it nice in implementations is to use de Bruijn levels in the semantic domain. That was such a helpful thing to learn for me.