Polymorphic contracts

What does it mean for a the ML or Haskell type checker to give your function the type ∀α.α→α? It means that even though you haven't told the compiler what type T you're thinking of, it can prove that your function has type T→T anyway. After a moment's reflection you realize (and after a huge pile of math you can prove) that the only way the type checker could do that is if your function has all of those types simultaneously, so it (a) doesn't do anything to its argument and (b) returns that argument intact. Or maybe it diverges on all inputs, or maybe it remembers prior values it's been given and returns one of those or something like that, but it never makes up new values and returns those.

So, what does it mean if you give a Scheme function the contract ∀α.α→α? One interpretation is that you're asserting that your function satisfies all of the contracts C→C for every C simultaneously. There's only one way you can say that; it's if your function returns its argument intact, or diverges on all inputs, or returns a previously-remembered input value. (That's easy enough to show based on the view of contracts as pairs of projections, incidentally.) It may make first-order observations about its argument, but it cannot do anything to it that would assume any particular contract on it, like seeing that it's a procedure and calling it with an argument. If you do, it's a contract violation because whatever you do there's some contract that your use would be violating. That system almost already implemented in the current PLT Scheme contract library, in the form of anaphoric contracts.

There's another way to do it, too, though, based on a different interpretation. We could also interpret the contract ∀α.α→α to mean, "for any contract C you give me, I can give you back a function that satisfies the contract C→C." In this interpretation, contracts aren't analagous to for-all types, they're analagous to kinds in the sense of System F_ω. In this system, a function gets to know the contract it's expected to conform to, and it might be able to take special action based on that knowledge. It's more powerful, but also more difficult to use: your function has to explicitly take in a contract, and anywhere you use it you've got to tell it the contract you're thinking of. Furthermore, it's not really a "contract" anymore, since it's not a projection on values directly; it's more a "contract kind."

This system is technically already possible in the PLT Scheme contract system: (->d contract? (lambda (c) (-> c c))) is the contract kind that produces C→C contracts.

[Edit 3.08.06 9:34: "Anaphoric", not "anamorphic" (nor "Anamorphic", and definitely not "Animorphic"). Thanks Dave!]