From: Philip Lee Wadler Date: Sat, 27 Feb 88 15:33:30 GMT To: bob@lfcs.ed.ac.uk, fplangc@cs.ucl.ac.uk, mads@lfcs.ed.ac.uk, plw@cs.glasgow.ac.uk Subject: Overloading in Haskell Sender: fplangc-request@cs.ucl.ac.uk Proposal: Overloading in Haskell Phil Wadler 24 February 1988 Overloading was a topic that sparked much discussion at the Yale meeting. It seemed clear that if the language was to be usable, we would at least need overloading of operations such as "+" and "*". The overall philosophy of the language suggested that we should do this in as general a way as possible, rather than just as a special case for a few operators. There appeared to be no easy "off-the-shelf" solution available for us to use. A worrying point was exemplified by the definition square x = x * x Since "*" applies to values of both type "int" and type "float", shouldn't "square" apply to both as well? Clearly this was desirable, but we could see no easy way to achieve it. (The simplest method leads to a potential blow-up when the original source with overloading is translated to a core language with overloading removed.) Another source of discussion was the "polymorphic equality" operator. The "polymorphic equality" operation found in Standard ML and Miranda is, from some perspectives, an odd beast. Standard ML requires an extension to the type system, "equality types", to guarantee, for example, that two functions are never compared for equality. Further, polymorphic equality is not "lambda definable"---it must be defined as a new primitive. This poses problems for some implementations, such as TIM (though not insurmountable ones). It was unclear whether it should be possible to extend the polymorphic equality operator with user-defined equality operations over abstract types. This proposal suggests a new approach to dealing with overloading. It provides a solution to the "square" problem. It is possible at compile-time to translate a program with overloading to a program without overloading, and to do so in a way that avoids blow-up. Somewhat to my surprise, it also provides a solution to the polymorphic equality problem! I have organised this paper so that well-baked ideas appear near the beginning, and ideas become more poorly-baked as one approaches the end. Part 1 presents a limited form of overloading; it can be viewed as one way of making concrete the ideas for overloading discussed at the Yale meeting. I first heard the idea from Jon, but it turns out to be exactly what is used in the Edinburgh implementation of Standard ML (although it is not included in the language standard). (An interesting aside: Kevin Mitchell claims that the Appel/MacQueen implementation of overloading in Standard ML is more restrictive than the Edinburgh implementation. The problem is that the standards document says that the overloading must be resolvable at compile-time, but says nothing about how it is to be resolved!) Part 2 describes generalised overloading. I have presented the ideas in an informal manner. The formal theory is still being developed. I have discussed these ideas with Bob Harper and Mads Tofte at Edinburgh: we've found no obvious bugs yet, and there appear to be strong relations between these new ideas and some well-developed parts of type theory. Another encouraging development is that, as it turns out, similar ideas have been proposed independently by Kevin Mitchell (as an unimplemented extension to the Edinburgh Standard ML referred to above) and by Nick Rothwell (also at Edinburgh, who has implemented it as an extension to Prolog). Unfortunately, they have not developed the corresponding theory, so important work remains to be done; but the existence of a running implementation based on these ideas is reassuring. Acknowledgements usually come at the end of a paper, but this one requires an acknowledgement to Joe Fasel up front. The original idea of handling overloading on numberical types in a polymorphic way and reflecting this in the type scheme is due to Joe. He first suggested it to me at the POPL meeting in San Diego, immediately following the Yale meeting. The idea has changed very much since then; I'm grateful to Joe, Luca Cardelli, John Hughes, Bob Harper, Mads Tofte, Kevin Mitchell, and Nick Rothwell for discussions that helped it evolve. This paper is organised as follows. Part 0 contains notational preliminaries. Part 1 presents a simple form of overloading. Part 2, which is by far the largest part of the paper, presents a generalised form of overloading. Part 3 concludes. 0. Preliminaries Unlike in Standard ML or Miranda, type quantifiers will be written explicitly. For example: k : \a b. a -> b -> a k = \x y. x Note that I use "\" as concrete syntax for both "for every" in types, and "lambda" in expressions. Which is meant should always be clear from context. One advantage of explicit type quantification is that it eliminates the need to lexically distinguish type variables; thus we avoid uglies such as 'a in Standard ML or *** in Miranda. In the Hindley/Milner type system, quantifiers may only appear at the outer level of a type. For example, the type given above for "k" is legal, whereas the type "\a. a -> (\b. b -> a)" is not. I will use ":" as concrete syntax for "has type", and "::" as concrete syntax for "cons". I assume the existence of two types, "int" and "float", defined in the standard prelude, together with the operations such as intadd : int -> int -> int intmul : int -> int -> int intneg : int -> int and similarly for "float". There is no overloading of constants: "1" has type "int", and "1.0" has type "float". I will write "==" for computable equality, to distinguish it from denotational equality, which is written "=". The difference is that "bottom == bottom" denotes bottom, while "bottom = bottom" denotes True. Computable equality is used for tests performed at run-time, denotational equality for definitions. 1. Simple overloading An identifier is defined to be overloaded by giving one OVERLOAD declaration and several INSTANCE declarations. OVERLOAD (+) : \a. a -> a -> a (*) : \a. a -> a -> a (PREFIX -) : \a. a -> a INSTANCE (+) = intadd (*) = intmul (PREFIX -) = intneg INSTANCE (+) = floatadd (*) = floatmul (PREFIX -) = floatneg The OVERLOAD declaration specifies a type for each overloaded identifier. Each INSTANCE declation specifies a binding of the identifier; the type of the bound value must be an instance of the corresponding type in the OVERLOAD declaration. Every instance of an overloaded identifier must have a type disjoint from every other instance. (Two types are disjoint iff they are not unifiable.) Any identifier may be overloaded. Whether or not that identifier is also an operator (like infix + or prefix -) is an independent issue. Overloading is resolved at compile-time as follows. First, type inference is performed, where the type of the overloaded identifier is taken to be the type given in the OVERLOAD declaration. Second, after type inference each occurrence of an overloaded identifier is examined. If its type matches that of an instance, then the identifier is replaced by the corresponding instance value. If its type matches no instance, then the overloading cannot be resolved, and an error is declared. For example, assume the standard prelude also declares sqrt : float -> float If we write distance (x,y) = sqrt ((x*x) + (y*y)) then type inference dervies distance : (float,float) -> float and the type assigned to "+" and "*" is "float -> float -> float", which matches one of the instance declarations, so "+" and "*" are instantiated as "floatadd" and "floatmul". On the other hand, if we write square x = x * x then type inference derives square : \a. a -> a and the type assigned to "*" is "\a. a -> a -> a", which matches no instance, so this definition is illegal. One way around this is to further overload "square". For example, we could define, OVERLOAD square : \a. a -> a INSTANCE square = squareint INSTANCE square = squarefloat squareint : int -> int squareint x = x * x squarefloat : float -> float squarefloat x = x * x This demonstrates the same problem of potential blow-up mentioned earlier, although now the blow-up is explicit in the source code rather than implicit in the translation to a core language. 2. General overloading This part introduces a generalisation of the simple overloading just described. It allows for "square" to be a true polymorphic function. In addition, it allows for equality to be treated as an overloaded operator, without introducing a special polymorphic equality operation as is done in Miranda and Standard ML. This part is organised as follows. Section 2.1 presents the basic ideas. Section 2.2 shows how to translate programs with overloading into equivalent programs without overloading. Section 2.3 presents the definition of equality as an extended example. Section 2.4 presents illustrates further points by means of a second example. Section 2.5 discusses relationships between this form of overloading, object-oriented programming, and abstract data types. 2.1 Introduction to general overloading The key idea is to introduce predicates over types, and to cluster related groups of overloaded identifiers together and associate them with a predicate. This is done with a slight variant of the previous overload declaration: CLASS num a (+) : a -> a -> a (*) : a -> a -> a (PREFIX -) : a -> a This introduces the type predicate "num", and states that "a" is a numeric type if it has functions named (+), (*), and (PREFIX -), of the appropriate types, defined on it. We declare instances in almost the same way as before: INSTANCE num int (+) = intadd (*) = intmul (PREFIX -) = intneg INSTANCE num float (+) = floatadd (*) = floatmul (PREFIX -) = floatneg The first declaration asserts that "int" is a numeric type, and justifies this assertion by giving appropriate bindings for the relevant operators. The second declaration does the same thing for "float". Given these declarations, the definition of "distance" given before is still valid, and the overloading is resolved in the same way. However, it is now also possible to write a polymorphic definition of "square: square x = x * x There exists a generalised version of the type inference algorithm that works with classes and type predicates. It derives the type double : \a. num a. a -> a The phrase "\a. num a." is read "for every a, such that a is a numeric type". We can now write applications such as "double 1" and "double 2.0", and an appropriate type will be derived for each. On the other hand, writing "double [3]" will yield a type error at run time, because "[int]" (the type "list of int") has not been asserted (via an instance declaration) to be a numeric type. Just as all type quantifiers must come at the beginning of a type, so must all type predicates. Thus, in general a type will always have the following form: zero or more type quantifiers, followed by zero or more type predicates, followed by a type term. 2.2 Translation of general overloading One feature of this form of overloading is that it is possible at compile-time to translate any program containing overloading to an equivalent program that does not. We will distinguish between overloadings of an operator that can be resolved at the point of occurrence (as with "+" and "*" in "distance") and those that cannot (as with "*" is "square"). The former will be called "resolvable", the latter "polymorphic". For resolvable overloading the translation is straightforward: each occurrence of the overloaded identifier is replaced by the corresponding value bound in the relevant instance declaration. For example, the definition of "distance" translates to distance (x,y) = sqrt (floatadd (floatmul x x) (floatmul y y)) For polymorphic overloading, we need to do a little more work. First, for each class declaration we introduce a new type synonym. TYPE num' a = (a -> a -> a, a -> a -> a, a -> a) For each instance, one also declares an object of the corresponding type. numint' : num' int numint' = (intadd, intmul, intneg) numfloat' : num' float numfloat'= (floatadd, floatmul, floatneg) Type predicates correspond to parameters of the corresponding class type. For example, here is the definition of "square" with its type: square : \a. num a. a -> a square x= x * x This translates to square' : \a. num' a -> a -> a square' pkg x = mul x x WHERE (add, mul, neg) = pkg Each application of "square" must be translated to pass in the appropriate extra parameter: square 1 --> square' numint 1 square 2.0 --> square' numfloat 2.0 Note that square' is a perfectly valid function, and has a perfectly valid Hindley/Milner type. Thus, we have translated functions with polymorphic overloading and types with predicates into functions without overloading and types without predicates. 2.3 Example: Equality This section shows, as an extended example, how to define equality using the overloading mechanism. Overloaded equality has some advantages over polymorphic equality: it relies on the general overloading mechanism, rather than introducing special mechanisms such as equality types into the system; it is "lambda definable"; and it is possible for the user to define equality over abstract types. We begin by defining a class for the overloaded equality operation, with "int" and "char" as simple instances: CLASS eq a (==) : a -> a -> bool INSTANCE eq int (==) = intequal INSTANCE eq char (==) = charequal We can now define the "member" operation in the usual way: member : \a. eq a. [a] -> a -> bool member [] y= False member (x :: xs) y= (x == y) \/ (member xs y) The type of "member" need not be given explicitly, as it can be inferred. We may now write terms such as member [1,2,3] 2 member "Haskell" 'k' which both evaluate to True. In just the same style as "member" we can define equality over lists: listequal : \a. eq a. [a] -> [a] -> bool listequal [] [] = True listequal (x::xs) (y::ys) = (x == y) & (listequal xs ys) ELSE listequal xs ys = False Again, the type can be inferred from the definition. We can use a natural extension of the instance mechanism to overload (==) to include equality over lists. INSTANCE \a. eq a. eq [a] (==) = listequal This declaration states that for every type "a" such that "a" is an equality type, "list of a" is also an equality type. Now we may write terms such as "hello" == "goodbye" [[1,2,3],[4,5,6]] == [] member ["Haskell", "Alonzo"] "Moses" which all evaluate to False. Similarly, if "gorp a b" is a user-defined abstract type, parameterised over types "a" and "b", and it has defined on it an operation gorpequal : \a b. eq a. eq b. gorp a b -> gorp a b -> bool then we may write INSTANCE \a b. eq a. eq b. eq (gorp a b) (==) = gorpequal So we may overload (==) with user-defined equality operations on abstract types, without needing to add any special mechanism to the language to accomplish this. We now consider how the translation mechanism applies to this example. First, we get a new type synonym: TYPE eq' a = a -> a -> bool In this case the tuple of functions has degenerated to a single function. We can bind the classes as before: inteq' : eq' int inteq' = intequal chareq' : eq' char chareq' = charequal The member operation translates as: member': \a. eq' a -> [a] -> a -> bool member' eql [] y= False member' eql (x::xs) y= (eql x y) \/ (member eql xs y) Here are two terms and their translations: member [1,2,3] 2--> member' inteq' [1,2,3] 2 member "Haskell" 'k'-->member' chareq' "Haskell" 'k' Similarly, "listequal" translates as: listequal': \a. eq' a -> [a] -> [a] -> bool listequal' eql [] []= True listequal' eql (x::xs) (y::ys)= (eql x y) & (listequal' eql xs ys) ELSE listequal' eql xs ys= False The translation of the instance declaration for list equality is a little trickier. Recall that it reads: INSTANCE \a. eq a. eq [a] (==) = listequal Applying the same translation method as before still leaves us with a type containing a type predicate: listeq' : \a. eq a. eq' [a] listeq' = listequal However, a second translation step removes the type predicate: listeq' : eq' a -> eq' [a] listeq' = listequal' Here are three terms and their translations: "hello" == "goodbye" --> listequal' (listeq' chareq') "hello" "goodbye" [[1,2,3],[4,5,6]] == [] --> listequal' (listeq' (listeq' inteq')) [[1,2,3],[4,5,6]] [] member ["Haskell", "Alonzo"] "Moses" --> member' (listeq' chareq') ["Haskell", "Alonzo"] "Moses" Finally, observe that gorpequal : \a b. eq a. eq b. gorp a b -> gorp a b -> bool will translate into a function that takes two extra parameters, one providing equality over type "a", the other providing equality over type "b". It is worthwhile to compare the relative efficiency of overloaded and polymorphic equality. The individual operations, such as "intequal" are slightly more efficient than polymorphic equality, because the type of the argument is known in advance. On the other hand, operations such as "member" and "listequal" must explicitly pass an equality operation around, an overhead that polymorphic equality avoids. This concludes the extended example. It is hoped that this has served to illustrate the power of this overloading mechanism, and to show that it is possible to translate overloaded definitions into the core language in a systematic way. 2.4 Example: Collections In general, a type predicate may have more than one argument. We given an example of this by showing how to overload operations on collections, such as lists and sets. (The example is intended purely for illustrative purposes; I don't mean to suggest that this should be included in the standard prelude.) CLASS collection a b (.in) : a -> b -> bool (.union) : b -> b -> b singleton : a -> b The predicate "collection a b" asserts that "b" is a collection with elements of type "a". One implementation of a collection is a list: INSTANCE \a. eq a. collection a [a] x .in xs= member xs x xs .union ys = xs ++ ys singleton x = [x] Say that we have also defined the abstract type "set a" with the functions setmember : \a. eq a. set a -> a -> bool setunion : \a. set a -> set a -> set a setsingleton : \a. a -> set a Then a second instance is given by INSTANCE \a. eq a. collection a (set a) x .in xs= setmember xs x (.union)= setunion singleton= setsingleton Finally, say that we have defined operations to implement collections of integers using Godel numbering: godelmember : int -> int -> bool godelunion : int -> int -> int godelsingleton : int -> int (For instance, "godelsingleton n" should return 2 raised to the n'th power.) Then a third instance is given by INSTANCE collection int int m .in n= godelmember m n (.union)= godelunion singleton= godelsingleton This final example, although a bit contrived, demonstrates why the "collection" predicate needs two parameters. A parameterised type, like "set a" is not sufficiently general to capture all possible methods of implementing collections. Here are two examples of functions defined over collections: doublet : \a b. collection a b. a -> a -> b doublet x y = (singleton x) .union (singleton y) squarein : \a b. num a. collection a b. a -> b -> bool squarein x s = (square x) .in s The second example demonstrates how different overloadings can be combined. In both examples, the type need not be given explicitly, as it can be inferred. 2.5 Subclasses In the preceeding, "num" and "eq" were considered as completely separate classes. If we want to use both numerical and equality operations, then these each appear in the type separately: squaremember : \a. eq a. num a. [a] -> a -> bool squaremember xs x = member xs (square a) As a practical matter, this seems a bit odd---we would expect every data type that has (+), (*), and (PREFIX -) defined on it to have (==) defined as well; but not the converse. Thus it seems sensible to make "num" a subclass of "eq". To allow this, the notation is extended so that one may include class names in the signature part of a class declaration: CLASS num a eq a (+) : a -> a -> a (*) : a -> a -> a (PREFIX -) : a -> a This asserts that every type "a" satisfying the predicate "num a" must also satisfy the predicate "eq a". In other words, "num" is a subclass of "eq", or, equivalently, "eq" is a superclass of "num". The instance declarations remain the same as before---but the instance declaration "num int" is only valid if there is also an instance declaration "eq int" active within the same scope. For the preceding definition of "squaremember" we would now infer the type squaremember : \a. num a. [a] -> a -> bool The type predicate "eq a" no longer needs to be mentioned, because it is implied by "num a". In translation terms, we simply add a component to the tuple representing an instance of "num" that stands for the corresponding instance of "eq". Thus, we now have the translations: TYPE eq' a = a -> a -> bool TYPE num' a = (eq' a, a -> a -> a, a -> a -> a, a -> a) eqint': eq' int eqint'= (intequal) numint': num' int numint'= (eqint', intadd, intmul, intneg) squaremember' : \a. num' a -> [a] -> a -> bool squaremember' numpkg x= member eqpkg xs (square numpkg x) WHERE (eqpkg, add, mul, neg) = numpkg square' : \a. num' a -> a -> a square' numpkgx= mul x x WHERE (eqpkg, add, mul, neg) = numpkg And the translation of "member" is the same as before. In general, each class may have any number of sub or superclasses. Here is a contrived example: CLASS top a fun1 : a -> a CLASS left a top a fun2 : a -> a CLASS right a top a fun3 : a -> a CLASS bottom a top a left a right a fun4 : a -> a The relationships among these types can be diagrammed as follows: top / \ / \ left right \ / \ / bottom Although multiple superclasses pose some problems for the usual means of implementing object-oriented languages, they pose no problems for the translation scheme outlined here. At first glance, subclasses may appear to be very similar to subtypes, but there is an important difference. Subtypes are "anti-monotonic" with regard to the function type constructor. That is, if we write a <= b for "a is a subtype of b", then we have (a -> b) <= (a' -> b') iff a' <= a and b <= b' This is anti-monotonic because we have written a' <= a, rather than the reverse. Anti-monotonicity leads to some complications in theories involving subtypes. Subclassing, on the other hand, is not anti-monotonic. For example, the type predicate "num" is more specific than the type predicate "eq", and the type \a. num a. a -> a is more specific than the type \a. eq a. a -> a That is, any type matching the first also matches the second, but not the converse. Anti-monotonicity is not a problem because type predicates can only come at the beginning of a type, and so cannot appear inside a type term built with the function type constructor. 2.6 Object-oriented programming, multiple implementations of abstract types, and assertions. As the name "CLASS" suggests, there are some parallels between object-oriented programming and the ideas described here. In object-oriented languages, a class groups together a related set of operations on a data-type. The object carries these operations, or "methods" around with it at run-time. Here the idea has been slightly generalised: a class declaration groups together operations on one or more related types, and the operations are passed separately, rather than with the objects. In a way, the class mechanism provides for multiple implementations of abstract types. Whenever the type of a function is such that a type predicate is applied only to type variables, then any instance of the class is a suitable argument to the function. In the "collection" example in section 2.4, both "doublet" and "squarein" are polymorhic in this way. Any function that requires only the operations ".in", ".union", and "singleton" on sets could be defined similarly. In effect, the class specifies the signature of an abstract type, and the instances provide different implementations of this type. We saw three possible implementations of set, and there could be any number of additional implementations (some based on concrete types, like lists, and others based on abstract types, using whatever abstraction mechanism the language defines). Even a concrete type, like list, is secure when passed to a function like "doublet" or ".squarein", because the type guarantees that the function can only apply the class operations, and no other operations on lists. Further, the typing guarantees that the implementations match appropriately. For example, "doublet" may be called when the arguments are both represented by lists, or both represented by Godel numbers, but not when one is a list, and one a Godel number. It is also natural to think of adding assertions to the class declaration, specifying properties that each instance must satisfy: CLASS collection a b (.in) : a -> b -> bool (.union) : b -> b -> b singleton : a -> b ;; for all x : a and s, t : b ;; x .in (singleton x) ;; x .in (s .union t) <=> x .in s \/ x .in t It is valid for any proof to rely on these properties, so long as one proves that they hold for each instance declaration. I have written the assertions as comments, because insisting on or verifying proofs of such properties is outside the scope of Haskell (though it would be interesting to consider an extension containing them). 3. Conclusion The mechanism proposed in Section 1 seems straightforward, and I recommend that we adopt that as the approach to overloading. Should we extend this to the mechanism in Section 2? The advantage is a more powerful language: the "square" problem is solved. Also a smaller language: instead of defining polymorphic equality as a new semantic primitive, we can define equality using the overloading mechanism. (We still need to add a little to the language to support equality: each new algebraic type definition must also be taken to include an instance declaration for equality over that type. But this is just syntactic sugar.) Further, it is easy for the user to define equality over an abstract data type. Another advantage is the ability to define overloaded operations such as show : a -> string read : string -> a This seems a convenient thing to be able to do. Note that Miranda defines "show" as a polymorphic operation (like equality), but defining "read" as a polymorphic operation poses problems of type security. Overloading can define both in a type-secure way. On the negative side, the idea is still very new, and its implications are unclear. There appears to be a suitable inference algorithm, but this still needs to be formally specified and proved sound. (I hope to do this before the April meeting; Bob Harper has indicated he may be willing to help with this.) It is also unclear whether in practice the inferred types will be cluttered with a large number of type predicates. (Though the experience of Standard ML with equality types suggests that this may not be a problem.) The natural method of implementing overloading requires that each predicate in a type corresponds to a tuple of operations to be passed at run-time. Is the overhead in this acceptable? Comments are very welcome!