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 ?
  • $\begingroup$ Curry-Howard applies to any program, stateful or functional, any program can be seen as a mapping from initial state or value to final state or value. Also if you're going to reason about terms like "the Curry Howard correspondence", quote a definition & show that your claims follow by applying it. (And a vague informal simile someone told you is not a definition or claim.) "Functional programming" doesn't even have single precise meaning. And if you gave one it's not clear how it couldn't be applied to what could reasonably be called non-functional programming. $\endgroup$ – philipxy Jan 18 at 20:17
  • 1
    $\begingroup$ @philipxy: your comments about stateful computations and Curry-Howard are at least misleading, because one has to modify CH to account for state in a non-trivial way. The usual CH applies to (variants of) dependent type theory, so it's pretty clear what is meant by "functional programming" in this context. The rest of the comment is just condescending and unhelpful. When a person is trying to understand a new concept, they cannot "quote a definition & show that the claim follow by applying it". If they could do that, the would not be asking the question in the first place. $\endgroup$ – Andrej Bauer Jan 18 at 20:28
  • $\begingroup$ @Andrej Bauer My comment is helpful & your characterization of my attitude is unjustified & wrong. $\endgroup$ – philipxy Jan 18 at 20:38
  • $\begingroup$ We'll let the internet decide, shall we? $\endgroup$ – Andrej Bauer Jan 18 at 22:23
  • $\begingroup$ I believe that the claim by your someone is unsubstantiated. A static type system for any programming language provides some correctness guarantees, for example, that a boolean will not be added to a number. Type systems for (functional) programming languages in the ML family may be extended to express statements and proofs of higher-order logic. I do not think this makes these languages more apt for programming since you can program and prove in different languages. $\endgroup$ – beroal Jan 28 at 18:00

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.

  • $\begingroup$ Is there some language implementing that kind of constructs with dependent types that you would recommend for a beginner to look at ? $\endgroup$ – Weier Jan 18 at 21:26
  • 1
    $\begingroup$ Idris or Agda come to mind. $\endgroup$ – Andrej Bauer Jan 18 at 22:22
  • $\begingroup$ The terms "write documentation in English" and "keep function properties in our heads" exaggerate the real life, where the documentation and the properties are written in machine-readable/executable/verifiable forms of contracts (aka preconditions, postconditions, invariants, etc.). In that case strong type checking is replaced with verification. $\endgroup$ – Alexander Kogtenkov Jan 19 at 14:02
  • 1
    $\begingroup$ @AlexanderKogtenkov: Let's not discuss what % of real-life software has machine-readable contracts. What you describe is quite similar in spirit to dependent programming, but with different overall organization: in dependent programming the assertions are part of the code (and generally cannot be seprated from the code easily), whereas in verification they annotate the code (and can be just deleted if so desired). Perhaps you can suggest to the OP some verification tools that will demonstrate how this alternative approach works? $\endgroup$ – Andrej Bauer Jan 19 at 14:34
  • $\begingroup$ @AndrejBauer Talking about code associated with dependent types (e.g. the one that checks that a sequence is sorted) I believe it is thrown away like contracts after successful verification (because the valid order of elements is guaranteed by the suitable type). Some examples of verification tools and languages are collected at rise4fun: see Dafny, Chalice, Vcc. And I agree that dependent type checks are mandatory, whereas verification is optional, though I would not be surprised to see an "optimistic type checker" that ignores the code. $\endgroup$ – Alexander Kogtenkov Jan 19 at 18:12

Your Answer

