Hostname: page-component-6bf8c574d5-xtvcr Total loading time: 0 Render date: 2025-02-20T23:32:40.895Z Has data issue: false hasContentIssue false
  • English
  • Français

Blame and coercion: Together again for the first time

Part of: Gradual Typing

Published online by Cambridge University Press:  13 October 2021

JEREMY G. SIEK Open the ORCID record for JEREMY G. SIEK [Opens in a new window] ,
PETER THIEMANN  and
PHILIP WADLER
JEREMY G. SIEK
Affiliation:
Department of Computer Science, Bloomington, Indiana (e-mail: [email protected])
PETER THIEMANN
Affiliation:
Faculty of Engineering, Freiburg, Germany (e-mail: [email protected])
PHILIP WADLER
Affiliation:
School of Informatics, Edinburgh (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop four calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are as follows: $\lambda{B}$ , based on the blame calculus of Wadler and Findler (2009); $\lambda{C}$ , inspired by the coercion calculus of Henglein (1994); $\lambda{S}$ inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006); and $\lambda{T}$ based on the threesome calculus of Siek and Wadler (2010). While $\lambda{B}$ and $\lambda{T}$ are little changed from previous work, $\lambda{C}$ and $\lambda{S}$ are new. Together, $\lambda{B}$ , $\lambda{C}$ , $\lambda{S}$ , and $\lambda{T}$ provide a coherent foundation for design, implementation, and optimization of gradual types. We define translations from $\lambda{B}$ to $\lambda{C}$ , from $\lambda{C}$ to $\lambda{S}$ , and from $\lambda{S}$ to $\lambda{T}$ . Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: $\lambda{C}$ has a particularly simple definition, and the subtle definition of blame safety for $\lambda{B}$ is justified by the simple definition of blame safety for $\lambda{C}$ . Our calculus $\lambda{S}$ is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from $\lambda{C}$ to $\lambda{S}$ to establish an equational theory of coercions; and second, using full abstraction from $\lambda{B}$ to $\lambda{S}$ to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.

