TR-2006-08
Principal Type Schemes for Modular Programs
Derek Dreyer; Matthias Blume. 26 October, 2006.
Communicated by Pedro Felzenszwalb.
Abstract
Two of the most prominent features of ML are its expressive module
system and its support for Damas-Milner type inference. However,
while the foundations of both these features have been studied
extensively, their interaction has never received a proper
type-theoretic treatment. One consequence is that both the official
Definition and the alternative Harper-Stone semantics of Standard ML
are difficult to implement correctly. To bolster this claim, we offer
a series of short example programs on which no existing SML
typechecker follows the behavior prescribed by either formal
definition. It is unclear how to amend the implementations to match
the definitions or vice versa. Instead, we propose a way of defining
how type inference interacts with modules that is more liberal than any
existing definition or implementation of SML and, moreover, admits a
provably sound and complete typechecking algorithm via a
straightforward generalization of Algorithm W. In addition to being
conceptually simple, our solution exhibits a novel hybrid of the
Definition and Harper-Stone semantics of SML, and demonstrates the
broader relevance of some type-theoretic techniques developed recently
in the study of recursive modules.
Original Document
The original document is available in PDF (uploaded 26 October, 2006 by
Pedro Felzenszwalb).
