Simon Peyton Jones

Well, you see, that is pretty obvious, isn't it?

You want to make the platform-specific bit as small as possible.

You would like to have, as it were, like a generic architecture, one that can do addition and has a program counter and a stack and so forth.

That's all C minus minus is.

It's just a portable assembly language.

And then you say, oh, the nitty gritty of, you know, whether you have double precision add and set the floating point bit here and there.

That, well, that's platform specific.

Core is itself statically typed.

You know, but in some ways it's surprising because no other compiler has this property.

No other production compiler.

By core is statically typed.

I don't just mean that the initial program was typed correct.

I mean that a core program, you can run a type checker on that.

I might say, why do you need to?

Because after all, if GHC is correct, it started with a type correct core program, because it came from a type correct Haskell program, assuming the de-sugar was right.

And all the optimizations, if they're right, will generate a type correct core program.

So why do you need a type checker?

Answer, to discover bugs in GHC.

Now, these are serious bugs.

If you ever take a type-correct call program and an optimization pass produces a type-incorrect call program, what will happen if we don't have the type checker for call?