Localized Lama Gradual Typing
https://doi.org/10.15514/ISPRAS-2021-33(3)-5
Abstract
Gradual typing is a modern approach for combining benefits of static typing and dynamic typing. Although scientific research aim for soundness of type systems, many of languages intentionally make their type system unsound for speeding up performance. This paper describes an implementation of a dialect for Lama programming language that supports gradual typing with explicit annotation of dangerous parts of code. The target of current implementation is to grant type safety to programs while keeping their power of untyped expressiveness. This paper covers implementation issues and properties of created type system. Finally, some perspectives on improving precision and soundness of type system are discussed.
About the Author
Viktor Sergeevich KRYSHTAPOVICH
ITMO University
Russian Federation
Russian Federation
Master's student
References
1. Jeremy G. Siek and Walid Taha. Gradual Typing for Functional Languages. In Proc. of the Seventh Workshop on Scheme and Functional Programming, 2006, pp. 81-92.
2. Cameron Moy, Phúc C. Nguyễn et al. Corpse reviver: sound and efficient gradual typing via contract verification. Proceedings of the ACM on Programming Languages, vil. 5, issue POPL, 2021, Article 53, 28 p.
3. D. Boulytchev. JetBrains-Research/Lama source code. Available at https://github.com/JetBrains-Research/Lama, accessed 27/03/2021.
4. Ingkarat Rak-amnouykit, Daniel McCrevan et al. Python 3 types in the wild: a tale of two type systems. In Proc of the 16th ACM SIGPLAN International Symposium on Dynamic Languages (DLS 2020), 2020, pp. 57-70.
5. Guido van Rossum, Ivan Levkivskyi. PEP 483 – The Theory of Type Hints. Available at https://www.python.org/dev/peps/pep-0483/ Request timestamp: 27/03/2021.
6. Guido van Rossum, Jukka Lehtosalo, Łukasz Langa. “PEP 484 – Type Hints. Available at https://www.python.org/dev/peps/pep-0484/, , accessed 27/03/2021.
7. Jukka Lehtosalo et al. Mypy: Optional Static Typing for Python. Available at https://github.com/python/mypy, accessed 27/03/2021.
8. Pytype: A static type analyzer for Python code. Available at https://github.com/google/pytype, accessed 27/03/2021.
9. Sam Tobin-Hochstadt, Vincent St-Amour et al. The Typed Racket Guide. Available at https://docs.racket-lang.org/tsguide/index.html, accessed 27/03/2021.
10. D. Boulytchev. Lama language specification v. 1.10. Available at https://github.com/JetBrains-Research/Lama/blob/1.10/lama-spec.pdf, accessed 27/03/2021.
11. R. Rivest. S-Expressions., 4/05/1997. Available at http://people.csail.mit.edu/rivest/Sexp.txt, accessed 29/03/2021.
12. Amal Ahmed, Dustin Jamneret al. Theorems for free for free: parametricity, with and without types. Proceedings of the ACM on Programming Languages, vol. 1, issue ICFP, 2017, Article 39, 28 p.
13. Jack Williams, J. Garrett Morris, and Philip Wadler. The root cause of blame: contracts for intersection and union types. Proceedings of the ACM on Programming Languages, vol. 2, issue OOPSLA, 2018, Article 134, 29 pages.
14. P. Wadler. A Complement to Blame. In Proc. of the 1st Summit on Advances in Programming Languages (SNAPL 2015), 2015, pp. 309-320.
15. Henry Gordon Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, vol. 74, no. 2. 1953, pp. 358- 366.
16. Benjamin C. Pierce. Types and Programming Languages. The MIT Press, 2002, 648 p.
17. Giuseppe Castagna, Victor Lanvin et al. 2019. Gradual typing: a new perspective. Proceedings of the ACM on Programming Languages, vol. 3, issue POPL, 2019, Article 16, 32 p.
18. Karla Ramírez Pulido, Jorge Luis Ortega-Arjona et al. Gradual Typing Using Union Typing with Records. Electronic Notes in Theoretical Computer Science, vol.354, 2020, pp. 171-186.
19. Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi. 2019. Dynamic type inference for gradual Hindley–Milner typing. Proceedings of the ACM on Programming Languages, vol. 3, issue POPL, 2019, Article 18, 29 pp.
20. V. Kryshtapovich. GraduLama source code Available at https://github.com/kry127/Lama/tree/gradulama, accessed 27/03/2021.
Review
For citations:
KRYSHTAPOVICH V.S. Localized Lama Gradual Typing. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(3):61-76. https://doi.org/10.15514/ISPRAS-2021-33(3)-5
Email this article 