Typed holes

Contents
  • Digging holes
  • Working incrementally
  • Errors into warnings
  • Refinement hole fits
  • Querying GHCi
  • History

Often while developing code, we find ourselves wanting to stick an undefinedAccording the docs, undefined is meant to give helpful errors, but somehow this hasn’t been implemented in GHC, as far as we know. in somewhere, a placeholder that will let the code compile even though some things aren’t implemented yet. But what if we had an undefined that also told the compiler to help us implement the function by giving us information about the types and telling us some options?

That’s what typed holes are for!

The term typed holes usually refers to holes left in expressions for the purpose of eliciting inferred type information from GHC. You can also leave holes in type signatures. We’ll compare those two techniques a bit in this article, but this will primarily be about holes at the term level.

Sign up for access to the full page, plus the complete archive and all the latest content.