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實際上非常相似，這三種語言提供了可比的策略來應對類型類實例唯一性的限制。