Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
An Extension of ML with First-Class Abstract Types In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, San Francisco, June 1992 Konstantin Laufer, New York University, laufer@cs.nyu.edu Martin Odersky, Yale University, odersky@cs.yale.edu This paper presents a semantic extension of ML, where the component types of a datatype may be existentially quantified. We show how datatypes over existential types add significant flexibility to the language without even changing ML syntax; in particular, we give examples demonstrating how we express o first-class abstract types, o multiple implementations of a given abstract type, o heterogeneous aggregates of different implementations of the same abstract type, and o dynamic dispatching of operations with respect to the implementation type. We have a deterministic Damas-Milner inference system for our language, which leads to a syntactically sound and complete type reconstruction algorithm. Furthermore, the type system is semantically sound with respect to a standard denotational semantics. Most previous work on existential types does not consider type reconstruction. Other work appears to be semantically unsound or does not permit polymorphic instantiation of variables of existential type. By contrast, in our system such variables are let-bound and may be instantiated polymorphically. We have implemented a Standard ML prototype of an interpreter with type reconstruction for our core language, Mini-ML extended with recursive datatypes over existentially quantified component types. All examples from this paper have been developed and tested using our interpreter.