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 \(\mathcal{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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Damas, L., Milner, R.: Principal type schemes for functional programs. In: POPL ’82 (1982)
Dreyer, D.: Recursive type generativity. To appear in Journal of Functional Programming. Original version appeared in ICFP ’05.
Dreyer, D.: Practical type theory for recursive modules. Technical Report TR-2006-07, University of Chicago, Department of Computer Science (August 2006)
Dreyer, D., Blume, M.: Principal type schemes for modular programs. Technical Report TR-2007-02, Univ. of Chicago Comp. Sci. Dept. (January 2007)
Dreyer, D., Harper, R., Chakravarty, M.M.T.: Modular type classes. In: POPL ’07 (2007)
Harper, R., Lillibridge, M.: A type-theoretic approach to higher-order modules with sharing. In: POPL ’94 (1994)
Harper, R., Stone, C.: A type-theoretic interpretation of Standard ML. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction: Essays in Honor of Robin Milner, MIT Press, Cambridge (2000)
Kahrs, S., Sannella, D., Tarlecki, A.: The definition of Extended ML: A gentle introduction. Theoretical Computer Science 173(2), 445–484 (1997)
Leroy, X.: Applicative functors and fully transparent higher-order modules. In: POPL 95 (1995)
Leroy, X.: Manifest types, modules, and separate compilation. In: POPL ’94 (1994)
Leroy, X.: Polymorphic Typing of an Algorithmic Language. PhD thesis, Université Paris 7 (1992)
Lillibridge, M.: Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, Carnegie Mellon University (May 1997)
MacQueen, D.: Private communication (2006)
Miller, D.: Unification under a mixed prefix. Journal of Symbolic Computation 14, 321–358 (1992)
Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 348–375 (1978)
Milner, R., et al.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. Transactions on Programming Languages and Systems 10(3), 470–502 (1988)
Odersky, M.: Putting type annotations to work. In: POPL ’96, pp. 54–67 (1996)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Russo, C.V.: Types for Modules. PhD thesis, University of Edinburgh (1998)
Russo, C.V.: First-class structures for Standard ML. Nordic Journal of Computing 7(4), 348–374 (2000)
Wright, A.K.: Polymorphic references for mere mortals. In: Krieg-Brückner, B. (ed.) ESOP 1992. LNCS, vol. 582, Springer, Heidelberg (1992)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Dreyer, D., Blume, M. (2007). Principal Type Schemes for Modular Programs. In: De Nicola, R. (eds) Programming Languages and Systems. ESOP 2007. Lecture Notes in Computer Science, vol 4421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71316-6_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-71316-6_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71314-2
Online ISBN: 978-3-540-71316-6
eBook Packages: Computer ScienceComputer Science (R0)