Open and Closed Worlds for Overloading: a Definition and Support for Coexistence

Carlos Camarão (Universidade Federal de Minas Gerais, Brazil)

Cristiano Vasconcellos (Universidade Federal de Ouro Preto, Brazil)

Lucília Figueiredo (Universidade Federal de Ouro Preto, Brazil)

João Nicola (Universidade Federal de Minas Gerais, Brazil)

Abstract: The type system of Haskell and some related systems are based on an open world approach for overloading. In an open world, the principal type of each overloaded symbol must be explicitly annotated (in Haskell, annotations occur in type class declarations) and a definition of an overloaded symbol is required to exist only when overloading is resolved. In a closed world, on the other hand, each principal type is determined according to the types of definitions that exist in the relevant context and, furthermore, overloading resolution for an expression considers only the context of the definition of its constituent symbols. In this paper we formally characterize open and closed worlds, and discuss their relative advantages. We present a type system that supports both approaches together, and compare the defined system with Haskell type classes extended with multi-parameter type classes and functional dependencies. We show in particular that functional dependencies are not necessary in order to support multi-parameter type classes, and present an alternative route.

Keywords: closed and open world approaches for overloading, constrained polymorphism, type inference, type system

Categories: D.3.1, D.3.3