Локализованное применение частичной типизации
https://doi.org/10.15514/ISPRAS-2021-33(3)-5
Аннотация
Частичная типизация – это современный подход для сочетания преимуществ статической и динамической типизации. Но несмотря на то, что научные исследования направлены на корректность систем типов, многие языки намеренно делают систему некорректной для ускорения производительности. Данная работа посвящена реализации диалекта языка Лама, который поддерживает частичную типизацию для явно указанных участков кода. Целью реализации является сочетание двух подходов: обеспечение типобезопасности в одних участках кода и производительность языка в других участках кода. Статья раскрывает детали реализации и свойства полученной системы типов. Также рассматриваются способы улучшения полноты и корректности полученной системы типов.
Ключевые слова
Список литературы
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.
Рецензия
Для цитирования:
КРЫШТАПОВИЧ В.С. Локализованное применение частичной типизации. Труды Института системного программирования РАН. 2021;33(3):61-76. https://doi.org/10.15514/ISPRAS-2021-33(3)-5
For citation:
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
Послать статью по эл. почте 