Curry–Howard correspondence and functional programming "reliability"

Question

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 -> B is 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 t of a type T it 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 a, b, c, ... of the same type A available, I may use a transformation A -> B on the wrong one.
• I may have different functions with the same signature A -> B but 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 ?

Answer 1

The dependent types allow you to specify what properties your function should have, not just what its domain and codomain are. This way it becomes impossible to accidentally use the wrong function.

For example, suppose we want a function that sorts lists (of integers). In ordinary programming we would ask for a value of type List → List, and then we would write documentation in English that says "and it is supposed to sort lists".

With dependent types, we would write down a fancier type:

Σ (f : List → List) Π (lst : List) isSorted(f lst) × isPermutation(lst, f lst)

(See below how one defines isSorted and isPermutation.) An element of this type is a pair (f, p) such that f : List → List and p is a function which takes as input any list lst and outputs a pair (q, r), such that: q is the proof that isSorted f lst and r is the proof that lst is a permutation of f lst. In other words, p proves that the output of f lst is precisely the sorted list lst.

If you think about it, it is impossible to accidentally use a non-sorting function. If you do, then you will not be able to also write down the proof that it really sorts lists.

In ordinary programming we are used to write down data and functions into the source code, but keep their properties in our heads. In dependent programming the properties are part of the source code, and so are the proof that those properties are satisfied.

P.S. We define isSorted : List → Type as

isSorted nil = True
isSorted (x :: lst) = (Π (y : int) . elementOf y lst → x ≤ y) × isSorted lst

It is a bit more annoying to define isPermutation, so I will not do it here.

Answer 2

The type system in FP languages helps you avoid a certain number of errors. The more you use various features of the type system, the more errors you can exclude.

For example, if you need the list of session IDs to be always non-empty, you can use a data type "non-empty list" and ensure at compile time that no place in the program will, by mistake, create an empty list as the list of session IDs.

If you are concerned that the function of type a -> a -> b should not confuse the two arguments, you can create two new types and use them instead of a. So, instead of a function of type String -> String -> IO String you write:

 newtype KafkaTopicForInput = KTFI String
 newtype KafkaTopicForOutput = KTFO String
 f :: KafkaTopicForInput -> KafkaTopicForOutput -> IO String

Then it is not possible to pass arguments to f in the wrong order.

There are other such tricks in the FP arsenal. If you use the State monad, you cannot accidentally forget to update the mutable state. If you use the Either monad, you cannot accidentally forget to handle an error situation.

The Curry-Howard correspondence ensures another type of correctness: that your program will not crash at runtime if it compiles without errors. In languages that do not fully follow the CH correspondence, one can write a program that will crash at runtime because the program appears to compute a value of some type but actually does not. (In the CH correspondence, the corresponding logical theorems are false but appear to be true because the logic is inconsistent and you can prove a false statement.)

At the same time, FP type systems typically will not help you write correct algorithms. If you need all session IDs to contain valid base-64 alphanumeric strings, the type system will not be able to help you, it's a very complicated condition. Other tools should be used to ensure that.