Static dependent types for first class modules

ABSTRACT

Static dependent types are the basis of a new type system that permits types and values to be packaged together into first class modules. Unlike other approaches to modules, static dependent types permit unrestricted access to the types and values in first class modules without sacrificing static type checking or data abstraction. Static dependent types are type safe in the presence of side effects because they rely on an effect system that can make deductions conventional type systems cannot. Experience with an implementation, built as an extension to the FX-87 programming language, shows that static dependent types can be used for building large systems.

REFERENCES

• Boehm & Demers 86: Hans-Juergen Boehm , Alan Demers, Implementing RUSSELL, Proceedings of the 1986 SIGPLAN symposium on Compiler construction, p.186-195, June 25-27, 1986, Palo Alto, California, United States
• Boehm et al. 80: Hans Boehm , Alan J. Demers , James E. Donahue, An Informal Description of Russell, Cornell University, Ithaca, NY, 1980
• Burstall & Lampson 84: R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
• Cardelli 89: Luca Cardelli. Typeful programming. In IFIP Advanced Seminar on Formal Description of Programming Concepts, 1989.
• Gifford et al. 87: David K. Clifford, Pierre Jouvelot, John M. Lucassen, &rid Mark A. Sheldon. FX.87 Reference Manual. Technical Report MIT/LCS/TR-407, M.I.T. Laboratory for Computer Science, September 1987.
• Hook & Howe 86: James G. Hook , Douglas J. Howe, Impredicative Strong Existential Equivalent to Type:Type, Cornell University, Ithaca, NY, 1986
• Jouvelot & Giffozd 88: Pierre Jouvelot and David K. Gifford. The FX-87 interpreter, in Proceedings of the ~nd Int q. Conf. on Comp. Lang., Miami,Florida, October 1988.
• Liskov et al. 81: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• Lucassen & Gifford 88: J. M. Lucassen , D. K. Gifford, Polymorphic effect systems, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-57, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73564]
• MacQueen 84: David MacQueen, Modules for standard ML, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.198-207, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802036]
• McCracken 79: Nancy Jean McCracken. An Investigation of a Programming Language with a Polffmorphic Type Structure. Ph.D. thesis, Syrcuse University, 1979.
• Mitchell & Plotkin 88: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential type, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.3, p.470-502, July 1988 [doi>10.1145/44501.45065]
• Sheldon 90: Mark A. Sheldon. Static Dependent Types lor First. Class Modules. Technical Report MIT/LCS/TR-472, M.I.T. Laboratory for (3omputer Science, 1990.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: LISP
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Functional constructs

General Terms:
Algorithms, Design, Languages