GHC’s typed intermediate language

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.