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.

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.

Typed holes in GHC: https://wiki.haskell.org/GHC/Typed_holes

Agda Emacs mode: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.htm...

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. https://www.manning.com/books/type-driven-development-with-i...

The idea of a type hole sounds really nice! Also, I hadn’t thought of Idris, but it makes sense that the more advanced a type system, the more they can take over for tests.

Have you heard of the Curry-Howard correspondence [0]? This states that a type system is actually a logical system. The types are propositions (logical statements) and their terms (the expressions of that type) are proofs. It's a straightforward syntactic correspondence:

- A -> B (Function type) and A => B (Logical implication)

- A * B (Product/Tuple type) and A /\ B (Logical conjunction)

- A + B (Sum/Tagged union type) and A \/ B (Logical disjunction)

Proving that A implies B is the same thing as writing a function that takes a proof of A and returns a proof of B. Proving the logical conjunction of A and B is the same thing as pairing together a proof of A and a proof of B.

So writing a definition that has a certain type is the same thing as proving a theorem.

Dependent types [1], which Coq, Agda, and Idris have, further the Curry-Howard correspondence. With dependent types, you can mention programs inside types and therefore express theorems about programs. You have:

- The dependent function type (x : A) -> B(x), where the return type B(x) is a function of the input x.

This is the same thing as universal quantification, "for all x of type A, B(x) holds."

- The dependent tuple type (x : A) B(x), where the type of the second element is a function of the first element x.

This is the same thing as existential quantification, "there exists an x of type A where B(x) holds."

So with dependent types, you can write mathematical proofs about programs. For example, you can show that a binary operation is commutative. Another good example is the "vector" type [2], which is like the functional-style linked list type, but parameterized over a length. Thus, you can prove that an index out-of-bounds error cannot happen. If you want to learn more about the theory, keywords to search up are "constructive math/proof," "intuitionalistic logic," and "Martin-Lof/intuitionalistic type theory."

[0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

[1] https://en.wikipedia.org/wiki/Dependent_type

[2] https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...

Very interesting, and I'd never heard of Curry-Howard correspondence. I've also always wondered how dependent types worked conceptually (as in, what's going on there, what are we proving, etc).

Thanks for the insights and the links!

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.

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.