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:

Your users will learn your interface faster, because OO programmers already have mental machinery for reasoning about classes and type systems. As soon as they look at a method they will be able to understand its contract as easily as a child understands that a square peg won't fit in a round hole.
Your code's performance will be improved, because you won't need to include as many run-time checks, and you won't have to worry about redundant condition checking. (This gain can be nulled out if your language takes a performance hit on systems with lots of classes. See below.)
The set of compilable but incorrect uses of your interface is smaller, so the probability of your user making a silent mistake is lessened (in general).
If a lot of the complexity of your semantics are checked at compile-time, then there is less of a burden on you and your users to construct elaborate test code, and it brings you closer to creating test cases that exercise your interface representatively (or better yet) exhaustively.
You will wind up creating more classes than you otherwise would have, because (in theory) every distinct representational invariant must have its own class, and this can get nasty in languages where adding classes impacts application small-ness (such as Java applets where code must be moved over a net connection.)
This pattern will only be useful in languages that have static types. That is, types have to be explicitly definable and, once created, have to be immutable for a particular run of the software. That means that LISP [LispLanguage] and its ilk are totally out, because you can add and delete methods and properties at run-time, thus destroying the invariant property of types. The exception to this is a language with structural types; that is, types are not named but the compiler takes two objects to have the same type if their signatures (the methods that operate on them) is the same. ML [MlLanguage] has this, and I believe that NuPrl? from CornellUniversity? supports a somewhat more aggressive version of this property as well. Could someone say something about how this will work in SmallTalk? I don't know enough about it to say.
More classes will slow down development because the codebase will be larger and refactoring will be more cumbersome unless your DevelopmentTools are extremely good (as in SmallTalk).
If your interface is very complex or contains many contracts, you will inundate the user with lots of classes. This can be daunting, because it will be harder for users to figure out which classes are the important ones that they will use most, and which are just the little misc classes that are used between operations.
In hybrid languages where both object types and primitive types exist (Java and C++, primarily), your methods will sometimes need to use classes to encapsulate otherwise primitive or nearly primitive types. This will be annoying to both you and your users because:
these languages usually make primitive types explicit because they are faster, have different semantics, and are more lightweight. Reimplementing them as object types will probably degrade performance. Especially Java: if you have a VirtualMachine with a crappy GarbageCollection algorithm, creating a primitive versus object type variable in some inner loop somewhere can be the difference between acceptable and unacceptable performance.
- it becomes unlikely that your interface will accept the type that the user's data is already in. (i.e. they are plugging your graphics interface up to a 3rd party math interface, but the math interface gives results as doubles and your interface accepts only PositiveDoubles?. You will force the user to add conversion code that will be both slow to write and slow to run.) This gets even stupider if the first thing your interface does upon receipt of the variable is covert it to a primitive.

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, CategoryObjectOrientation