WikiEdge:ArXiv速递/2025-02-27
摘要
- 原文标题:On the State of Coherence in the Land of Type Classes
- 中文标题:类型类领域中的一致性状态
- 发布日期:2025-02-27 21:42:04+00:00
- 作者:Dimi Racordon, Eugene Flesselle, Cao Nguyen Pham
- 分类:cs.PL
- 原文链接:http://arxiv.org/abs/2502.20546v1
原文摘要:Type classes are a popular tool for implementing generic algorithms and data structures without loss of efficiency, bridging the gap between parametric and ad-hoc polymorphism. Since their initial development in Haskell, they now feature prominently in numerous other industry-ready programming languages, notably including Swift, Rust, and Scala. The success of type classes hinges in large part on the compilers' ability to infer arguments to implicit parameters by means of a type-directed resolution. This technique, sometimes dubbed
- implicit programming**, lets users elide information that the language
implementation can deduce from the context, such as the implementation of a particular type class. One drawback of implicit programming is that a type-directed resolution may yield ambiguous results, thereby threatening coherence, the property that valid programs have exactly one meaning. This issue has divided the community on the right approach to address it. One side advocates for flexibility where implicit resolution is context-sensitive and often relies on dependent typing features to uphold soundness. The other holds that context should not stand in the way of equational reasoning and typically imposes that type class instances be unique across the entire program to fend off ambiguities. Although there exists a large body of work on type classes and implicit programming, most of the scholarly literature focuses on a few select languages and offers little insight into other mainstream projects. Meanwhile, the latter have evolved similar features and/or restrictions under different names, making it difficult for language users and designers to get a sense of the full design space. To alleviate this issue, we set to examine Swift, Rust, and Scala, three popular languages featuring type classes heavily, and relate their approach to coherence to Haskell's. It turns out that, beyond superficial syntactic differences, Swift, Rust, and Haskell are actually strikingly similar in that the three languages offer comparable strategies to work around the limitations of the uniqueness of type class instances. 中文摘要:类型类是用于实现通用算法和数据结构而不损失效率的流行工具,弥合了参数化多态和特设多态之间的差距。自它们在Haskell中的最初发展以来,现在它们在许多其他工业级编程语言中占据了重要地位,特别是包括Swift、Rust和Scala。类型类的成功在很大程度上取决于编译器通过类型导向解析推断隐式参数的能力。这种技术有时被称为**隐式编程**,它允许用户省略语言实现可以从上下文中推导出的信息,例如特定类型类的实现。 隐式编程的一个缺点是类型导向解析可能会产生模糊的结果,从而威胁到一致性,即有效程序具有唯一含义的属性。这个问题在社区中引发了关于如何解决它的正确方法的争论。一方主张灵活性,其中隐式解析是上下文敏感的,并且通常依赖于依赖类型特征来保持健全性。另一方则认为上下文不应妨碍等式推理,并且通常要求类型类实例在整个程序中是唯一的,以避免歧义。 尽管关于类型类和隐式编程的研究文献很多,但大多数学术文献集中在少数几种语言上,对其他主流项目的见解很少。与此同时,后者在不同的名称下发展出了类似的特征和/或限制,使得语言用户和设计者难以全面了解设计空间。为了缓解这个问题,我们着手研究Swift、Rust和Scala这三种广泛使用类型类的流行语言,并将它们的一致性方法与Haskell的方法进行比较。结果表明,除了表面上的语法差异外,Swift、Rust和Haskell实际上非常相似,这三种语言提供了可比的策略来应对类型类实例唯一性的限制。