Types Can Be Like Tests

- 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...