Loading...
Please wait, while we are loading the content...
Similar Documents
Practical Type Theory for Recursive Modules (2001)
| Content Provider | CiteSeerX |
|---|---|
| Author | Dreyer, Derek |
| Abstract | There has been much work in recent years on extending ML with recursive modules. We consider two problems with the typechecking of recursive modules that have proven to be serious stumbling blocks for existing proposals. Both problems involve the interaction of recursion and data abstraction. The first, more fundamental problem is that, inside a recursive module, one may wish to define an abstract data type in a context where a name for the type already exists. We call this the double vision problem because it has the effect that the programmer sees two distinct versions of the same type when they should only see one. The second, more superficial problem is that the use of data abstraction inside recursive modules often requires the programmer to write duplicate signature annotations for no clear reason. We call this the repetitive stress problem. In this paper, we present a recursive module calculus called RMC that addresses both of these problems. We formalize RMC using an elaboration semantics that translates recursive ML-style modules into an internal module type system. The design of the internal language exploits previous work of ours on a type-theoretic foundation for solving the double vision problem. To remedy the repetitive stress problem, our elaboration algorithm employs a novel form of bidirectional typechecking. Although our approach to elaboration generally follows the framework of Harper and Stone, in certain key details it more closely resembles the Definition of Standard ML. The RMC design thus illustrates a viable hybrid of two approaches to defining ML that are commonly viewed as incompatible. |
| File Format | |
| Language | English |
| Publisher Date | 2001-01-01 |
| Access Restriction | Open |
| Subject Keyword | Recursive Module Practical Type Theory Repetitive Stress Problem Data Abstraction Double Vision Problem Abstract Data Type Bidirectional Typechecking Recursive Ml-style Module Elaboration Algorithm Superficial Problem Recursive Module Calculus Certain Key Detail Viable Hybrid Internal Module Type System Duplicate Signature Annotation Much Work Elaboration Semantics Distinct Version Novel Form Recent Year Internal Language Exploit Previous Work Type-theoretic Foundation Standard Ml Rmc Design Fundamental Problem Clear Reason |
| Content Type | Text |
| Resource Type | Technical Report |
