Anzeige
Erschienen in:
1999 | OriginalPaper | Buchkapitel
Non-dependent Types for Standard ML Modules
verfasst von : Claudio V. Russo
Erschienen in: Principles and Practice of Declarative Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Two of the distinguishing features of the Standard ML modules language are its term dependent type syntax and the use of type generativity in its static semantics. From a type-theoretic perspective, the former suggests that the language involves first-order dependent types, while the latter has been regarded as an extra-logical device that bears no direct relation to type-theoretic constructs. We reformulate the existing semantics of Standard ML modules to reveal a purely second-order type theory. In particular, we show that generativity corresponds precisely to existential quantification over types and that the remainder of the modules type structure is based exclusively on the second-order notions of type parameterisation, universal type quantification and subtyping. Our account is more direct than others and has been shown to scale naturally to both higher-order and first-class modules.