<p>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.</p>

<p>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 <a href="http://research.microsoft.com/en-us/projects/specsharp/">Spec#</a> and the <a href="http://frama-c.com/jessie.html">Jessie plugin of Frama-C</a>. They both work by expressing "this program obeys this contract" as a statement in <a href="http://en.wikipedia.org/wiki/First-order_logic">first-order logic</a> via <a href="http://scholar.google.co.uk/scholar?cluster=2215741797543540501">verification condition</a> generation, and then asking an <a href="http://combination.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf">SMT</a> 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, <a href="http://scholar.google.co.uk/scholar?cluster=3520513541734269654">jStar</a>.</p>

<p>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.</p>

CC BY-SA 2.5
2011-03-01T11:07:12.143Z
2011-03-01T11:07:12.143Z
Radu GRIGore
<p>Contracts can be checked statically. If you look at Dana Xu's old work on <a href="http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm">ESC/Haskell</a>, 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:</p>

CC BY-SA 2.5
2011-03-05T13:30:15.680Z
2011-03-05T13:30:15.680Z
Liam O'Connor
<p>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.</p>

<p>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 <em>depend</em> 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.</p>

<p>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.</p>

CC BY-SA 2.5
2011-03-01T11:10:12.643Z
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.
Radu GRIGore
CC BY-SA 2.5
2011-03-01T11:52:14.400Z
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.
Jason Reich
CC BY-SA 2.5
2011-03-01T13:06:37.363Z
You are right. But I live in the automated world, where the user is usually *not* asked for a proof.
Radu GRIGore
CC BY-SA 2.5
2011-03-01T11:00:37.843Z
2011-03-01T11:00:37.843Z
Jason Reich
<p>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). </p>

<p>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 <a href="http://www.springerlink.com/content/d0vv8g7774666526/">"Undoing Dynamic Typing"</a>, for example.)</p>

<p>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). </p>

<p>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 <a href="http://www.cs.indiana.edu/~amal/papers/blameall.pdf">"Blame for All"</a>, or Reynolds' <a href="http://repository.cmu.edu/cgi/viewcontent.cgi?article=2290&amp;context=compsci">"The Meaning of Types: from Intrinsic to Extrinsic Semantics"</a>. </p>

