A Formal Specification for the Haskell 98 Module System

by Iavor S. Diatchki, Mark P. Jones, Thomas Hallgren

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.

Download

pdf | ps | ps.gz | source code, a version rectifying a minor bug in the function mProgram

pdf | ps | ps.gz | source code, the original:

Iavor S. Diatchki

Last updated: 30 September 2002