关于“函数”交与并类型的同构
On Isomorphism of "Functional" Intersection and Union Types
摘要：
类型同构对于检索库组件很有用，因为库中的函数可以具有与用户期望的类型不同但同构的类型。此外，类型同构免费提供了在用户程序中包含正确类型的函数所需的强制。本文研究了具有交类型和并类型的系统的类型同构问题。在交和并的存在下，同构不是一个同余，不能用等式的方式来描述。仍然可以给出一个特征，但由于函数类型和非函数类型之间的干扰而变得非常复杂。在本文中，我们将每个原子类型解释为将任何参数映射到类型本身的解释中的函数集，从而面临这个缺点。这一选择是由斯科特的逆极限模型的初始投影提出的。本文的主要结果是保证型同构的条件，基于同构保持约简。
英文摘要：
Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the function in the user program with the right type. The present paper faces the problem of type isomorphism in a system with intersection and union types. In the presence of intersection and union, isomorphism is not a congruence and cannot be characterised in an equational way. A characterisation can still be given, quite complicated by the interference between functional and non functional types. This drawback is faced in the paper by interpreting each atomic type as the set of functions mapping any argument into the interpretation of the type itself. This choice has been suggested by the initial projection of Scott's inverse limit lambda-model. The main result of this paper is a condition assuring type isomorphism, based on an isomorphism preserving reduction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