CC BY-SA 2.5
2011-03-01T13:12:33.003Z
Why do you say contracts are quantifier free?
Radu GRIGore
CC BY-SA 2.5
2011-03-01T14:41:22.203Z
Because you can't generally use tests to establish universally quantified properties of functions, that's all.
Neel Krishnaswami
CC BY-SA 2.5
2011-03-01T18:58:59.080Z
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).
Andrej Bauer
CC BY-SA 2.5
2011-03-01T22:04:05.060Z
Let me rephrase: Why do you insist on contracts being checkable at runtime? That's not what JML does, it's not what Boogie does, it's not what separation logic tools do, etc. Yes, it's what "code contracts" do, what Eiffel contracts do, etc. But's it's far from being a property of all contracts.
Radu GRIGore
CC BY-SA 2.5
2011-03-01T22:06:46.727Z
Thanks for the [searchable types reference](http://scholar.google.com/scholar?cluster=13983294822949835758). I didn't know it.
Radu GRIGore
CC BY-SA 2.5
2011-03-02T08:25:39.343Z
@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.)
Neel Krishnaswami
CC BY-SA 2.5
2011-03-02T09:01:55.980Z
@Neel: Thanks. I call "contracts" anything that abstracts a procedure call as a pre-post pair. I can't find the paper you mention. In a sense, there are side-effecting assertions in JML (they throw exceptions), but that's rather unintended (see [Chalin](http://scholar.google.co.uk/scholar?cluster=15864206322431745680)).
Radu GRIGore
CC BY-SA 2.5
2011-03-02T09:09:24.733Z
That's because I mispelled Tov's last name. See "Stateful Contracts for Affine Types", http://www.ccs.neu.edu/home/tov/pubs/affine-contracts/
Neel Krishnaswami
CC BY-SA 2.5
2011-03-01T11:51:39.220Z
2011-03-01T11:51:39.220Z
Neel Krishnaswami
<p>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.</p>

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

<ul>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93.3743&amp;rep=rep1&amp;type=pdf">Hybrid Type Checking</a> (C. Flanagan - 2006)</li>
<li><a href="http://sage.soe.ucsc.edu/tfp07-gronski-flanagan.pdf">Unifying Hybrid Types and Contracts</a> (J. Gronski, C. Flanagan - 2007)</li>
</ul>

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

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

<pl.programming-languages><type-theory><program-verification><dependent-type>
Relationship between contracts and dependent typing
Brian McKenna
# Relationship between contracts and dependent typing

(Asked by: username_0 on 2011-03-01)

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:

* [Hybrid Type Checking](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93.3743&rep=rep1&type=pdf) (C. Flanagan - 2006)
* [Unifying Hybrid Types and Contracts](http://sage.soe.ucsc.edu/tfp07-gronski-flanagan.pdf) (J. Gronski, C. Flanagan - 2007)

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?

**Tags:** pl.programming-languages, type-theory, program-verification, dependent-type


---

## 4 answers

### Answer by username_4 on 2011-03-01. Score: 27 | Accepted answer

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"](http://www.springerlink.com/content/d0vv8g7774666526/), 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"](http://www.cs.indiana.edu/~amal/papers/blameall.pdf), or Reynolds' ["The Meaning of Types: from Intrinsic to Extrinsic Semantics"](http://repository.cmu.edu/cgi/viewcontent.cgi?article=2290&context=compsci).

> **Comments:**
> **username_1**: Why do you say contracts are quantifier free?  
> **username_4**: Because you can't generally use tests to establish universally quantified properties of functions, that's all.  
> **username_5**: 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).  
> **username_1**: Let me rephrase: Why do you insist on contracts being checkable at runtime? That's not what JML does, it's not what Boogie does, it's not what separation logic tools do, etc. Yes, it's what "code contracts" do, what Eiffel contracts do, etc. But's it's far from being a property of all contracts.  
> **username_1**: Thanks for the [searchable types reference](http://scholar.google.com/scholar?cluster=13983294822949835758). I didn't know it.  
> **username_4**: @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.)  
> **username_1**: @Neel: Thanks. I call "contracts" anything that abstracts a procedure call as a pre-post pair. I can't find the paper you mention. In a sense, there are side-effecting assertions in JML (they throw exceptions), but that's rather unintended (see [Chalin](http://scholar.google.co.uk/scholar?cluster=15864206322431745680)).  
> **username_4**: That's because I mispelled Tov's last name. See "Stateful Contracts for Affine Types", http://www.ccs.neu.edu/home/tov/pubs/affine-contracts/  

---

### Answer by username_1 on 2011-03-01. Score: 13

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#](http://research.microsoft.com/en-us/projects/specsharp/) and the [Jessie plugin of Frama-C](http://frama-c.com/jessie.html). They both work by expressing "this program obeys this contract" as a statement in [first-order logic](http://en.wikipedia.org/wiki/First-order_logic) via [verification condition](http://scholar.google.co.uk/scholar?cluster=2215741797543540501) generation, and then asking an [SMT](http://combination.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf) 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](http://scholar.google.co.uk/scholar?cluster=3520513541734269654).

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.


---

### Answer by username_2 on 2011-03-05. Score: 7

Contracts can be checked statically. If you look at Dana Xu's old work on [ESC/Haskell](http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm), 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:


---

### Answer by username_3 on 2011-03-01. Score: 6

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.

> **Comments:**
> **username_1**: 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.  
> **username_3**: 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.  
> **username_1**: You are right. But I live in the automated world, where the user is usually *not* asked for a proof.  

---