Type
Research Article
Information
Journal of Functional Programming , Volume 31 , 2021 , e20
Check for updates
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Abadi, M., Cardelli, L., Pierce, B. & Plotkin, G. (1991) Dynamic typing in a statically typed language. ACM Trans. Prog. Lang. Syst. 130 (2), 0 237–268.CrossRefGoogle Scholar
Ahmed, A., Findler, R. B., Siek, J. G. & Wadler, P. (2011) Blame for all. In Principles of Programming Languages (POPL), pp. 201–214.CrossRefGoogle Scholar
Ahmed, A., Jamner, D., Siek, J. G. & Wadler, P. (2017) Theorems for free for free: Parametricity, with and without types. In International Conference on Functional Programming, ICFP.CrossRefGoogle Scholar
Aiken, A., Wimmers, E. L. & Lakshman, T. K. (1994) Soft typing with conditional types. In POPL ’94: Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, New York, NY, USA: ACM Press, pp. 163–173.CrossRefGoogle Scholar
Benton, N. (2008) Undoing dynamic typing (declarative pearl). In Functional and Logic Programming, Garrigue, J. & Hermenegildo, M. (eds), vol. 4989. Lecture Notes in Computer Science. Springer Berlin Heidelberg, pp. 224–238.CrossRefGoogle Scholar
Bierman, G., Meijer, E. & Torgersen, M. (2010) Adding dynamic types to C#. In European Conference on Object-Oriented Programming, ECOOP 2010. Springer-Verlag.CrossRefGoogle Scholar
Bierman, G. M., Abadi, M. & Torgersen, M. (2014) Understanding TypeScript. In European Conference on Object-Oriented Programming (ECOOP), pp. 257–281.CrossRefGoogle Scholar
Blume, M. & McAllester, D. (2006) Sound and complete models of contracts. J. Funct. Program., 160 (4&5):0 375–414, 2006.Google Scholar
Bracha, G. & Bak, L. (2011) Dart, a new programming language for structured web programming. In Presentation at GOTO Conference.Google Scholar
Chitil, O. (2012) Practical typed lazy contracts. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, New York, NY, USA: ACM, pp. 67–76.CrossRefGoogle Scholar
Dimoulas, C., Findler, R. B., Flanagan, C. & Felleisen, M. (2011) Correct blame for contracts: no more scapegoating. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, New York, NY, USA: ACM, pp. 215–226.CrossRefGoogle Scholar
Dimoulas, C., Tobin-Hochstadt, S. & Felleisen, M. (2012) Complete monitors for behavioral contracts. In ESOP.CrossRefGoogle Scholar
Disney, T., Flanagan, C. & McCarthy, J. (2011) Temporal higher-order contracts. In Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, New York, NY, USA: ACM, pp. 176–188.CrossRefGoogle Scholar
ECMA. Dart Programming Language Specification, 2nd edition, December 2014.Google Scholar
Feigenbaum, L. (2008) Walkthrough: Dynamic programming in Visual Basic 10.0 and C# 4.0. Available at: http://blogs.msdn.com/b/vbteam/archive/2008/12/17/walkthrough-dynamic- programming-in-visual-basic-10-0-and-c-4-0-lisa-feigenbaum.aspxGoogle Scholar
Felleisen, M. (1987) The Calculi of Lambda-v-CS Conversion: A Syntactic Theory of Control and State in Impereative Higher-Order Programming Languages. PhD thesis, Indiana University.Google Scholar
Feltey, D., Greenman, B., Scholliers, C., Findler, R. B. & St-Amour, V. (2018) Collapsible contracts: Fixing a pathology of gradual typing. Proc. ACM Program. Lang. 20 (OOPSLA), 0 133:1–133:27.CrossRefGoogle Scholar
Findler, R. & Blume, M. (2006) Contracts as pairs of projections. In Functional and Logic Programming (FLOPS).CrossRefGoogle Scholar
Findler, R. B. & Felleisen, M. (2002) Contracts for higher-order functions. In International Conference on Functional Programming (ICFP), pp. 48–59.CrossRefGoogle Scholar
Flanagan, C. (2006) Hybrid type checking. In Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B. & Stata, R. (2002) Extended static checking for Java. In PLDI 2002: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, New York, NY, USA: ACM Press, pp. 234–245.Google Scholar
Flatt, M. & PLT (2014) The Racket Reference 6.0. Technical report, PLT. Available at: http://docs.racket-lang.org/reference/index.html Google Scholar
Floyd, R. W. (1967) Assigning meanings to programs. In Symposium in Applied Mathematics, vol. 19, pp. 19–32.CrossRefGoogle Scholar
Garcia, R. (2013) Calculating threesomes, with blame. In International Conference on Functional Programming (ICFP), pp. 417–428.CrossRefGoogle Scholar
Greenberg, M. (2013) Manifest Contracts. PhD thesis, University of Pennsylvania.Google Scholar
Greenberg, M., Pierce, B. C. & Weirich, S. (2010) Contracts made manifest. In Principles of Programming Languages (POPL) 2010.CrossRefGoogle Scholar
Greenman, B. & Felleisen, M. (2018) A spectrum of type soundness and performance. Proc. ACM Program. Lang. 20 (ICFP), 0 71:1–71:32.CrossRefGoogle Scholar
Gronski, J., Knowles, K., Tomb, A., Freund, S. N. & Flanagan, C. (2006) Sage: Hybrid checking for flexible specifications. In Scheme and Functional Programming Workshop (Scheme), pp. 93–104.Google Scholar
Hejlsberg, A. (2012) Introducing TypeScript. Microsoft Channel 9 Blog.Google Scholar
Henglein, F. (1992) Global tagging optimization by type inference. In LFP 1992: Proceedings of the 1992 ACM Conference on LISP and Functional Programming, New York, NY, USA: ACM Press, pp. 205–215.CrossRefGoogle Scholar
Henglein, F. (1994) Dynamic typing: Syntax and proof theory. Sci. Comput. Program. 220 (3), 0 197–230.Google Scholar
Henglein, F. & Rehof, J. (1995) Safe polymorphic type inference for a dynamically typed language: translating Scheme to ML. In Functional Programming Languages and Computer Architecture (FPCA).CrossRefGoogle Scholar
Herman, D., Tomb, A. & Flanagan, C. (2007) Space-efficient gradual typing. In Trends in Functional Programming (TFP).Google Scholar
Herman, D., Tomb, A. & Flanagan, C. (2010) Space-efficient gradual typing. Higher-Order Symb. Comput. 23, 0 167–189.CrossRefGoogle Scholar
Hinze, R., Jeuring, J. & LÖh, A. (2006) Typed contracts for functional programming. In Proceedings of the Eighth International Symposium on Functional and Logic Programming (FLOPS 2006), Hagiya, M. & Wadler, P. (eds), vol. 3945. Lecture Notes in Computer Science. Springer Berlin/Heidelberg, pp. 208–225.CrossRefGoogle Scholar
Hoare, C. A. R. (1969) An axiomatic basis for computer programming. Commun. ACM 120 (10), 0 576–580.Google Scholar
Kuhlenschmidt, A., Almahallawi, D. & Siek, J. G. (2019) Toward efficient gradual typing for structural types via coercions. In Conference on Programming Language Design and Implementation, PLDI. ACM.CrossRefGoogle Scholar
Lu, K.-C. (2020) Equivalence of Cast Representations in Gradual Typing. Master’s thesis, Indiana University, April 2020.Google Scholar
Matthews, J. & Findler, R. B. (2007) Operational semantics for multi-language programs. In Principles of Programming Languages (POPL), pp. 3–10.CrossRefGoogle Scholar
Meyer, B. (1988) Object-Oriented Software Construction. Prentice Hall.Google Scholar
Moy, C., Nguyundefinedn, P. C., Tobin-Hochstadt, S. & Van Horn, D. (2021) Corpse reviver: Sound and efficient gradual typing via contract verification. Proc. ACM Program. Lang. 50 (POPL).CrossRefGoogle Scholar
Myers, A. (2013) Evaluation contexts, semantics by translation. CS 6110 Lecture 8.Google Scholar
New, M. S., Jamner, D. & Ahmed, A. (2019) Graduality and parametricity: Together again for the first time. Proc. ACM Program. Lang. 40 (POPL).CrossRefGoogle Scholar
Ou, X., Tan, G., Mandelbaum, Y. & Walker, D. (2004) Dynamic typing with dependent types. In IFIP International Conference on Theoretical Computer Science, pp. 437–450.CrossRefGoogle Scholar
Patterson, D., Politz, J. G. & Krishnamurthi, S. (2014) Pyret Language Reference. PLT, Brown University, 5.3.6 edition, 2014. http://www.pyret.org/docs/.Google Scholar
Pierce, B. (2002) Types and Programming Languages. MIT Press.Google Scholar
Rastogi, A., Chaudhuri, A. & Hosmer, B. (2012) The ins and outs of gradual type inference. In Symposium on Principles of Programming Languages, POPL, pp. 481–494.CrossRefGoogle Scholar
Rastogi, A., Swamy, N., Fournet, C., Bierman, G. M. & Vekris, P. (2015) Safe & efficient gradual typing for TypeScript. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015, Rajamani, S.K. & Walker, D. (eds), pp. 167–180. ACM.CrossRefGoogle Scholar
Richards, G., Nardelli, F. Z. & Vitek, J. (2015) Concrete types for TypeScript. In European Conference on Object-Oriented Programming, ECOOP 2015. Springer-Verlag.Google Scholar
Siek, J. (2020a) Toward a Mechanized Compendium of Gradual Typing. Available at: https://arxiv.org/abs/2001.11560Google Scholar
Siek, J., Thiemann, P. & Wadler, P. (2015a) Blame and coercion: Together again for the first time. In Programming Language Design and Implementation (PLDI), pp. 425–435.CrossRefGoogle Scholar
Siek, J. G. (2020b) Gradual typing in Agda repository. Available at: https://github.com/jsiek/gradual-typing-in-agda Google Scholar
Siek, J. G. & Garcia, R. (2012) Interpretations of the gradually-typed lambda calculus. In Scheme and Functional Programming Workshop.CrossRefGoogle Scholar
Siek, J. G. & Taha, W. (2006) Gradual typing for functional languages. In Scheme and Functional Programming Workshop (Scheme), pp. 81–92.Google Scholar
Siek, J. G. & Wadler, P. (2006) Threesomes, with and without blame. In Workshop on Script-to-Program Evolution (STOP), pp. 34–46.Google Scholar
Siek, J. G. & Wadler, P. (2010) Threesomes, with and without blame. In Principles of Programming Languages (POPL), pp. 365–376.CrossRefGoogle Scholar
Siek, J. G., Garcia, R. & Taha, W. (2009) Exploring the design space of higher-order casts. In European Symposium on Programming, ESOP, pp. 17–31.Google Scholar
Siek, J. G, Vitousek, M. M., Cimini, M. & Boyland, J. T. (2015b) Refined criteria for gradual typing. In Summit on Advances in Programming Languages (SNAPL).Google Scholar
Strickland, T. S., Tobin-Hochstadt, S., Findler, R. B. & Flatt, M. (2012) Chaperones and impersonators: run-time support for reasonable interposition. In Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2012.CrossRefGoogle Scholar
Swamy, N., Fournet, C., Rastogi, A., Bhargavan, K., Chen, J., Strub, P.-Y. & Bierman, G. (2014) Gradual typing embedded securely in Javascript. In ACM Conference on Principles of Programming Languages (POPL).CrossRefGoogle Scholar
Thiemann, P. (2014) Session types with gradual typing. In Trustworthy Global Computing – 9th International Symposium, TGC 2014, Rome, Italy, September 5–6, 2014. Revised Selected Papers, Maffei, M. & Tuosto, E. (eds), vol. 8902. Springer, pp. 144–158.CrossRefGoogle Scholar
Tobin-Hochstadt, S. & Felleisen, M. (2006) Interlanguage migration: From scripts to programs. In Dynamic Languages Symposium (DLS), pp. 964–974.CrossRefGoogle Scholar
Tobin-Hochstadt, S. & Felleisen, M. (2008) The design and implementation of typed scheme. In Principles of Programming Languages (POPL), pp. 395–406. doi: 10.1145/1328438.1328486.CrossRefGoogle Scholar
Toro, M., Labrada, E. & Tanter, E. (2019) Gradual parametricity, revisited. Proc. ACM Program. Lang. 30 (POPL), 0 17:1–17:30.CrossRefGoogle Scholar
Vitousek, M., Swords, C. & Siek, J. G. (2017) Big types in little runtime. In Symposium on Principles of Programming Languages, POPL.Google Scholar
Vitousek, M. M., Siek, J. G., Kent, A. & Baker, J. (2014) Design and evaluation of gradual typing for Python. In Dynamic Languages Symposium.CrossRefGoogle Scholar
Vitousek, M. M., Siek, J. G. & Chaudhuri, A. (2019) Optimizing and evaluating transient gradual typing. In Proceedings of the 15th ACM SIGPLAN International Symposium on Dynamic Languages, DLS 2019, New York, NY, USA: Association for Computing Machinery, pp. 28–41.CrossRefGoogle Scholar
Wadler, P. (2015) A complement to blame. In Summit on Advances in Programming Languages (SNAPL).Google Scholar
Wadler, P. & Findler, R. B. (2009) Well-typed programs can’t be blamed. In European Symposium on Programming (ESOP), pp. 1–16.CrossRefGoogle Scholar
Wadler, P., Kokke, W. & Siek, J. G. (2020) Programming Language Foundations in Agda.Google Scholar
Williams, J., Morris, J. G., Wadler, P. & Zalewski, J. (2017) Mixed messages: Measuring conformance and non-interference in TypeScript. In European Conference on Object-Oriented Programming (ECOOP), MÜller, P. (ed), vol. 74. Leibniz International Proceedings in Informatics (LIPIcs), pp. 28:1–28:29. Available at: http://drops.dagstuhl.de/opus/volltexte/2017/7264 Google Scholar
Williams, J., Morris, J. G. & Wadler, P. (2018) The root cause of blame: Contracts for intersection and union types. Proc. ACM Program. Lang. 20 (OOPSLA). doi: 10.1145/3276504.CrossRefGoogle Scholar
Wright, A. K. & Cartwright, R. (1997) A practical soft typing system for Scheme. ACM Trans. Prog. Lang. Syst. 190 (1). Available at: http://portal.acm.org/citation.cfm?id=239912.239917 Google Scholar
Yankov, B. (2013) Definitely Typed Repository. Available at: https://github.com/borisyankov/DefinitelyTyped.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.