Simon Peyton Jones

We'll generate machine code and we'll run it and we'll get a segfault.

Now we have to backtrack from a particular test program that now crashes

all the way to back up the pipeline, up the pipeline, up the pipeline, up the pipeline.

Oh, it was this pass of GHC that was faulty.

That's super hard to do because, you know, you're getting out GDB on some runtime failure that is an indirect and perhaps distant consequence of the fact you just generated a type, you know, you had a bug in the optimizer.

So it is amazing to have a type checker for core.

Now, why does nobody else do this?

Well, it's because their intermediate language typically, and this I really am talking typically because I know of no other compiler that has this property, none, production compiler.

Typically, they're complex syntax trees decorated with all sorts of pragma information and things hanging onto it here and there.

And there's no type checker for it at all.

And there's no hope of one.

So I'm very proud of the fact that Core is statically typed.

And I also think the most delightful thing is that the way that it is statically typed, it is an implementation of something called System F. So System F, when I said Lambda Calculus, Lambda Calculus, as Alonzo Church had it, was untyped.

It had no type system at all.

But Girard defined something called System F, which is a statically typed lambda calculus, a rather powerful one.

And core is essentially System F. So he literally adopted something from the nerdy theoretical computer science, you know, logic community, logic of mathematics community, and adopted it directly in a production implementation.

So I'm very proud of that.

I think core is, and the fact that we can do, we have 35 years worth of development that has been not just not impeded, but actively aided by statically typed intermediate language is really a big marker in the ground.

So Haskell embodies one key idea.

Immutability changes everything.