COMP3161/COMP9164 Supplementary Lecture Notes
Overloading
Liam O’ ̊ November 10, 2021
So far, all the operations we have in MinHS are either monomorphic or polymorphic. Monomorphic operations work on a specific type, for example addition (+) : Int → Int → Int. Polymorphic operations 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. Note the operator name. The programmer must remember to use + for adding Ints, and +Float for adding Floats This would make the language rather annoying to use. It gets even worse for a language with a more realistic set of types, including integers and floats of different size.
Even worse, consider an operation such as ==. Ideally, == should work not just on basic types, but also on compound types, like pairs and sum types, but not on function types.
We want a way to refer to multiple functions by the same name, and have the exact implemen- tation determined by type of its arguments. This is called overloading or ad-hoc polymorphism.
1 Type Classes in 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 where 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
In words: for all types a in the 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 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
Also, generative rules that specify instances that themselves depend on another instance:
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
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 adapt our existing typing rules to this new feature, we thread our axiom set A through them but otherwise leave them unchanged. For example, here is the typing rule for fst before and after:
Γ ⊢ e : τ1 × τ2 A | Γ ⊢ e : τ1 × τ2 Γ ⊢ fst e : τ1 A | Γ ⊢ snd e : τ2
To use an overloaded type, we 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:
1. Weknowthat(+)::∀a.(Numa)⇒a→a→a∈Γ.
2. We know that Num Float ∈ A.
3. Instantiating the type variable a, we can conclude that (+) :: (Num Float) ⇒ Float → Float → Float.
4. Using the Inst rule above and (3), we can conclude (+) :: Float → Float → Float
5. By the function application rule, we can conclude 3.2 + 4.4 :: Float as required.
Here’s a more formal derivation, where we’ll abbreviate F as Float.
(+) : ∀a. (Num a) ⇒ a → a → a ∈ Γ A | Γ ⊢ (+) : ∀a. (Num a) ⇒ a → a → a A | Γ ⊢ (+) : (Num F) ⇒ F → F → F
Num F ∈ A A Num F
A | Γ ⊢ (+) : F → F → F
A | Γ ⊢ (+) 3.2 : F → F
A | Γ ⊢ 3.2 : F
A | Γ ⊢ 4.4 : F The following example derivation illustrates the use of the Gen rule. We will assume that
A | Γ ⊢ 3.2 + 4.4 : F
x:a∈Γandy:a∈Γ. Wecanthenderiveatypefortheexpressionx+yasfollows:
(+) : ∀b. (Num b) ⇒ b → b → b ∈ Γ
Num a, A | Γ ⊢ (+) : ∀b. Num b ⇒ b → b → b Num a, A | Γ ⊢ (+) : Num a ⇒ a → a → a
Num a, A | Γ ⊢ (+) : a → a → a
Num a, A | Γ ⊢ (+) x : a → a
Num a, A | Γ ⊢ x : a
Num a, A | Γ ⊢ y : a
Num a, A | Γ ⊢ x + y : a A | Γ ⊢ x + y : Num a ⇒ a
This type has a free type variable, which is appropriate since x,y occur in the typing context. This derivation also uses the Inst rule to massage the type of (+); note that we elided the side condition Num a, A Num a.
3 Overloading Resolved
Up to this point, we only discussed the effect overloading has on the static semantics. What 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 languages, objects typically know what to do — that is, an object is asso- ciated 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
type EqDict a = (a → a → Bool × a → a → Bool)
Instances become values of the dictionary type:
instance where
True == True = True False == False = True
== = False a /= b = not(a==b)
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)
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]