Nick Benton
Combining Static and Dynamic Types in Hack
Hack is the language that powers the 'business logic' of Facebook. It has evolved from PHP, most significantly via the addition of an expressive type system. Nearly all of our very large codebase is now statically typed but there are still places where type errors are supressed, which means we cannot fully trust the type information. We aim to achieve soundness for the whole codebase by introducing a novel form of sound gradual typing and using that to selectively weaken the claims made by some of the type annotations. This talk will describe how we combine static and dynamic typing in Hack without introducing costly new runtime checks or throwing away the benefits of our existing types, as well as an associated semantic soundness result formalised in the Coq proof assistant.
back to overview
Watch Recording
