Collaborating with your computer using typed holes!

on YouTube ↗09m

" summary

Demos show typed holes in Python, Haskell and Agda, with editor integration and a proof-search engine that synthesizes code from holes; a dependent-vector example uses type-level lengths to prevent a common bug and the tool fills cases, compiles and actually runs; examples contrast Python’s silent failures with Haskell’s type-driven suggestions and Agda’s stronger guarantees; mentions Sketch and SMT-based synthesis as research directions and reports what concretely worked and where limits remain.

AI-written summary · about

" chapters (4)

1. 0:00Introduction
2. 1:52The Problem
3. 2:18In Practice
4. 7:58Conclusion

" related talks

• 31mTaming the Duck with Type HintsBrian Danilko · PyCon AU 2023
• 28mMind the gap! Why static typing requires more than just adding annotationsJia Chen, Steven Troxler · PyCon US 2026
• 29mSyntax Hijacking: Genius or Evil?Tennessee J Leeuwenburg · PyCon AU 2017
• 03h 40mTypingCarl Meyer, Jukka Lehtosalo, Jia Chen, Pradeep Kumar Srinivasan, Maggie Moss, David Foster · PyCon US 2021
• 32mType-checked Python in the real worldCarl Meyer · PyCon 2018
• 47mWhat's so hard about writing a type checker? A tour of tyCarl Meyer · PyCon US 2026
• 31mAdventures in not writing testsAndy Fundinger · PyData NYC 2023
• 32mMore testing with fewer testsClinton Roy · PyCon AU 2016