In the spirit of Alan Perlis...

"The pain of testing for bottom-up development is producing test data without a front-end. The pain of testing for top-down development is that you can't."

- Richard Cobbe

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).

Lambdas everywhere

From Mitch Wand's lecture notes for CSG264, Semantics of Programming Languages:

+----------------------------------------------------------------+
| Key questions:                                                 |
|                                                                |
|                                                                |
|            Syntax: What _is_ a program?                        |
|                   |                                            |
|                   |                                            |
|                   |                                            |
|                   |                                            |
|            Operational Semantics: What does a program compute? |
|                  /\                                            |
|                 /  \                                           |
|                /    \                                          |
|               /      \                                         |
|              /        \                                        |
|             /          \                                       |
|            /            \                                      |
|           /              \                                     |
| Equational Theories:      Denotational Semantics:              |
| When are two expressions  What does an expression mean?        |
| equivalent?                                                    |
+----------------------------------------------------------------+

I think I need more sleep--I'm seeing lambdas everywhere...