Contracts

Can you spot the error in the following?

var raise = function (div) {
  div.style.setProperty('z-index',
      div.style.getProperty('z-index') + 1);
}

If the z-index of div was ‘4’, then calling raise(div) would set z-index to ’41’! The reason is that style properties are strings, and when one of the arguments to + is a string, it coerces the other to a string and concatenates the two.

Contracts can help avoid errors like the one above. A first-order contract is a function that either returns its input or throws an exception.  Here are two first-order contracts:

var str = function (s) {
  if (typeof s !== 'string') {
    throw new TypeError('Expected a string.');
  }
  return s;
};

var nat32 = function (n) {
  if ((n | 0) !== n || n < 0) {
    throw new TypeError('Expected a 32-bit ' +
        'natural.');
  }
  return n;
};

Here are two functions from nat32 to str:

var itoa = function (n) {
  return str('' + nat32(n));
};

var spaces = function (n) {
  nat32(n);
  var result = new Array(n + 1).join(' ');
  return str(result);
};

I’ll denote the types of itoa and spaces as

itoa: nat32 -> str
spaces: nat32 -> str

Now for some math: a category consists of

  • a collection of objects, and
  • for any pair of objects A, B, a set of morphisms between them (if f is a morphism from A to B, we write f:A -> B)

such that

  • every object A has an identity morphism id_A:A -> A;
  • we can compose morphisms f, g if the target object of f matches the source object of g;
  • composition is associative; and
  • composing with the identity gives back the same morphism.

Contracts and the functions between them form a category. Given any two contracts, there’s a set of functions going between them. If we have two functions

f:A -> B
g:B -> C,

we can compose them to get

gf: A -> C

by writing

var gf = function (a) {
  return g(f(a));
};

Also, given any contract A, there’s the identity function from A to itself:

var id_A = function (a) {
  return A(a);
};

This is obviously equivalent to the contract A, so we’ll always use A instead.

Had setProperty used the appropriate contract, raise would have caused an error the first time it was used, and we could have fixed it:

var raise = function (div) {
  div.style.setProperty('z-index',
      // The unary + coerces the
      // result to a number.
      +div.style.getProperty('z-index') + 1);
}
Advertisements

6 Comments to “Contracts”

  1. So is it true to say that Contracts ensure membership of a category? I feel that my intuition of what a category is isn’t quite right…

    So in your examples about are Strings and 32 bit Integers categories and is the function itoa a morphism from String to Int32?

    • Contracts ensure membership in a set. Categories have two parts, objects and morphisms. The contracts are the objects in this category, so str is one object and nat32 is another object. Morphisms go between objects, so as you said, itoa is a morphism between str and nat32.

  2. It’s a shame so many programming languages overload string concatenation on “+”, which in mathematics is always a commutative operation.

  3. Shouldn’t atoi be called itoa (or ntoa?)

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: