Types Are Contracts

This pattern was motivated by the discussion on DesignByContract. So, in (roughly) GangOfFour notation...

TypesAreContracts (better name suggestions welcome)

Context: You are designing a software interface such as a component, an API, a library, or a framework that will be used programmatically by others. That is, other programmers will have to instantiate objects and/or call methods that you write.

Religion: [A slight deviation from the normal protocol; I'd like to add here a bit of my own beliefs on software. Skip this section if you only care about the pattern.] In my own work, I try to think of everything as a component, which means that this pattern applies to pretty much every piece of software I ever write. As you may guess, this causes my code to suffer a lot from YouArentGonnaNeedIt, but on the upside I find that when I think about a future user of my code, I come up with better designs. But then I am a HumanFactors professional, so your mileage with this approach may vary.

Problem: To ensure that your interface is learnable and usable, you will need to convey the semantics (or contract) to your client/user/programmer/whomever somehow.

(aside) the worst-case scenario of API design has to be the older versions of MFC from Microsoft... The interface is obfuscated, there's lots of juicy gotchas in the usage semantics, and then they published a 9-volume book set about it. This is a particularly effective solution if you would like a high learning curve to your software, thus getting clients to commit huge time investment to it, which in turn prevents them from trying to learn competitor's interfaces and keeps them coming back for version after version. But if you don't happen to have a vertical monopoly in the software industry (or if your users are people that you could potentially find yourself alone with, away from help and near heavy objects of any kind) this won't be a good choice for you.

Solution: Realize that the interface methods and classes that you create can themselves be the contracts, that are implicitly enforced by the type system. We specify named classes like String and InputStream that have a certain set of operations associated with them; because of the encapsulating nature of objects in most OO languages, this places a restriction on what can be done with these objects, and what states that they can be in. So, your interface can come with a type system that allows you and your user to infer all of the contractual information you need from the types that cross your interface.

To make my point more clear (and to help you see that you already understand what I'm trying to explain), ask yourself why you would rather work with an interface that has methods like the third one instead of the first or second one:

	/** opens a connection to a server at the given URL, using the
	given network interface, and returns a handle to it, throwing
	an exception if there is a problem. **/

public Object openConnection (Object[] args) throws Exception public int openConnection (String url, int nintHandle) throws Exception public Connection openConnection (URL url, NetInterface? nint) throws NetworkException?
The second one is better than the first one because the types surrounding the method at least convey (a) the number of arguments and (b) that the URL has to be a string, and that the handles to connections and network interfaces must be integers. But the third one is better than the second because (a) The kind of exception that can be thrown is restricted so that you know what to catch; (b) the URL object's constructor enforces wellformed-ness properties, so you can infer that the URL is well-formed (c) the Connection object can have a protected constructor so that it can only be created in the openConnection method. The user of this method can then assume that if a Connection object exists, it must represent a valid, open connection. None of this "oh, the handle ID might be invalid" crap.

In this one little fragment, many things can be inferred about the integrity of the parameters and result (preconditions and post-conditions) just by the way the object invariants are defined. Encapsulation is a key language property for using this technique; without it you could not infer anything about the nature of the changes that have been made to your objects.

If you code with this pattern in mind, I think you will find that your design focus will be shifted toward defining the semantics of your types (DesignByContract, only where the contract is object-wise rather than method-wise).

Consequences: The more of your interface's semantics you can embed in the type structure of your software, the more of your contracts will be enforced at compile time, by the type-checker. However, you will have to create more classes to encapsulate these contracts, and depending on your language, it won't be worth it to you to encapsulate some of the more minor contracts. Further consequences:

Good luck! -- RusHeywood


Isn't this a point on the path that leads from doing things like
	typedef int fooHandle ;
in C, which is checked only by people, onwards through
	enum fooHandle{ Min=0, Max=MAX_INT};
which is compiler checked in some ways, and on to programmer-defined types as frst class, and on further to proofs?

Is there any value to viewing these concepts as points in a discrete spectrum?
I think it's true and worth saying (and here we cherish the obvious). There's a phrase, "A type checker is a poor man's program prover", which I first heard from BertrandMeyer about 10 years ago although it may be older. In Eiffel [EiffelLanguage] a new class might be useful solely for its extra invariants, even if its actual implementation is unchanged from its base class.

What is not necessarily obvious or true is whether automated proofs are worth the cost. The basic cost, in most current systems (ie C++/Java), is huge, in terms of overhead, complexity, redundancy and so forth. A static type system can be, well, static: rigid, inflexible, hard to change, as well as not sufficiently expressive. Automated program provers are not yet as clever as human program provers. However, given that you have a static type-system, you can sometimes use the TypesAreContracts insight to get more value out of it without much extra work. -- DaveHarris
All you seem to have done is argued that The right parameters are passed to the method. This doesn't work for checking if params are null, it also only covers preconditions, and only one type of preconditions at that. There are other types of precondition (such as ensuring a stack is non-empty before popping) as well as postconditions and invariants.

I don't see any real parallels between what you're saying here and DesignByContract. (which isn't to say that well specified types aren't a good thing anyway... Xp - SelfDocumentingCode :-)
The page states that TypesAreContracts, not the other way round, so it's ok for types to be only one type of precondition. The return type is a postcondition. -- FalkBruegmann
A most excellent, but known only in the circles-who-know-him senior programmer recently wrote me:

My meat-ball programmer's comment on type checking is:
There are a whole bunch of assertions I would like to be able to make about my programs; the fact that a variable is only permitted to dereference to an object of a specified type is one, not especially useful, assertion. I would like these assertions to be verified as soon as possible - before running the program would be nice, while editing would be even better.


Modern FunctionalProgrammingLanguages such as Haskell [HaskellLanguage] and Standard ML [SmlLanguage] and Clean [CleanLanguage] have type systems that have much more meaningful contracts than do modern object oriented languages such as Java [JavaLanguage] or the CeePlusPlus.

For example they can define linear objects that can only be accessed from one place at a time, i.e. ensure that some object is not being aliased (see LinearTypes). The analogy is like a locker at an airport. If I put something in the locker and take the key, no one else can get in the locker as long as I have the key. Before anyone else can get in the locker, I have to give them the key. Upon giving the key to someone else, I can no longer get into the locker until someone gives the key back to me.

All of these actions can be type checked at compile time. This is how modern statically typed functional programming languages do side effects like I/O, GUIs, concurrency, databases, CORBA, etc. and retain the benefits of FP.

Also see OnMonads.
Then interfaces are also contracts:
     inferred template<Typename rettype>
     rettype with(IDisposable disposable, Delegate<typeof(disposeable), :returns rettype> use) {
         try {
             return use(disposable);
         } finally {
             disposable.Dispose()
         }
     }
     with(open(filename), file => file.readAll())
This is probably the ultimate example of TypesAreContracts. Translating it will do this:
    func with(disposable, use)
    where( disposable.instanceOf(IDispsable)
       &&  use       .instanceOf(Delegate<disposable.type>)) { ... }
    guarantees (returnVal.instanceOf(use.returnType))

Eloquent, isn't it?
And what about ContractsAreAspects? -- stephan
CategoryLanguageTyping

EditText of this page (last edited August 22, 2010) or FindPage with title or text search