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 (C. Flanagan - 2006)Unifying Hybrid Types and Contracts (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?
Relationship between contracts and dependent typing
pl.programming languages;type theory;program verification;dependent type
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. 