Union contracts as a side-effect Clause Samples

Union contracts as a side-effect. In Nickel, the failure of a function contract can always be traced back to a single call. For example, take the function f with a simple contract attached of Figure 11. The whole program fails with a contract error blaming f because the return value of the second call f 5 violates the Positive con- tract. The first call to f does not matter, and f 5 is a single and independent witness of the contract violation. The user is pointed to this one location in practice. This single witness property can be justified as follows. Apart from the error reporting part (although this is the cru- cial bit in practice!), the current contract system of Nickel can be implemented purely as a library, requiring only a fail primitive to abort the execution. In practice, applying a function contract to f replaces it with a f¹ that performs the additional checks. Thus, since the core language is pure (albeit partial, if only because fail), the failure of f¹ 5 must be independent of its environment and of any previous call to f¹. ✞ ☎ 1 let f | Positive → Positive 2 = fun x ⇒ x - 7 in 3 ( f 10) + ( f 5) This behavior indicates that union contracts introduce side-effects. The result of f 5 now depends on the previous execution and more specifically on any prior call to f. This behavior of union contracts break the property 1 introduced in Section 2.2, that is required to perform CSE-like optimiza- tions in all generality. The candidate example of Figure 5 in Section 2.2 can’t be optimized in general. Figure 13 illustrates this point further. It contains an orig- inal program and an optimized version where the common subexpression f 1 has been eliminated. While equivalent in a pure language without contracts, these two programs be- have differently because of unions: • The original version returns (1, "False") without fail- ing. • The optimized version fails with a contract violation. In the original version, each partial application f 1 gives rise to a fresh instance of the contract Bool → Num ∪ Bool → Str. These instances are independent, and can pick a dif- ferent component of the union to satisfy. Although f doesn’t actually respect the contract, these calls are not enough to prove so. In the optimized version, g is endowed with a sin- gle contract, that must pick one of the two components of the union. There, the two calls refer to the same union con- tract, and shows that f does violate its initial contract. ✞ ☎ ✝ ✆ let f | Num → ( Bool → Num ∪ Bool → Str ) = fun x y ⇒ if y then x...