Starting to get my head around compiling! It's fun! Trying to take a bidirectionally typed language and convert it into a reasonable Rust API. Kind of has the same energy as these little molecular machines that read/replicate DNA… tearing apart a program and reconstructing it.
Conversation
It's taken a bit to get my head around... it seems there's lots of similarities to elaboration (where you take the concrete syntax and turn it into the core language, checking that it's well-typed in the process).
Replying to
One thing I had to get my head around was how to compile a bidirectionally typed core language. You end up making a bidirectional compiler too:
fn synth(&Context, &source::Term) -> (target::Term, target::Type)
fn check(&Context, &source::Term, &target::Type) -> target::Term
1
2