In his final talk, Simon Peyton Jones will explain GHC’s intermediate language: System FC
In GHC, Haskell is typechecked and desugared into an intermediate language with only 10 operators (and has been like that for 22 years!)
Having a small IL is great, since conde generization and optimization only handle a small language, but there are downsides too, since debugging is harder. (however as Simon says “you don’t need debugging, if it type-checks, it works” :)) The solution to this is using a typed intermediate language. Transformation is robust (ie if the term is well typed, then the transformed term is well typed):
It is easy to maintain types with simple, local rules.
But, what about GADT’s?
They lead to problems if we have right-hand sides of pattern matching rules, since they assume a certain type
The pattern matching actually serves as a witness in the scope.
These evidences can be composed again with rules, like identity or transitivity. This is called evidence parsing and has it’s own rules.
It was great to see some Haskell again and in a lot of more depth than I have seen before. It is also cool to see how many research is still done on Haskell, how it keeps evolving and how elements of Haskell end up in commercial languages.
Images taken from the slides.