Tech Talk: Type-directed compilation in the wild: Haskell and Core

Galois is pleased to host the following tech talk.
These talks are open to the interested public–please join us!
(There is no need to pre-register for the talk.)

Please note the unusual day for this talk; it is on Monday.

abstract:
Academic papers often describe typed calculi, but it is rare to find
one in a production compiler. Indeed, I think the Glasgow Haskell Compiler
(GHC) may be the only production compiler in the world that really has a
remorselessly statically-typed intermediate language, informally called “Core”,
or (when writing academic papers) the more respectable-sounding “System FC”.

As real compilers go, GHC’s Core language is tiny: it is a slight extension of
System F, with letrec, data types, and case expressions. Yet all of Haskell
(now a bit of a monster) gets translated into it. In the last few years we
have added one new feature to Core, namely typed (but erasable) coercions that
witness type equalities, which turn Core into a particular kind of
proof-carrying code. This single addition has opened the door to a range of
source-language extensions, such as GADTs and type families.

In this talk I’ll describe Core, and how it has affected GHC’s development over the last two decades, concentrating particularly on recent developments,
coercions, evidence, and type families.

To test your mettle I hope to end up with the problem we are currently
wrestling with: proving consistency of a non-terminating rewrite system with
non-left-linear rules.

bio:
Simon Peyton Jones, MA, MBCS, CEng, graduated from Trinity College Cambridge in 1980. After two years in industry, he spent seven years as a lecturer at
University College London, and nine years as a professor at Glasgow University, before moving to Microsoft Research (Cambridge) in 1998.

His main research interest is in functional programming languages, their
implementation, and their application. He has led a succession of research
projects focused around the design and implementation of production-quality
functional-language systems for both uniprocessors and parallel machines. He
was a key contributor to the design of the now-standard functional language
Haskell, and is the lead designer of the widely-used Glasgow Haskell Compiler
(GHC). He has written two textbooks about the implementation of functional
languages.

More generally, he is interested in language design, rich type systems,
software component architectures, compiler technology, code generation, runtime
systems, virtual machines, and garbage collection. He is particularly motivated
by direct use of principled theory to practical language design and
implementation — that’s one reason he loves functional programming so much.
His home page is at http://research.microsoft.com/~simonpj.