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
Replying to
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
1
Replying to
Aren't IRs typically fully explicitly typed? There's no inference going on, elaboration produces IR that has all the types. What's the reason for wanting inference for IR types? Hand-writing IR?
1
Ah sorry, I missed twitter.com/brendanzab/sta
Redundant type information causing blowup. That's an interesting problem to have. 😅
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
Show replies