In this talk, Andor Penzes shows how to combine emerging technologies of functional programming. Idris is a dependently typed programming language, which makes it as a sharp tool in the programmer’s hand. A very good fit to modeling complex domains with high accuracy. Idris has a plugin architecture for the code generation, which allows engineers to implement code generations for even exotic technologies. Penzes' exotic backend is the code generator of the Glasgow Haskell Compiler. How to implement such a thing?
The pieces of the puzzle are: a) External STG (ExtSTG), which is a clone of the intermediate representation of the Glasgow Haskell Compiler. b) An interpreter for ExtSTG which is formalized and written in Haskell. c) GHC-WPC which is a modified GHC compiler that can compile binaries from ExtSTG. d) The architecture of the Idris2 compiler back-end.
The main focus of the talk is how to write Idris2 back-end. The take-away is how simple are the intermediate representation of the compilers when they are formalized in functional programming, and a recipe for your Idris2 backend.