Transparent Modules with Fully Syntactic Signatures

Abstract

ML-style modules are valuable in the development and maintenance of large software systems, unfortunately, none of the existing languages support them in a fully satisfactory manner. The official SML'97 Definition does not allow higher-order functors, so a module that refers to externally defined functors cannot accurately describe its import interface. MacQueen and Tofte 26 extended SML'97 with fully transparent higher-order functors, but their system does not have a type-theoretic semantics thus fails to support fully syntactic signatures. The systems of manifest types 19, 20 and translucent sums 12 support fully syntactic signatures but they may propagate fewer type equalities than fully transparent functors. This paper presents a module calculus that supports both fully transparent higher-order functors and fully syntactic signatures (and thus true separate compilation). We give a simple type theoretic semantics to our calculus and show how to compile it into an F omega-like lambda-calculus extended with existential types.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 24, 1999
Accession Number
ADA436465

Entities

People

  • Zhong Shao

Organizations

  • Yale University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Calculus
  • Information Operations
  • Language
  • Linguistics
  • Mathematics
  • New York
  • Notation
  • Semantics
  • Social Sciences
  • Specifications
  • Symmetry
  • Three Dimensional
  • Translations
  • Transparencies
  • Words (Language)

Fields of Study

  • Computer science

Readers

  • Computational Linguistics