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.