• Mark Evans (28/28) Feb 19 2003 Contracts for Higher-Order Functions

Mark Evans <Mark_member pathlink.com> writes:

Contracts for Higher-Order Functions

How to do contracts in functional languages, showing that functional features
are not out of the question for D just because of contracts.  -M.

http://people.cs.uchicago.edu/~robby/publications/papers/ho-contracts-icfp2002.pdf

"Assertions play an important role in the construction of robust software. Their
use in programming languages dates back to the 1970s. Eiffel, an object-oriented
programming language, wholeheartedly adopted assertions and developed the
“Design by Contract” philosophy. Indeed, the entire object-oriented community
recognizes the value of assertion-based contracts on methods.

"In contrast, languages with higher-order functions do not support
assertion-based contracts. Because predicates on functions are, in general,
undecidable, specifying such predicates appears to be meaningless. Instead, the
functional languages community developed type systems that statically
approximate interesting predicates.

"In this paper, we show how to support higher-order function contracts in a
theoretically well-founded and practically viable manner....

"Dynamically enforced pre- and post-condition contracts have been widely used in
procedural and object-oriented languages [11, 14, 17, 20, 21, 22, 25, 31]. As
Rosenblum [27] has shown, for example, these contracts have great practical
value in improving the robustness of systems in procedural languages. Eiffel
[22] even developed an entire philosophy of system design based on contracts
('Design by Contract'). Although Java [12] does not support contracts, it is one
of the most requested extensions.

"With one exception, higher-order languages have mostly ignored assertion-style
contracts. The exception is Bigloo Scheme [28], where programmers can write down
first-order, type-like constraints on procedures. These constraints are used to
generate more efficient code when the compiler can prove they are correct and
are turned into runtime checks when the compiler cannot prove them correct."