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
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
Yeah, not talking about unification/inference - eg. all implicit type applications are explicitly applied at this point. We're not carrying around extraneous typing annotations though - we instead synthesizing from existing stuff we know about.
1
Replying to
The other issue is that as far as I know, going from a bidirectional core language to a fully explicit core language would require me to 'weaken' values back to the source syntax rather than going via readback, which is non-trivial I think? I could be wrong though.
Replying to
TBH the latter thing is more what I'm trying to avoid here, seeing as my language is not going to be used for heavy-duty theorem proving - it's just a data description language. But ultimately I'd also like to be able to figure out this to avoid the size blowup too.
1
This is one of the reasons why I was avoiding explicit types in my core language, for what it's worth: twitter.com/brendanzab/sta - seems to me like its actually the size blowup problem again though 😅
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
Show replies