Sign up ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free.

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.

share|improve this question

migrated from Feb 22 '14 at 20:01

This question came from our site for professional and enthusiast programmers.

My answer here might give a better understanding of what dependant typing is, also have a read of the wikipedia page. – Jimmy Hoffa Feb 22 '14 at 22:53
I did a project in Coq where I modelled graphs. So I'm familiar with dependent typing. – fsl Feb 23 '14 at 6:14

3 Answers 3

up vote 1 down vote accepted

(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.

share|improve this answer

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.

share|improve this answer
I used Eiffel in college, it can do static analysis depending on how you compile, I think some of the options were melt and freeze. – Andy Feb 23 '14 at 23:47

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.

share|improve this answer
I get the distinct sense you don't know what dependant typing is, as you really didn't describe it at all here, -1. – Jimmy Hoffa Feb 22 '14 at 21:55
I did a project in Coq where I modelled graphs. So I'm familiar with dependent typing. – fsl Feb 23 '14 at 6:15
the point you're trying to make doesn't look compelling because, as been already pointed by @JimmyHoffa, answer fails to demonstrate sufficient understanding of dependent typing. Don't get me wrong, you may be good at it, it's just the way the answer is written now doesn't let readers to see that – gnat Feb 23 '14 at 8:10

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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