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?

Eg. I& #39;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: https://twitter.com/brendanzab/status/1278860210770079744.">https://twitter.com/brendanza... I& #39;m guessing I might need to re-evaluate types to figure that out?

Not sure if @pigworker 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’” https://abs.twimg.com/emoji/v2/... draggable="false" alt="😅" title="Lächelndes Gesicht mit offenem Mund und Angstschweiß" aria-label="Emoji: Lächelndes Gesicht mit offenem Mund und Angstschweiß">: https://twitter.com/brendanzab/status/1163979356030558209">https://twitter.com/brendanza...

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: https://twitter.com/brendanzab/status/1120190725184872448">https://twitter.com/brendanza...

Apparently, according to @ollfredo, 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:

• https://github.com/AndrasKovacs/smalltt/
•">https://github.com/AndrasKov... https://github.com/ollef/sixty/ ">https://github.com/ollef/six...

If I understand correctly, this explains why @ollfredo 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): #L796">https://github.com/ollef/sixty/blob/f840ec29b0820f25e246671c6253263324f04078/src/Elaboration.hs #L796">https://github.com/ollef/six...