32
$\begingroup$

I've been reading some articles on dependent types and programming contracts. From the majority of what I've read, it seems that contracts are dynamically checked constraints and dependent types are statically checked.

There have been some papers that have made me think that it's possible to have contracts that are partially statically checked:

With this, there seems to be a significant amount of overlap and my categorisation of contracts vs dependent types starts to disappear.

Is there something deeper in either concepts that I'm missing? Or are these really just fuzzy categories of representing the same underlying concept?

Improve this question
$\endgroup$

4 Answers 4

Reset to default
27
$\begingroup$

On a practical level, contracts are assertions. They let you check (quantifier-free) properties of individual executions of a program. The key idea at the heart of contract checking is the idea of blame -- basically, you want to know who is at fault for a contract violation. This can either be an implementation (which does not compute the value it promised) or the caller (who passed a function the wrong sort of value).

The key insight is that you can track blame using the same machinery as embedding-projection pairs in the inverse limit construction of domain theory. Basically, you switch from working with assertions to working with pairs of assertions, one of which blames the program context and the other of which blames the program. Then this lets you wrap higher-order functions with contracts, because you can model the contravariance of the function space by swapping the pair of assertions. (See Nick Benton's paper "Undoing Dynamic Typing", for example.)

Dependent types are types. Types specify rules for asserting whether or not certain programs are acceptable or not. As a result, they do not include things like the notion of blame, since their function is to prevent ill-behaved programs from existing in the first place. There is nothing to blamed since only well-formed programs are even grammatical utterances. Pragmatically, this means that it is very easy to use dependent types to speak of properties of terms with quantifiers (eg., that a function works for all inputs).

These two views are not the same, but they are related. Basically, the point is that with contracts, we start with a universal domain of values, and use contracts to cut things down. But when we use types, we try to specify smaller domains of values (with a desired property) up front. So we can connect the two via type-directed families of relations (ie logical relations). For example, see Ahmed, Findler, Siek and Wadler's recent "Blame for All", or Reynolds' "The Meaning of Types: from Intrinsic to Extrinsic Semantics".

Improve this answer
$\endgroup$
8
  • $\begingroup$ Why do you say contracts are quantifier free? $\endgroup$
    – Radu GRIGore
    Mar 1, 2011 at 13:12
  • 4
    $\begingroup$ Because you can't generally use tests to establish universally quantified properties of functions, that's all. $\endgroup$
    – Neel Krishnaswami
    Mar 1, 2011 at 14:41
  • 4
    $\begingroup$ Unless the quantifiers range over finite domains, in which case they can be viewed as large conjunctions and disjunctions. Or if you wish to get fancy, you can check certain kinds of quantified statements, provided the quantiers range over Martin Escardo's searchable types (which can be infinite). $\endgroup$
    – Andrej Bauer
    Mar 1, 2011 at 18:58
  • 2
    $\begingroup$ @Radu: I call things like JML & co "program logics". The assertion languages of program logics are not restricted to being terms from the language of programs. This lets you rule out things like nonterminating or side-effecting assertions, which do not have a nice logical interpretation. (However, such things do matter for contract checking -- see Pucella and Tove's recent work at ESOP on using stateful, imperative contracts to track linearity properties.) $\endgroup$
    – Neel Krishnaswami
    Mar 2, 2011 at 8:25
  • 2
    $\begingroup$ That's because I mispelled Tov's last name. See "Stateful Contracts for Affine Types", ccs.neu.edu/home/tov/pubs/affine-contracts $\endgroup$
    – Neel Krishnaswami
    Mar 2, 2011 at 9:09
13
$\begingroup$

The (fairly abstract) problem that both types and contracts attack is "How to ensure that programs have certain properties?". There is an inherent tension here between being able to express a wider class of properties and being able to check that a program has or not a property. Type systems usually ensure a very specific property (the program never crashes in certain ways) and have a type checking algorithm. On the other hand, contracts let you specify a very wide range of properties (say, the output of this program is a prime number) but do not come with a checking algorithm.

Nevertheless, the fact that there is no contract checking algorithm (which always works) does not mean that there are no almost contract checking algorithms (which tend to work in practice). I would recommend you look at Spec# and the Jessie plugin of Frama-C. They both work by expressing "this program obeys this contract" as a statement in first-order logic via verification condition generation, and then asking an SMT solver to go try to find a proof. If the solver fails to find a proof, then either the program is wrong or, well, the solver failed to find a proof that exists. (Which is why this is an "almost" contract checking algorithm.) There are also tools based on symbolic execution, which means roughly that "this program obey this contract" is expressed as a bunch of propositions (in some logic). See, for example, jStar.

Flanagan's work tries to take what's best from both worlds such that you can quickly check type-like properties and then labour for the rest. I am not really familiar with hybrid types, but I do remember the author saying that his motivation was to come up with a solution that requires fewer annotations (than his previous work on ESC/Java did). In a sense, however, there is some loose integration between types and contracts in ESC/Java (and Spec#) too: when checking contracts, the solver is told that type-checking succeeded so it can se that information.

Improve this answer
$\endgroup$
7
$\begingroup$

Contracts can be checked statically. If you look at Dana Xu's old work on ESC/Haskell, she was able to implement full contract checking at compile time, only relying on a theorem prover for arithmetic. Termination is solved by a simple depth limit if I remember correctly:

Improve this answer
$\endgroup$
6
$\begingroup$

Both contracts and types allow you to represent Hoare-style (pre/post condition) specifications on functions. Both can be checked either statically at compile time or dynamically at runtime.

Dependent types allow you to encode a very wide range of properties in the type system, the kinds of properties that contract programmers expect. This is because they can depend on the values of the type. Dependent types have a tendency to be checked statically although I believe the papers you cited look at alternative approaches.

Ultimately, there is little difference. I think it is more that dependent types are a logic in which you can express specifications whereas contracts are a programming methodology in which you do express specifications.

Improve this answer
$\endgroup$
3
  • $\begingroup$ It's a little misleading to say that Hoare-style annotations can be checked statically. If the logic is FO, as it usually is, then the problem is certainly undecidable. But, yes, I know you meant that one can try and even succeed in many situations. $\endgroup$
    – Radu GRIGore
    Mar 1, 2011 at 11:10
  • 1
    $\begingroup$ I was under the impression that generating the proof may be undecidable but checking a proof should be. Many dependently-typed languages rely on the user to supply the proof-value of the theorem-type's inhabitance. $\endgroup$
    – Jason Reich
    Mar 1, 2011 at 11:52
  • $\begingroup$ You are right. But I live in the automated world, where the user is usually not asked for a proof. $\endgroup$
    – Radu GRIGore
    Mar 1, 2011 at 13:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.