Skip to main content
SpringerLink
Log in

Type isomorphisms for module signatures

  • Tools and Programming Environments
  • Conference paper
  • First Online:
Programming Languages: Implementations, Logics, and Programs (PLILP 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1140))

Abstract

This work focuses on software reuse for languages equipped with a module system. To retrieve modules from a library, it is quite reasonable to use module signatures as a search key, up to a suitable notion of signature isomorphism.

We study a formal notion of isomorphism for module signatures, which naturally extends the notion of isomorphism for types in functional languages. Isomorphisms between module types surprisingly have nontrivial interactions with the theory of isomorphisms of the base language to which the module system is added. We investigate the power of this notion in equating module signatures, and we study its decidability. This work does not impose any limitative assumption on the module system as we handle type declarations in signatures, type sharing and higher order modules.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. María Virginia Aponte. Extending records typing to type parametric modules with sharing. In 20th symposium on Principles of Programming Languages, 1993.

    Google Scholar 

  2. Roberto Di Cosmo. Type isomorphisms in a type assignment framework. In 19th Ann. ACM Symp. on Principles of Programming Languages (POPL), pages 200–210. ACM, 1992.

    Google Scholar 

  3. Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.

    Google Scholar 

  4. Roberto Di Cosmo. Second order isomorphic types. A proof theoretic study on second order λ-calculus with surjective pairing and terminal object. Information and Computation, pages 176–201, June 1995.

    Google Scholar 

  5. Robert Harper, Robin Milner, and Mads Tofte. A type discipline for program modules. In Theory and Practice of Programming Languages, volume 250 of Lecture Notes in Computer Science. Springer Verlag, 1987.

    Google Scholar 

  6. Xavier Leroy. Manifest types, modules, and separate compilation. In 21st symposium on Principles of Programming Languages, pages 109–122. ACM Press, January 1994.

    Google Scholar 

  7. Xavier Leroy. A syntactic approach to type generativity and sharing (extended abstract). In Record of the 1994 ACM-SIGPLAN Workshop on ML and its Applications, pages 1–12. INRIA, June 1994.

    Google Scholar 

  8. Xavier Leroy. Applicative functors and fully transparent higher-order modules. In 22nd symposium on Principles of Programming Languages. ACM Press, January 1995.

    Google Scholar 

  9. Xavier Leroy. The Caml Special Light system. Technical report, INRIA, Roquencourt, Le Chesnay Cedex 78153, France, 1995. Available as ftp://ftp.inria.fr/lang/caml-light/csl*.

    Google Scholar 

  10. Xavier Leroy. The Objective Caml reference manual. Technical report, INRIA, Roquencourt, Le Chesnay Cedex 78153, France, 1996. Available as ftp://ftp.inria.fr/lang/caml-light/ocaml*.

    Google Scholar 

  11. David MacQueen. Modules for standard ML. In ACM Symposium on Lisp and Functional Programming, 1984.

    Google Scholar 

  12. Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. The MIT Press, 1990.

    Google Scholar 

  13. Departement of Defense DoD. Ada reference manual. 1983.

    Google Scholar 

  14. Patrick Parot. Automatisation d'une bibliothèque de modules. In Journées Francophones des Langages Applicatifs, pages 75–98, 1995.

    Google Scholar 

  15. Mikael Rittri. Searching program libraries by type and proving compiler correctness by bisimulation. PhD thesis, University of Göteborg, Göteborg, Sweden, 1990.

    Google Scholar 

  16. Mikael Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1):71–89, 1991.

    Google Scholar 

  17. Pierre Weis and Xavier Leroy. Le langage Caml. InterÉditions, 1993.

    Google Scholar 

  18. Amy Moormann Zaremsky and Jeannette M. Wing. Signature matching: a key to reuse. In SIGSOFT, December 1993. Also available as CMU-CS-93-151, May 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CNAM Conservatoire National des Arts et Métiers, 292, rue St. Martin, 75003, Paris, France

    María -Virginia Aponte

  2. DMI-LIENS (CNRS URA 1347) Ecole Normale Supérieure, 45, Rue d'Ulm, 75230, Paris Cedex 05, France

    Roberto Di Cosmo

Authors
  1. María -Virginia Aponte
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roberto Di Cosmo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Herbert Kuchen S. Doaitse Swierstra

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aponte, M.V., Di Cosmo, R. (1996). Type isomorphisms for module signatures. In: Kuchen, H., Doaitse Swierstra, S. (eds) Programming Languages: Implementations, Logics, and Programs. PLILP 1996. Lecture Notes in Computer Science, vol 1140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61756-6_95

Download citation

  • DOI: https://doi.org/10.1007/3-540-61756-6_95

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61756-3

  • Online ISBN: 978-3-540-70654-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation