Polymorphic Type Inference and Abstract Data Types
NEW YORK UNIV NY DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
Many statically typed programming languages provide an abstract data type construct, such as the package in Ada, the cluster in CLU, and the module in Modula2. However, in most of these languages, instances of abstract data types are not first-class values, and they cannot be assigned to a variable, passed as a function parameter, or returned as a function result. The higher-order functional language ML has a strong and static type system with parametric polymorphism. In addition, ML provides type reconstruction and does not require type declarations for identifiers. Although the ML module system supports abstract data types, their instances cannot be used as first-class values for type-theoretic reasons. In this thesis, the author describes a family of extensions of ML. While retaining MLs static type discipline, type reconstruction, and most of its syntax, he adds significant expressive power to the language by incorporating first-class abstract types as an extension of MLs free algebraic data types. In particular, he is now able to express multiple implementations of a given abstract type, heterogeneous aggregates of different implementations of the same abstract type, and dynamic dispatching of operations with respect to the implementation type. Following Mitchell and Plotkin, he formalizes abstract types in terms of existentially quantified types, and proves that this type system is semantically sound with respect to a standard denotational semantics. He then presents an extension of Haskell, a non-strict functional language that uses type classes to capture systematic overloading. This language results from incorporating existentially quantified types into Haskell and gives first-class abstract types with type classes as their interfaces. One can now express heterogeneous structures over type classes. The language is statically typed and offers comparable flexibility to object-oriented languages.
- Computer Programming and Software