COMPUTER SCIENCE TECHNICAL REPORT ABSTRACTS

Source: http://reports-archive.adm.cs.cmu.edu/anon/2001/abstracts/01-112.html Parent: https://www.cs.cmu.edu/~fox/publications.html


	CMU-CS-01-112 Computer Science Department School of Computer Science, Carnegie Mellon University --- CMU-CS-01-112 Toward a Practical Type Theory for Recursive Modules Derek R. Dreyer, Robert Harper, Karl Crary March 2001 CMU-CS-01-112.ps CMU-CS-01-112.pdf Keywords: Type systems, module systems, functional programming, phase splitting Module systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries. Previous work by Crary, Harper and Puri set out a type-theoretic foundation for recursive modules in the context of a phase-distinction calculus for higher-order modules. Two constructs were introduced for encoding recursive modules: a fixed-point module and a recursively dependent signature. Unfortunately, the implementations of both constructs involve the use of equi-recursive type constructors at higher-order kinds, the equivalence of which is not known to be decidable. In this paper, we show that the practicality of recursive modules is not contingent upon that of equi-recursive constructors. We begin with the theoretical infrastructure described above and study precisely how equi-recursiveness is used in the recursive module constructs, resulting in a clarification and generalization of the underlying ideas. We then examine in depth how the recursive module constructs in the revised type system can serve as the target of elaboration for a recursive module extension to Standard ML. 46 pages
--- Return to: SCS Technical Report Collection School of Computer Science homepage This page maintained by reports@cs.cmu.edu

CMU-CS-01-112 Computer Science Department School of Computer Science, Carnegie Mellon University --- CMU-CS-01-112 Toward a Practical Type Theory for Recursive Modules Derek R. Dreyer, Robert Harper, Karl Crary March 2001 CMU-CS-01-112.ps CMU-CS-01-112.pdf Keywords: Type systems, module systems, functional programming, phase splitting Module systems for languages with complex type systems, such as Standard ML, often lack the ability to express mutually recursive type and function dependencies across module boundaries. Previous work by Crary, Harper and Puri set out a type-theoretic foundation for recursive modules in the context of a phase-distinction calculus for higher-order modules. Two constructs were introduced for encoding recursive modules: a fixed-point module and a recursively dependent signature. Unfortunately, the implementations of both constructs involve the use of equi-recursive type constructors at higher-order kinds, the equivalence of which is not known to be decidable. In this paper, we show that the practicality of recursive modules is not contingent upon that of equi-recursive constructors. We begin with the theoretical infrastructure described above and study precisely how equi-recursiveness is used in the recursive module constructs, resulting in a clarification and generalization of the underlying ideas. We then examine in depth how the recursive module constructs in the revised type system can serve as the target of elaboration for a recursive module extension to Standard ML. 46 pages

--- Return to: SCS Technical Report Collection School of Computer Science homepage This page maintained by reports@cs.cmu.edu