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).
1
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
Right, if you don't want to cache the types from the typecheck phase, then you need to fuse the typecheck and code generation stages otherwise you'll duplicate a lot of type checking logic
1
1
Yeah, that is what I was stuck on - if I _had_ to run the type checker again during my next compiler phase. It seems hat you really need seems to be the target language's types, rather than the source language's types.
1
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
Replying to
Thanks for the link, I'll give it my full attention tomorrow. For now, I'm wondering if his talk of 'meaning-making' means that I should only cache types for checked terms.
1
1
Yeah I dunno! Still figuring this all out - haven’t yet delved too deep into that paper - it doesn’t really touch compilation alas.