Stacked contracts are not intersection types

In contract systems like PLT Scheme's, a value can acquire multiple contracts during control flow. For example, a value might get passed to and returned from a function with a C → C contract, and then later passed to and returned from a funtion with a D → D contract. This value will now be dynamically wrapped with both C and D contracts. Conceptually, this means that the value must satisfy the constraints of both C and D. I was long tempted to think of this like an intersection type: the value "is a C and a D".

But this intuition will lead you astray. Here's a simple example of stacked contracts which do not behave like intersection types at all:

(module wrap-int mzscheme
  (require (lib "contract.ss"))
  (define (wrap-int f) f)
  (provide/contract
   [wrap-int ((integer? . -> . integer?) . -> .
              (integer? . -> . integer?))]))

(module wrap-bool mzscheme
  (require (lib "contract.ss"))
  (define (wrap-bool f) f)
  (provide/contract
   [wrap-bool ((boolean? . -> . boolean?) . -> .
               (boolean? . -> . boolean?))]))

(module main mzscheme
  (require wrap-int wrap-bool)
  (define id (wrap-int (wrap-bool (lambda (x) x))))
  (provide id))

The first two modules both provide functions that take in a function argument and return it wrapped with integer → integer and boolean → boolean contracts, respectively. The main module then wraps the identity function in both of these contracts.

Now, if these were to behave like intersection types, the identity function would have type integer → integer ∧ boolean → boolean, and would be perfectly well-typed.

But with contracts, the function's contracts are checked one piece at a time by checking all arguments against all the contracts' domains and all results against all the contracts' ranges. This means that if we apply id to any value, it will be checked to be both an integer and a boolean. And if it ever produces a result (it won't) that result will also be checked to be both an integer and a boolean. That is, the resulting contract is more analogous to (integer ∧ boolean) → (integer ∧ boolean) than to (integer → boolean) ∧ (integer → boolean).