Matthías on "Suggesting Valid Hole Fits for Typed-Holes" at TimeEdit

We're back after a (very) long hibernation! Come join us at TimeEdit for a talk on a brand new extension to Haskell. This time, we have the author of the paper himself give us the talk!

-------------------------------------------

Abstract

Type systems allow programmers to communicate a partial specification of their program to the compiler using types, which can then be used to check that the implementation matches the specification. But can the types be used to aid programmers during development? In this talk I describe the design and implementation of my lightweight and practical extension to the typed-holes of GHC, partially available in GHC 8.4, and fully available in GHC 8.6 and onwards. The extension improves user experience by adding a list of valid hole fits and refinement hole fits to the error message of typed-holes. By leveraging the type checker, these fits are selected from identifiers in scope such that if the hole is substituted with a valid hole fit, the resulting expression is guaranteed to type check.

Note: this talk is a dry-run of a talk I'll be giving at Haskell Symposium in St. Louis, of my paper titled "Suggesting Valid Hole Fits for Typed-Holes (Experience Report)" and available at https://mpg.is/papers/gissurarson2018suggesting.pdf

-------------------------------------------

About the Speaker

Matthías Páll Gissurarson (aka. "Tritlo") is a PhD student in the Functional Programming division of Chalmers. His interests include Magic: The Gathering, video games (DotA and grand strategy) and being an armchair philosopher. He's currently working on the programming model for the Octopi project, a platform to program secure IoT applications.