COMP3161/COMP9164 Supplementary Lecture Notes
Overloading
Gabriele Keller, Liam O’Connor November 11, 2019
So far, all the operations we have in MinHS are either monomorphic in that they work on a specific type, as for example addition (+) : Int → Int → Int or they are polymorphic, in that they work on any type at all, such as the identity function of type ∀a. a → a.
In practice, this is not sufficient for a general purpose language. If we add, for example, floating point numbers to MinHS, we want at least all the operations we have on integers to be available on floats as well, so we need (+Float) : Float → Float → Float. However, this would make the language pretty annoying to use, and get even worse for a language with a more realistic set of types, including integers and floats of different size.
The situation is even worse when we consider an operation like checking two values for equality. This should, ideally, not only work on basic types, but on also on compound types, like pairs and sum types (but not on function types).
What we desire is a way to refer to multiple functions by the same name, and have the exact implementation determined based on the type of its arguments. This is called overloading or ad-hoc polymorphism.
1 Type Classes in Haskell
The idea behind type classes is to group a set of types together if they have several, conceptually similar operations in common. For example, in Haskell, the type class within which the methods addition, multiplication, subtraction and such are defined is called Num, and contains the types Int, Integer (not fixed length), Float and Double.
For example, the type of addition is: (+) : ∀ a. Num a ⇒ a → a → a
which reads as: for all types a in type class Num, (+) has the type a ⇒ a → a → a. The constraint Num restricts the types which addition can be applied to.
The Eq type class in Haskell contains all types whose elements can be tested for pairwise equality. When you type :info Eq into GHCi, the interpreter lists all its methods:
(==) :: Eqa ⇒ a → a → Bool (/=) :: Eqa ⇒ a → a → Bool
Also listed are the types which are in this type class. Basic integral types are included:
instance Eq Int instance Eq Float instance Eq Double instance Eq Char instance Eq Bool
Also, generative rules that specify instances that themselves depend on another instance: 1
instance Eq a ⇒ Eq [a]
instance Eq a ⇒ Eq (Maybe a) instance (Eq a, Eq b) ⇒ Eq (a, b)
These are rules about type class membership: if a type a is in Eq, then lists of a are also in Eq, as well as Maybe a. If two types a and b are both in Eq, so are pairs of a and b. Operations on these compound types are implemented in terms of the operations of the argument types. So, two pairs of values are considered to be equal if both of their components are equal:
instance (Eq a, Eq b) ⇒ Eq (a, b) where
(==) (a1, b1) (a2, b2) = (a1 == a2) && (b1 == b2)
And equality of lists can be defined, for example, as follows:
instance Eq a ⇒ Eq [a] where
(==) [] [] = True (==)(a:as)(b:bs)=(a==b)&&(as ==bs) (==) = False
Other examples of predefined type classes are Show and Read. A user can extend these type classes and define new classes.
2 Static Semantics
We write:
f :: ∀a. P ⇒ τ
To indicate that f has the type τ where a can be instantiated to any type under the condition that the constraint P is satisfied. Typically, P is a list of instance constraints, such as Num a or Eq b.
Extending implicitly typed MinHS with type classes, we allow constraints to occur on quantified type variables:
Predicates P ::= C τ
Polytypes π ::= τ | ∀a. π | P ⇒ π Monotypes τ ::= Int|Bool|τ+τ | ··· Class names C
Our typing judgement Γ ⊢ e : π now includes a set of type class axiom schema A: A|Γ⊢e:π
This set contains predicates for all type class instances known to the compiler, including generative instances, which take the form of implications like Eq a ⇒ Eq [a].
To add typing rules for this, we leave the existing rules unchanged, save that they thread our axiom set A through.
In order to use an overloaded type, one must first show that the predicate is satisfied by the known axioms, written A P :
A|Γ⊢e:P⇒π A P e:π
If, adding a predicate to the known axioms, we can conclude a typing judgement, then we can overload the expression with that predicate:
P, A | Γ ⊢ e : π A|Γ⊢e:P ⇒πGen
Putting these rules to use, we could show that 3.2 + 4.4, which uses the overloaded operator (+), is of type Float:
Inst
2
3
1. 2. 3.
4. 5.
Weknowthat(+)::∀a.(Numa)⇒a→a→a∈Γ. We know that Num Float ∈ A.
Instantiating the type variable a, we can conclude that (+) :: (Num Float) ⇒ Float → Float → Float.
Using the Inst rule above and (3), we can conclude (+) :: Float → Float → Float By the function application rule, we can conclude 3.2 + 4.4 :: Float as required.
Overloading Resolved
Up to this point, we only discussed the effect overloading has on the static semantics. But how about the dynamic semantics? At some point, the overloaded function has to be instantiated to the correct concrete operation. This could happen at run time, but that doesn’t seem to be the best way.
In object oriented language, objects typically know what to do — that is, an object is associated with a so-called virtual method or dispatch table, which contains all the methods of the object’s class. This approach isn’t applicable to a language like MinHS, where arguments of an overloaded function aren’t objects and can be of basic type, but we can use a similar idea: we pass the table of all the methods of a class to an overloaded function, and replace the overloaded function with one that simply picks the appropriate method from the table. We call this table a dictionary, and in MinHS, we represent a table with n functions as n-tuple.
Type classes are converted to type declarations for their dictionary:
class Eq a where (==) : a → a → Bool (/=) : a → a → Bool
becomes
type EqDict a = (a → a → Bool × a → a → Bool)
Instances become values of the dictionary type:
instance Eq Bool where
True == True = True False == False = True
== = False a /= b = not(a==b)
becomes
True ==Bool True = True False ==Bool False = True
==Bool = False a /=Bool b = not (a ==Bool b)
eqBoolDict = ((==Bool), (/=Bool)) Programs that rely on overloading now take dictionaries as parameters:
same ::∀a. (Eq a)⇒[a]→Bool
same [] = True
same (x : []) = True
same (x:y:xs)=x==y∧same (y:xs)
Becomes: 3
same :: ∀a. (EqDict a) →[a] → Bool
same eq [] = True
same eq (x : []) = True
same eq (x:y:xs)=(fsteq)xy∧same eq (y:xs)
In some cases, we can make instances also predicated on some constraints:
instance (Eq a) ⇒ (Eq [a]) where
[] == [] = True
(x:xs) == (y:ys) = x==y∧(xs==ys)
== = False a /= b = not(a==b)
Such instances are transformed into functions to produce new dictionaries: eqList :: EqDict a → EqDict [a]
4