Variance and Generalized Constraints for C# Generics
Variance and Generalized Constraints for C# Generics
复制标题
C 的方差和广义约束
DOI：
--
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
Dachuan Yu
中科院分区：
文献类型：
--
作者：
B. Emir;A. Kennedy;Claudio V. Russo;Dachuan Yu
C$^{Sharp}$中的泛型类型对子类型的行为是不变的。我们为C$^{Sharp}$提出了一个类型安全变量系统，该系统支持在泛型类型上声明协变和逆变类型参数。为了支持更广泛的方差应用，我们还使用类和方法上的任意子类型断言来概括现有的约束机制。即使在没有方差的情况下，这种扩展也是有用的，并且包含了为通用代数数据类型(GADT)建议的等式约束。我们以声明式和语法制导的方式形式化化子类型关系，并描述和证明了约束闭包和子类型算法的正确性。最后，我们形式化并证明了带有变量类和广义约束的轻量级语言的类型安全定理。
Generic types in C$^{sharp}$ behave invariantly with respect to subtyping. We propose a system of type-safe variance for C$^{sharp}$ that supports the declaration of covariant and contravariant type parameters on generic types. To support more widespread application of variance we also generalize the existing constraint mechanism with arbitrary subtype assertions on classes and methods. This extension is useful even in the absence of variance, and subsumes equational constraints proposed for Generalized Algebraic Data Types (GADTs). We formalize the subtype relation in both declarative and syntax-directed style, and describe and prove the correctness of algorithms for constraint closure and subtyping. Finally, we formalize and prove a type safety theorem for a featherweight language with variant classes and generalized constraints.