What is the difference between dependent typed languages and languages like Spec# and Eiffel that allow you to specify “contracts” for functions in your code for pre/postconditions? Is dependent typing basically the purely functional version of Eiffel’s “contracts”?
From what I understand, dependently typed languages let you specify your function’s pre and post conditions using predicate logic as part of the type.
Eiffel’s concept of contracts seems to be similar, but based on imperative programming, not functional programming.
2
(Full) dependent typing allows you to write arbitrary expressions on the type level including ones that, in a more “mainstream” language, would be exclusive to the value level. This can let you write type-checked pre- and post-conditions for your functions, but only as a special case of being able to write anything you like.
In contrast, “contracts” can only do some very specific checking, as opposed to checking literally anything you can conceive of (as long as it’s computable).
So-called “refinement types” fall somewhere in between.
One important difference that hasn’t been explicitly mentioned so far, is that dependent types are checked at type-checking time (duh!), i.e. statically, before runtime. Eiffel contracts are checked dynamically, at runtime. Spec# falls somewhere in between: contracts are checked dynamically, at runtime, but you can get a theorem prover which can (try to) prove (some) contracts statically, before runtime.
1
Contracts should always be expressed in a functional, sideeffect free manner. They are language agnostic as such. Contract libraries and extensions exist for languages such as scheme, java, c# and haskell. They are very expressive but seldom statically checked.
Dependent types on the other hand are often less expressive and to my knowledge always statically checked.
My point with this post is to dismiss the notion that contracts are limited to imperative languages.
3