Agda and GHC Haskell have a feature called "typed holes" that can enhance the workflow that you describe in the article. If you're not sure how to finish a definition, you can leave a "hole" in the expression where you are stuck, and the compiler will tell you what type you need to fulfill and list variables that might be helpful. Then, you can "fill" the typed hole with an expression, while possibly creating new holes. Thus, types can guide you as you incrementally build up an implementation.<p>Types let you to have a "dialogue" with the compiler. Programming in Agda is very much intended to be an interactive experience, via its Emacs mode.<p>Typed holes in GHC: <a href="https://wiki.haskell.org/GHC/Typed_holes" rel="nofollow">https://wiki.haskell.org/GHC/Typed_holes</a><p>Agda Emacs mode: <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html" rel="nofollow">https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.htm...</a><p>In the article, you compare the usage of types to guide you with test-driven development. There is actually a book called Type-Driven Development about using dependent types in the Idris language, although I have not read it. It is written by Edwin Brady, the creator of Idris. <a href="https://www.manning.com/books/type-driven-development-with-idris" rel="nofollow">https://www.manning.com/books/type-driven-development-with-i...</a>
Author here. I do practice TDD, which is where I think this thought came from. Types aren't exactly like tests, but we can use them for some of the same goals, such as constraining and influencing our implementations.<p>The example here may also be an example of development by "wishful thinking" (writing our implementations as if we had certain abstractions available), that is talked about in the SICP lectures.