Is Wadler's 'Theorems for Free' as general as Design By Contract for establishing correctness?

Question

Philip Wadler has written a brilliant paper called 'Theorems for Free'. The big idea is that you can use types to reason about your program, and even prove simple theorems about your program.

We see these ideas about types applied in the Haskell language.

At very roughly the same time period - we have an idea from Betrand Meyer called 'Design By Contract'- which is most notably implemented in the Eiffel Language. This has the following features:

• routine preconditions
• routine postconditions
• class invariants
• check instructions (like assert)
• loop invariants

The idea behind Design by Contract is software designers should define formal, precise and verifiable interface specifications for software components, which extend the ordinary definition of abstract data types with preconditions, postconditions and invariants.

Now many claim that using 'Types' in your programs leads to 'more correct programs' (via the Howard Curry Correspondence). From what I can see - even the most advanced use of Dependent Typing in Idris and Scala is limited to Sum Types and list lengths (correct me if I'm wrong).

By contrast - the power of 'Design By Contract' in establishing the correctness of my program is more general and more powerful. (Albeit not necessarily at compile-time - but at test time). I can for example establish in my banking program that all deposits are positive, and all reported account balances are positive.

The point being - types have a fascinating future of possibilities, and are enormously powerful and compile time - but right now their practical application seems limited.

My question is: is design by contract of more general application than using theorems from types to reason about the correctness of my program at present? (Or are we just talking about two different things)

Answer 1

"Theorems for free" are so-called because they follow from the type of the program, without looking at the the program code!

"Contracts" are clearly not free theorems, because they depend on the code of the program, not merely the type.

However, the connection you do want to make is between types and specifications. Specifications are in a way "more detailed" types. Or, state the other way, types are more basic specifications. Martin-Lof type theory is precisely about fusing the two ideas into one.

Answer 2

The power of "theorems for free" depends upon the type system you choose to use. But as it is typically used, yes, "design by contract" is more expressive than "theorems for free": "design by contract" lets you specify some properties that cannot easily be proven using the "theorems for free" approach. Of course that does not mean that the "theorems for free" idea is useless or uninteresting.

I think maybe you are thinking about this in not quite the right way. It sounds almost like you are looking for a silver bullet or The One True Path to program correctness. Personally, I doubt that there will be any one-size-fits-all answer that is a perfect solution. Instead, I suggest that you focus more on understanding the space of available techniques and getting a better grip on their strengths and weaknesses -- I think you'll find that more informative than trying to set up a "gorilla vs shark" dichotomy ("theorems for free vs design by contract -- in a fight between the two, who would win?").