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