Comparing design by contract to type systems_问答_开发者

I recently read a paper that compared Design-by-Contract to Test-Driven-Development. There seems to be lot开发者_开发知识库 of overlap, some redundancy, and a little bit of synergy between the DbC and TDD. For example, there are systems for automatically generating tests based on contracts.

In what way does DbC overlap with modern type system (such as in haskell, or one of those dependently typed languages) and are there points where using both is better than either?

The paper Typed Contracts for Functional Programming by Ralf Hinze, Johan Jeuring, and Andres Löh had this handy table that illustrates whereabouts contracts sit in the design spectrum of "checking":

                   |   static checking    |   dynamic checking
-------------------------------------------------------------------
simple properties  | static type checking | dynamic type checking
complex properties | theorem proving      | contract checking

It seems most answers assume that contracts are checked dynamically. Note that in some systems contracts are checked statically. In such systems you can think of contracts as a restricted form of dependent types which can be checked automatically. Contrast this with richer dependent types, which are checked interactively, such as in Coq.

See the "Specification Checking" section on Dana Xu's page for papers on static and hybrid checking (static followed by dynamic) of contracts for Haskell and OCaml. The contract system of Xu includes refinement types and dependent arrows, both of which are dependent types. Early languages with restricted dependent types that are automatically checked include the DML and ATS of Pfenning and Xi. In DML, unlike in Xu's work, the dependent types are restricted so that automatic checking is complete.

The primary differences is that testing is dynamic and incomplete, relying on measurement to give evidence that you have fully validated whatever property you are testing, while types and typechecking is a formal system that guarantees all possible code paths have been validated against whatever property you are stating in types.

Testing for a property can only approach in the limit the level of assurance a type check for the same property provides out of the box. Contracts increase the base line for dynamic checking.

DBC is valuable as long as you can't express all the assumptions in the type systen itself. Simple haskell example:

take n [] = []
take 0 _  = []
take n (a:as) = take (n-1) as

The type would be:

take :: Int -> [a] -> [a]

Yet, only values greater-equal 0 are ok for n. This is where DBC could step in and, for example, generate appropriate quickcheck properties.

(Of course, in this case, it is too easy to check also for negative values and fix an outcome other than undefined - but there are more complex cases.)

I think DbC and type's systems are not comparable. There are confusion between DbC and type systems (or even verification systems). For example, we can find comparing DbC and Liquid Haskell tool or DbC and QuickCheck framework. IMHO it's not correct: type's systems as well as formal prove systems assert only one - you: you have some algorithms in our mind and you declare properties of these algorithms. Then you implement these algorithms. Types systems as well as formal prove systems verify that the code of implementation corresponds to the declared properties.

DbC verifies not internal things (implementation/code/algorithm) but external things: expected features of things which are external to your code. It can be state of the environment, of file system, of DB, callers, sure your own state, anything. Typical contracts work at runtime, not at compile time or in special verification phase.

Canonical example of DbC shows how was found bug in HP chip. It happens because DbC declares properties of external component: of the chip, its state, transitions, etc. And if your application hits unexpected external world state, it report such case as exception. Magic here is that: 1) you define contracts in one place and don't repeat yourself 2) contracts can be easy turned-off (dropped out from compiled binary). They are more close to Aspects IMHO, due they are not "linear" like subroutines calls.

My recap here is that DbC are more helpful to avoid real world bugs than types systems, because most real bugs happen due to misunderstanding of behavior of external world/environment/frameworks/OS components/etc. Types and prove assistance help only to avoid your own simple errors which can be found with tests or modeling (in MatLab, Mathematica, etc, etc).

In short: you can not find bug in HP chip with types system. Sure, exists illusion that it's possible to something like indexed monads, but real code with such attempts will look super complex, unsupportable and not practical. But I think there are possible some hybrid schemes.