5

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.

Improve this question
2
  • 2
    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, 2014 at 22:53
  • I did a project in Coq where I modelled graphs. So I'm familiar with dependent typing.
    – fsl
    Feb 23, 2014 at 6:14

3 Answers 3

Reset to default
1

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

Improve this answer
2

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.

Improve this answer
1
  • 2
    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, 2014 at 23:47
-5

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.

Improve this answer
3
  • 2
    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, 2014 at 21:55
  • I did a project in Coq where I modelled graphs. So I'm familiar with dependent typing.
    – fsl
    Feb 23, 2014 at 6:15
  • 1
    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, 2014 at 8:10

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.