Resources for building a Polymorphic Lambda Calculus compiler?

Hey all, apologies if this isn’t a good place to post this, but this board seems like a good intersection of folks interested in FP, type theory, and compilers (and obviously OCaml).

I’m currently trying to write a functional programming language in OCaml without formal knowledge of type theory or compilers (I don’t have a CS degree). I’ve been reading up as much as I can across a lot of different papers, github projects, and some books that I’ve found online. Slowly I think I’ve started to build some of the knowledge I may have gotten from a compilers course.

So far I’ve implemented a type checker for higher-kinded polymorphic lambda calculus (System F omega - code is here), but I’ve found it incredibly hard to find resources on going from this to a call-by-value compiled program. I decided to implement System F Omega because I read that it’s what one of Haskell’s intermediate representations are built upon. System F is a really painful term to google, and most resources I’ve found are about formal verification or are nigh impenetrable for a hobbyist.

Ideally i’d like to take a type-checked System-F-omega AST and output LLVM, Cranelift or webassembly IR, but I don’t know what steps I’m missing in the middle. I have read enough to know that I’ll probably need some kind of abstract machine, and need to somehow convert that to CPS or SSA form before I can get it to machine code. I have heard about a few different abstract machines (Like G-Machine, SECD, Krivine), and have read about the CPS transform, but I don’t think I have enough knowledge or context to put them all together in practice.

I have found plenty of resources on the type-inference side of things so I don’t think that’ll be a big issue (famous last words :sweat_smile:).

Does anyone know any resources I should check out related to the above? Again, apologies for the somewhat off-topic post.

Have you seen “Implementing functional languages: a tutorial”? Might have some more of the practical side that you’re looking for.

1 Like

I think you probably can’t go wrong by having a read of:

J. Gregory Morrisett, David Walker, Karl Crary, Neal Glew:
From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3): 527-568 (1999)

Also, while not about the type systems you mention, the Rabbit and series of “Lambda the Ultimate” papers are excellent.

2 Likes

Hi, maybe this is a good starting point or at least useful reading:

Good luck!

2 Likes

Thanks for the suggestions everyone! These are an awesome start and should help a tonne!

I think Appel’s famous book Compiling with Continuations is still practically enough for compiling call by value typed programs to assembly using CPS along.

2 Likes

…stumbled upon RETROSPECTIVE:The Essence of Compiling with Continuations and it
seemed relevant

disclaimer: I don’t know what I’m talking about %)

2 Likes