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
Replying to
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.
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.
1
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
Show replies