Kotlin 的类型系统也是（不）可靠的
编程语言
2024-08-21 v1 软件工程
摘要
类型系统的可靠性是保证运行时不会对不受值支持的任何操作进行操作的基本属性。对于可靠类型系统的类型检查器预计会在每一次类型错误上发出警告。虽然可靠性是许多实际应用中 desirable 的属性，但 2016 年，Amin 和 Tate 首次提出了针对两种主要行业语言：Java 和 Scala 的不可靠性证明。该证明依赖于 use-site 变 variance 和隐式空值。我们提出了针对 Kotlin 的不可靠性证明，这种证明依赖于一种之前未知的语言特性组合。Kotlin 不具有隐式空值，这意味着 Amin 和 Tate 的证明对 Kotlin 不适用。我们的新证明使用 Kotlin 的声明-site 变 variance 规范，且不需要隐式空值。我们在完整呈现此可靠性反面案例，并对每一步进行详细解释。最后，我们对导致此问题的确切语言特性进行了彻底讨论，以及如何修补 Kotlin 编译器以纠正它。
引用
@article{arxiv.2408.10804,
title = {Kotlin's Type System is (Also) Unsound},
author = {Elad Kinsbruner and Hila Peleg and Shachar Itzhaky},
journal= {arXiv preprint arXiv:2408.10804},
year = {2024}
}