Type isomorphisms in a type-assignment framework
Type isomorphisms in a type-assignment framework
复制标题
类型分配框架中的类型同构
DOI：
10.1145/143165.143208
复制
发表时间：
1992
期刊：
影响因子：
--
通讯作者：
R. D. Cosmo
中科院分区：
文献类型：
--
作者：
R. D. Cosmo
本文包含对配备 ML 风格多态类型推理机制的语言的同构类型的完整处理。令人惊讶的是，所获得的结果与人们普遍认为 ML 是二阶 λ 演算的子集的看法相矛盾：我们可以提供核心 ML 语言中保持的类型同构，但在二阶 λ 演算中则不然。这种新的同构不仅允许为 ML 风格语言中的所有类型同构提供完整的（且可判定的）公理化（这是库搜索中类型作为规范范式的相关问题），而且还提出了一种自然扩展，在某种意义上完成了 ML 中的类型推断机制。此扩展易于实现，并且允许进一步了解 let 多态构造的本质。
This paper contains a full treatment of isomorphic types for languages equipped with an ML style polymorphic type inference mechanism. Surprisingly enough the results obtained contradict the common-place feeling that (the core of) ML is a subset of second order λ-calculus: we can provide an isomorphism of types that holds in the core ML language, but not in second order λ-calculus. This new isomorphism not only allows to provide a complete (and decidable) axiomatisation of all the type isomorphic in ML style languages, a relevant issue for the type as specifications paradigm in library searches, but also suggest a natural extension that in a sense completes the type-inference mechanism in ML. This extension is easy to implement and allows to get a further insight in the nature of the let polymorphic construct.