A Formal Specification for the Haskell 98 Module System

A Formal Specification for the Haskell 98 Module System

Iavor S. Diatchki, Mark P. Jones, and Thomas Hallgren. In Proceedings of the ACM SIGPLAN 2002 Haskell Workshop, Pittsburgh, PA, October 2002.


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.

Available by http in pdf.