Looking for a talk where you can learn about both Haskell and Type Theory?
At F(by) Conference, Vitaly Bragilevsky showed us how theory can be fruitful and exciting and that Haskell can be seen from many points of view.
Haskell and Type Theory: Better Together
Haskell can be seen from many points of view: you can build web services with it or study category theory. My favourite one is Haskel as a practical application of a type theory, which is a lovely piece of theoretical computer science by itself. Why not see how they work together?
Type theory is used in GHC to compile Haskell code. I'll first present lambda calculus and several type systems over it and then continue on with the demonstration how high-level code in Haskell is translated into the Core, intermediate language inside GHC, which is, in fact, a modest extension of Girard's System F. The talk is going to be split in half: 50% of type theory and 50% of Haskell and GHC internals.
I don't expect any prior knowledge of type theory, basic acquaintance with Haskell will be useful to understand what is going on in the second part of the talk. The main idea of the talk is to justify the fact that theory can be quite fruitful and exciting.
This talk was given by Vitaly Bragilevsky at F(by) Conference 2018.