Has anyone done used bidirectionally typed IRs for compilation before? If you have dependent types (or some sort of parametric polymorphism), does that mean you have to re-implement an evaluator for each type-directed compiler pass?
Conversation
Eg. I'm doing a compilation pass from my bidirectional PTS-style core language to a stratified language, but I need to know the types of function arguments to do so: twitter.com/brendanzab/sta. I'm guessing I might need to re-evaluate types to figure that out?
Quote Tweet
The paper sneakily leaves the generalization to a PTS (which is close to what I have in my core language) right until the end! 
twitter.com/brendanzab/sta
twitter.com/brendanzab/staShow this thread
1
Not sure if has any ideas - I was trying to go down the route of a bidirectionally typed IR based on what I read in “The types who say ‘ni’” 😅:
Quote Tweet
Replying to @brendanzab and @ielliott95
Read this in Conor McBride's Types Who Say Ni thing which is kind of motivating this - not a massive problem for me right now, but it would be neat to figure out how it works in practice! github.com/pigworker/Type
1
1
So, in some detective work going back into my prior state of mind, it seems like this thread is where I got scared off from using readback in my elaborator, which actually seems quite similar to what McBride is talking about in the above quote:
Quote Tweet
@andrasKovacs6 Running into an issue with my elaborator. It seems that I get lots of bloated definition when I elaborate to my core syntax - seemingly because `synth_term` unfolds variables to their definitions a bit too eagerly. Was wondering if you had any tips! cc. @derKha
Show this thread
1
1
Apparently, according to , using ‘glued evaluation’ might help here by allowing you to “read back terms smaller (close to the surface term they came from)”. This is implemented in smalltt and sixty:
• github.com/AndrasKovacs/s
• github.com/ollef/sixty/
1
2
If I understand correctly, this explains why can readback parameter types to core terms during elaboration without needing to worry about term-size blowup (which is what I was trying to avoid): github.com/ollef/sixty/bl
