A formal specification of the Haskell 98 module system

ABSTRACT

Many programming languages provide means to split large programs into smaller modules. The module system of a language specifies what constitutes a module and how modules interact.This paper presents a formal specification of the module system for the functional programming language Haskell. Although many aspects of Haskell have been subjected to formal analysis, the module system has, to date, been described only informally as part of the Haskell language report. As a result, some aspects of it are not well understood or are under-specified; this causes difficulties in reasoning about Haskell programs, and leads to practical problems such as inconsistencies between different implementations. One significant aspect of our work is that the specification is written in Haskell, which means that it can also be used as an executable test-bed, and as a starting point for Haskell implementers.

REFERENCES

• 1: B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.
• 2: Karl-Filip Faxén, A static semantics for Haskell, Journal of Functional Programming, v.12 n.5, p.295-357, July 2002 [doi>10.1017/S0956796802004380]
• 3: T. Hallgren. Home Page of the Proof Editor Alfa. http://www.cs.chalmers.se/~hallgren/Alfa/, 1996-2002.
• 4: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 5: M. P. Jones. Typing Haskell in Haskell. In Proceedings of the 3rd Haskell Workshop, Paris, France, October 1999.
• 6: Xavier Leroy, A modular module system, Journal of Functional Programming, v.10 n.3, p.269-303, May 2000 [doi>10.1017/S0956796800003683]
• 7: David B. MacQueen, Using dependent types to express modular structure, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.277-286, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512670]
• 8: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 9: S. Peyton Jones and J. Hughes (editors). Report on the programming language Haskell 98. Technical Report YALEU/DCS/RR-1106, Yale University, CS Dept., Feb. 1999.
• 10: S. Peyton Jones and P. Wadler. A static semantics for Haskell. Unpublished draft, 1992.
• 11: S. Peyton Jones (editor). Report on the programming language Haskell 98. http://research.microsoft.com/~simonpj/haskell98-revised/, March 2002.
• 12: M. Shields and S. Peyton Jones. First class modules for Haskell. In 9th International Conference on Foundations of Object-Oriented Languages (FOOL 9), Portland, Oregon, pages 28-40, Jan. 2002.
• 13: The GHC team. The Glasgow Haskell Compiler user's guide version 5.04. http://haskell.org/ghc/, July 2002.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Modules, packages; Recursion

General Terms:
Documentation, Languages, Standardization

Keywords:
Haskell, module system, specification