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!