Abstract
We present an untyped calculus of blame assignment for a higher-order contract system with two new operators: intersection and union. The specification of these operators is based on the corresponding type theoretic constructions. This connection makes intersection and union contracts their inevitable dynamic counterparts with a range of desirable properties and makes them suitable for subsequent integration in a gradual type system. A denotational specification provides the semantics of a contract in terms of two sets: a set of terms satisfying the contract and a set of contexts respecting the contract. This kind of specification for contracts is novel and interesting in its own right. A nondeterministic operational semantics serves as the specification for contract monitoring and for proving its correctness. It is complemented by a deterministic semantics that is closer to an implementation and that is connected to the nondeterministic semantics by simulation. The calculus is the formal basis of TJS, a language embedded, higher-order contract system implemented for JavaScript.
- A. Ahmed, R. B. Findler, J. G. Siek, and P. Wadler. Blame for all. In T. Ball and M. Sagiv, editors, Proc. 38th ACM Symp. POPL, pages 201–214, Austin, TX, USA, Jan. 2011. ACM Press. Google ScholarDigital Library
- F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types. In T. Ito and A. Meyer, editors, Proc. Theoretical Aspects of Computer Software, volume 526 of LNCS, Sendai, Japan, 1991. Springer. Google ScholarDigital Library
- F. Barbanera, M. Dezani-Ciancaglini, and U. de’ Liguoro. Intersection and union types: Syntax and semantics. Information and Computation, 119(2):202–230, 1995. Google ScholarDigital Library
- M. Blume and D. McAllester. Sound and complete models of contracts. J. Funct. Program., 16:375–414, July 2006. Google ScholarDigital Library
- M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv. Math. Logik, 19(139-156), 1978.Google Scholar
- R. Davies and F. Pfenning. Intersection types and computational effects. In P. Wadler, editor, Proc. ICFP 2000, pages 198–208, Montreal, Canada, Sept. 2000. ACM Press, New York. Google ScholarDigital Library
- C. Dimoulas and M. Felleisen. On contract satisfaction in a higher-order world. ACM TOPLAS, 33(5):16, 2011. Google ScholarDigital Library
- C. Dimoulas, R. B. Findler, C. Flanagan, and M. Felleisen. Correct blame for contracts: No more scapegoating. In T. Ball and M. Sagiv, editors, Proc. 38th ACM Symp. POPL, pages 215–226, Austin, TX, USA, Jan. 2011. ACM Press. Google ScholarDigital Library
- T. Disney, C. Flanagan, and J. McCarthy. Temporal higher-order contracts. In O. Danvy, editor, Proc. ICFP 2011, pages 176–188, Tokyo, Japan, Sept. 2011. ACM Press, New York. Google ScholarDigital Library
- J. Dunfield and F. Pfenning. Type assignment for intersections and unions in call-by-value languages. In A. D. Gordon, editor, FOSSACS 2003, volume 2620 of LNCS, pages 250–266. Springer, 2003. Google ScholarDigital Library
- R. B. Findler and M. Blume. Contracts as pairs of projections. In P. Wadler and M. Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 226–241, Fuji Susono, Japan, Apr. 2006. Springer. Google ScholarDigital Library
- R. B. Findler, M. Blume, and M. Felleisen. An investigation of contracts as projections. Technical Report TR-2004-02, University of Chicago, Computer Science Department, 2004.Google Scholar
- R. B. Findler and M. Felleisen. Contracts for higher-order functions. In S. Peyton-Jones, editor, Proc. ICFP 2002, pages 48–59, Pittsburgh, PA, USA, Oct. 2002. ACM Press, New York. Google ScholarDigital Library
- M. Flatt and PLT. The Racket Reference, v.6.1.1 edition, 2015. http://docs.racket-lang.org/reference/index.html.Google Scholar
- R. Floyd. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics, pages 19–32, 1967.Google Scholar
- M. Furr, J. An, J. S. Foster, and M. W. Hicks. Static type inference for Ruby. In S. Y. Shin and S. Ossowski, editors, SAC, pages 1859–1866, Honolulu, Hawaii, USA, Mar. 2009. ACM. Google ScholarDigital Library
- A. Guha, J. Matthews, R. B. Findler, and S. Krishnamurthi. Relationally-parametric polymorphic contracts. In P. Costanza and R. Hirschfeld, editors, DLS, pages 29–40. ACM, 2007. Google ScholarDigital Library
- R. Hinze, J. Jeuring, and A. Löh. Typed contracts for functional programming. In P. Wadler and M. Hagiya, editors, Proceedings of the 8th International Symposium on Functional and Logic Programming FLOPS 2006, pages 208–225, Fuji Susono, Japan, Apr. 2006. Springer. Google ScholarDigital Library
- C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12:576–580, 1969. Google ScholarDigital Library
- H. Hosoya, J. Vouillon, and B. C. Pierce. Regular expression types for XML. ACM TOPLAS, 27(1), 2004. Google ScholarDigital Library
- M. Keil and P. Thiemann. Blame assignment for higher-order contracts with intersection and union. Technical report, Institute for Computer Science, University of Freiburg, 2015.Google Scholar
- B. Meyer. Object-Oriented Software Construction. Prentice-Hall, 1988. Google ScholarDigital Library
- B. Meyer. Object-Oriented Software Construction. Prentice-Hall, Upper Saddle River, NJ, USA, 2nd edition, 1997. Google ScholarDigital Library
- B. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.Google Scholar
- B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, Dec. 1991. Google ScholarDigital Library
- J. G. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, Sept. 2006.Google Scholar
- S. Tobin-Hochstadt and M. Felleisen. Interlanguage migration: From scripts to programs. In Dynamic Languages Symposium, DLS 2006, pages 964–974, Portland, Oregon, USA, 2006. ACM. Google ScholarDigital Library
- S. Tobin-Hochstadt and M. Felleisen. The design and implementation of typed scheme. In P. Wadler, editor, Proc. 35th ACM Symp. POPL, pages 395–406, San Francisco, CA, USA, Jan. 2008. ACM Press. Google ScholarDigital Library
- S. Tobin-Hochstadt and D. Van Horn. Higher-order symbolic execution via contracts. In G. T. Leavens and M. B. Dwyer, editors, OOPSLA, pages 537–554. ACM, 2012. Google ScholarDigital Library
- J. A. Tov and R. Pucella. Stateful contracts for affine types. In A. D. Gordon, editor, ESOP 2010, volume 6012 of LNCS, pages 550–569. Springer, 2010. Google ScholarDigital Library
- P. Wadler and R. B. Findler. Well-typed programs can’t be blamed. In Proc. 18th ESOP, volume 5502 of LNCS, pages 1–16, York, UK, Mar. 2009. Springer. Google ScholarDigital Library
- A. K. Wright and R. Cartwright. A practical soft type system for Scheme. ACM TOPLAS, 19(1):87–152, Jan. 1997. Google ScholarDigital Library
Index Terms
Blame assignment for higher-order contracts with intersection and union
Recommendations
Blame assignment for higher-order contracts with intersection and union
ICFP 2015: Proceedings of the 20th ACM SIGPLAN International Conference on Functional ProgrammingWe present an untyped calculus of blame assignment for a higher-order contract system with two new operators: intersection and union. The specification of these operators is based on the corresponding type theoretic constructions. This connection makes ...
Does blame shifting work?
Contract systems, especially of the higher-order flavor, go hand in hand with blame. The pragmatic purpose of blame is to narrow down the code that a programmer needs to examine to locate the bug when the contract system discovers a contract violation. ...
The root cause of blame: contracts for intersection and union types
Gradual typing has emerged as the tonic for programmers with a thirst for a blend of static and dynamic typing. Contracts provide a lightweight form of gradual typing as they can be implemented as a library, rather than requiring a gradual type system.
...
Comments