Principal Type Schemes for Modular Programs

13 years 10 months ago

Download ttic.uchicago.edu

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 oﬃcial Deﬁnition and the alternative Harper-Stone semantics of Standard ML are diﬃcult to implement correctly. To bolster this claim, we oﬀer a series of short example programs on which no existing SML typechecker follows the behavior prescribed by either formal deﬁnition. It is unclear how to amend the implementations to match the deﬁnitions or vice versa. Instead, we propose a way of deﬁning how type inference interacts with modules that is more liberal than any existing deﬁnition 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...

Derek Dreyer, Matthias Blume

Real-time Traffic