Suggesting Valid Substitutions For Typed Holes
summary
Extension accepted into GHC that uses the compiler’s typechecker to list actual identifiers and multi-argument constructions that fit a hole, not vague examples; it ranks suggestions by subsumption checking so exact and more general fits surface first, and it offers refinement substitutions (searching for small applied expressions) controllable by a flag. Demos show it typechecks lens and DCC examples, handles type families and advanced features, and the implementation ships on GHC 8.4 with further refinements on the 8.6 line.
AI-written summary · about
chapters (5)
- 0:00What are Valid Substitutions?
- 9:38Refinement Substitutions
- 23:32Constraints Demo
- 33:37Conclusion
- 36:42Sorting the Output
related talks
21mTotal Type Error Localization and Recovery with Holes
29mType Inference Techniques: Implementation and Formalization, Better Together
44mHazel: A Live Functional Programming Environment with Typed Holes
16mDigging for Fold: Synthesis-Aided API Discovery for Haskell
38mType System Foundations for Super-Charged Semantic Code Search
32mSeriously, The Haskell Type Checker is Your Friend
16mWe’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
24mLet the Scala compiler work for you