They behave enough like types that the library in question is pretty much as far from idiomatic Ruby you get if you use it like in his examples and tutorial.
Constraining inputs to a specific class, for example is a huge, giant no-no. If you're going to make Ruby statically typed, then you're better off picking a language that's easier to make fast.
This is a pet peeve of mine as I've more than once had to work around arbitrary, stupid checks against specific classes in cases where meeting the "actual" contract of the method called would be down to implementing a simple method or two.
The tutorial hints at some possibly Ruby-ish possibilities, like contracts based on whether an object responds to a method, but all the focus seems to be on class comparisons.
I do like the idea of specifying contracts, fwiw, as long as they're focused on behaviour and not on matching specific classes.
I don't, however like the idea of specifying them in the class files. Specifying them in separate files, that could be loaded when wanted, and that could also be used by a testing app to do some degree of automated testing of limits etc., or by other apps to do limited static analysis would be interesting.
And their core, types and contracts are the same thing: logical propositions asserting properties of a program that have to be enforced somehow. The difference is the method of enforcement: types are enforced via static analysis and contracts are enforced via runtime checks.
Oh, and if what you meant was "types cannot check pre/postconditions", then you should have a look at dependently typed languages. Some dependently typed systems can express any proposition expressive in first-order predicate logic. (The downside is that satisfying the type checker becomes bloody hard.)
Thank you for seeking to educate me about dependent typing, but I have a Masters in PL theory, have done numerous proofs about PL and type theory in Coq, and did my Masters' thesis on contract systems, under the person who invented contracts in higher-order languages. I do, in fact, know what I'm talking about. :) Unfortunately, it is quite a long explanation and needs a full blog post to cover in detail.
A few notes, though: contracts can feature blame, which types cannot, and types are proofs and contracts aren't (which can be both a plus and a minus depending on your situation).
- The word 'contract' has different meanings depending on which subcommunity you are talking to. For example, the Penn crowd often uses the word 'contract' in relation to refinement typing. The Scheme folks tend to think of the problem in different terms, but I am not convinced there is any substantial or insightful difference between the various definitions. As you seem to be an expert in the subject, I am sure you have read the manifest contracts paper, but I will leave this link here for the others: http://www.cis.upenn.edu/~mgree/papers/popl2010_contracts.pd....
- I have never heard anyone say that types cannot feature blame. I would argue that, for example, Haskell's type checker is quite good at blaming the correct party for a type violation. To argue the opposite you would need a precise definition of blame, and I am aware there are several papers written on this subject. I am sure you could find a definition of blame that excludes static type systems, but I am not sure that definition would be useful.
- Types are not proofs, but typing derivations are. Even if you consider types and contracts to be different, the execution trace serves as a proof of a dynamically checked 'contract' (which is really just a derivation in an operational semantics).
This is definitely true, thanks for the correction.
I have never heard anyone say that types cannot feature blame. I would argue that, for example, Haskell's type checker is quite good at blaming the correct party for a type violation.
I agree this is dependent on how you construct blame. In the sense I was talking about, it would be difficult to construct a type system which blamed in the same way -- the type system would essentially require a runtime checker for independent pieces of the program crossing the contract boundary, which I have seen constructions of, but is generally not seen as standard.
For background, my contract work was in Racket, so I am of the Scheme school :)
Types themselves are not proofs. In particular, the proposition associated to a type might be a blatant lie - you simply should be unable to find a term for that type. Also, the notion of blame in a contract maps directly to the type checker telling you which term does not type check.
