The first time I heard about functional programming, someone told me "it's more reliable to code in a functional style because your type system is like a proof of correctness".
I recently learnt about the Curry-Howard (CH) correspondence and I think this is what he was using as a basis for his assertion about functional languages.
However, I have trouble understanding how far this leads to "more reliable programs".
Especially, here is my understanding:
- In the CH view, a function type
A -> Bis the same as an implication $A \implies B$ in some constructive view of logic, and so on... (union type, product of type, etc.)
- So if we end up being able to build an instance
tof a type
Tit means we used only the available function types / implications using the available variables / assumptions.
Still, there are many ways a program written this way could be incorrect :
- If I have several variables
c, ... of the same type
Aavailable, I may use a transformation
A -> Bon the wrong one.
- I may have different functions with the same signature
A -> Bbut different use cases, and the type system won't be able to detect if I use the wrong one.
My questions are:
- In practice, do functional programming languages enforce things like "there should be no more than one instance of a type" or some variant to avoid those kinds of errors ?
- Is there a theoretical background in which we enforce more restrictions on functional languages and give the "more reliable" a stronger meaning ?