An investigation of contracts as projections
Robert Bruce Findler, M. Blume, Matthias Felleisen · 2004
Software contracts help programmers enforce program properties that the language’s type system cannot express. Unlike types, contracts are (usually) enforced at run-time. When a contract fails, the contract system signals an error. Beyond such errors, contracts should have no other observable (functional) effect on the program’s results. In most implementations, however, the language of contracts is the full-fledged programming language, which means that programmers may (intentionally or unintentionally) introduce visible effects into their contracts. Here we present the results of investigating the nature of contracts from a denotational perspective. Specifically, we use SPCF and the category of observably sequential functions to show that contracts are best understood as projections. Thus far, the investigation has produced a significantly faster contract implementation and the insight that our contract language cannot express all projections, which in turn has produced a new contract combinator.