Loading...
Please wait, while we are loading the content...
Similar Documents
A type system for recursive models (2007)
| Content Provider | CiteSeerX |
|---|---|
| Author | Dreyer, Derek |
| Abstract | There has been much work in recent years on extending ML with recursive modules. One of the most difficult problems in the development of such an extension is the double vision problem, which concerns the interaction of recursion and data abstraction. In previous work, I defined a type system called RTG, which solves the double vision problem at the level of a System-F-style core calculus. In this paper, I scale the ideas and techniques of RTG to the level of a recursive ML-style module calculus called RMC, thus establishing that no tradeoff between data abstraction and recursive modules is necessary. First, I describe RMC’s typing rules for recursive modules informally and discuss some of the design questions that arose in developing them. Then, I present the formal semantics of RMC, which is interesting in its own right. The formalization synthesizes aspects of both the Definition and the Harper-Stone interpretation of Standard ML, and includes a novel two-pass algorithm for recursive module typechecking in which the coherence of the two passes is emphasized by their representation in terms of the same set of inference rules. |
| File Format | |
| Publisher Date | 2007-01-01 |
| Access Restriction | Open |
| Subject Keyword | Recursive Model Recursive Module Data Abstraction Double Vision Problem Design Question Novel Two-pass Algorithm Inference Rule Standard Ml Rmc Typing Rule Much Work Recursive Module Typechecking Harper-stone Interpretation Recursive Ml-style Module Calculus Formal Semantics System-f-style Core Calculus |
| Content Type | Text |
