Static types vs contracts

There are two common ways of making program boundaries more trustworthy: Contracts help when interface promises are richer than ordinary type signatures. They may depend on runtime values, state, or boundary crossing.

Contracts are often explained as runtime type checks, but that description is too small. A contract is better understood as localized agreement: when a value crosses a boundary, the contract system checks that the value is being used according to the agreement, and reports which side broke it if the agreement is violated.

Of course this means that with contracts we don't get to know if the program is "correct" upfront, but the goal here is to move error messages as close to the sources of errors as possible. To show what I mean, consider the following python type definition:

  class Rectangle:
    def __init__(self, height, width):
      self.height = height
      self.width = width
  
and a function that uses that type:

  def get_area(rec):
    rec.height * rec.width
  
Nothing prevents us from calling get_area on a an argument that it does not expect. But there is a difference between doing get_area("SOME STRING") and

  x = Rectangle("SOME", "STRING")
     ...
  return get_area(x)
  
The difference is that both calls result in an error thrown during the call, but only in the first example it would be the actual source of that error. In the second example, the source is the construction of a bad rectangle.

If we stick to dynamic typing, then the solution is to add type checks at every call, including calls to constructors.

  class Rectangle:
    def __init__(self, height, width):
      assert(instanceof(self, Rectangle))
      assert(typeof(height), number)
      assert(typeof(width), number)

      self.height = height
      self.width = width

    ...

  def get_area(rec):
    assert(instanceof(rec, Rectangle)) # ignore duck typing concerns
    rec.height * rec.width
  
But there are at least two things that we can improve on. One is to make it less verbose, since the code for type checking is currently not separated from the main logic. For this, we could move those checks to the functions signatures, like this:

  def get_area(rec: Rectangle):
    rec.height * rec.width
  
But the second issue is more subtle: our template solution is not directly transferrable to higher order objects. Consider this example:

  def iterate(fn: Function[Number, Number], n: Number)
    x = 0
    for i in range(n):
      x = fn(x)
    return x
  
It is not possible for iterate to check whether fn is of the right type at the moment of receiving the function. So if fn would ever return something other than a Number, the error would be thrown in iterate, without ever mentioning that it is actually the fn's fault. To combat this, we want to make the type signatures of Function objects public, and to also check that what they return is permitted by that signature. This is not ideal, but it helps.

But ordinary type checks are only the simplest case. The more interesting use of contracts is not to say that a value has the right shape, but to say that an operation is allowed in the current state of the world. For example, consider a function that grants access to a document:

def grant_access(actor_id: UserId, document_id: DocumentId, target_id: UserId):
  ...
The ordinary type signature can say that all three arguments are IDs. But that is not the real promise. The real promise is that the actor exists, the document exists, the target user exists, the actor currently has permission to share the document, the document is not archived, and the target user is allowed to receive access. Those facts are not sitting inside the source code. They live in the database, and they may change between deployments, requests, or even two calls to the same function.

The advantage of contracts is not that they are more disciplined than static types, or that static types are obsolete. Static types are checked early, but must usually stay within a decidable and relatively syntactic approximation of program behavior. Contracts are checked later, but can talk directly about runtime values, module boundaries, higher-order functions, and semantic promises that would be impossible to express as ordinary types.

return home