D - Contracts for Higher-Order Functions
- Mark Evans <Mark_member pathlink.com> Feb 19 2003
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  has shown, for example, these contracts have great practical value in improving the robustness of systems in procedural languages. Eiffel  even developed an entire philosophy of system design based on contracts ('Design by Contract'). Although Java  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 , 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."
Feb 19 2003