Introduction to Dependent Types with Idris: Encoding Program Proofs in Types

Conclusion

You’ve seen how powerful types are. They allow you to put additional constraints on values. This helps with reasoning about your programs since a whole class of non-valid programs will not be accepted by the type checker. For example, looking at the following function, you immediately know by its type that it returns a natural number:

1  f : Nat -> Nat

2  f _ = 6

Note that there are many constructors (proofs) for Nat. For example, you also have f _ = 7. Depending on whether you need 6 or 7 in practice has to be additionally checked. But you’re certain that it’s a natural number (by the type).

Most programming languages that have a type system have the same expressive power as that of propositional logic (no quantifiers). Dependent types ...