A type-theoretic approach to higher-order modules with sharing
A type-theoretic approach to higher-order modules with sharing
复制标题
具有共享功能的高阶模块的类型理论方法
DOI：
10.1145/174675.176927
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
Mark Lillibridge
中科院分区：
文献类型：
--
作者：
R. Harper;Mark Lillibridge
构建和维护大型程序的模块系统的设计是一项艰巨的任务，它提出了许多理论和实践问题。一个基本问题是在编译时通过接口的概念来管理程序单元之间的信息流。经验表明，完全不透明的接口在实践中使用起来很困难，因为隐藏了太多的信息，而完全透明的接口会导致过度的相互依赖，从而给维护和单独编译带来问题。标准ML的“共享”规范通过允许程序员在独立模块中指定类型之间的等式关系来解决这个问题，但表达能力不足以让程序员完全控制模块之间的类型信息传播。
这些问题是从类型论的观点，考虑一个基于吉拉德的系统Fω的微积分解决。微积分不同于以往的研究中所考虑的那些完全依赖于一种新形式的弱和类型在编译时传播信息，相反，基于强和依赖于替代的方法。新形式的和类型允许接口中等式以及类型和种类信息的规范。这提供了对程序单元之间的编译时信息传播的完全控制，并且足以以简单的方式对大多数用户的类型共享规范进行编码。模块被视为“一等”公民，因此系统支持高阶模块和一些面向对象的编程习惯;语言可能很容易被限制为ML类语言中的“二等”模块。
The design of a module system for constructing and maintaining large programs is a difficult task that raises a number of theoretical and practical issues. A fundamental issue is the management of the flow of information between program units at compile time via the notion of an interface. Experience has shown that fully opaque interfaces are awkward to use in practice since too much information is hidden, and that fully transparent interfaces lead to excessive interdependencies, creating problems for maintenance and separate compilation. The “sharing” specifications of Standard ML address this issue by allowing the programmer to specify equational relationships between types in separated modules, but are not expressive enough to allow the programmer complete control over the propagation of type information between modules.
These problems are addressed from a type-theoretic viewpoint by considering a calculus based on Girard's system Fω. The calculus differs form those considered in previous studies by relying exclusively on a new form of weak sum type to propagate information at compile-time, in contrast to approaches based on strong sums which rely on substitution. The new form of sum type allows for the specification of equational, as well as type and kind, information in interfaces. This provides complete control over the propagation of compile-time information between program units and is sufficient to encode in a straightforward way most users of type sharing specifications in Standard ML. Modules are treated as “first-class” citizens, and therefore the system supports higher-order modules and some object-oriented programming idioms; the language may be easily restricted to “second-class” modules found in ML-like languages.