Overloading Subtyping
1
Overloading and Subtyping
Christine Rizkallah
CSE, UNSW Term 3 2020
Overloading
Subtyping
2
Motivation
Suppose we added Float to MinHS.
Ideally, the same functions should be able to work on both Int and Float.
4+6 :: Int 4.3 + 5.1 :: Float
Similarly, a numeric literal should take on whatever type is inferred from context.
(5 :: Int) mod 3 sin(5 :: Float)
Overloading
Subtyping
3
Without Overloading
We effectively have two functions:
(+Int) :: Int → Int → Int (+Float) :: Float → Float → Float
We would like to refer to both of these functions by the same name and have the specific implementation chosen based on the type.
Such type-directed name resolution is called ad-hoc polymorphism or overloading.
Overloading
Subtyping
4
Type Classes
Type classes are a common approach to ad-hoc polymorphism, and exist in various languages under different names:
Type Classes in Haskell
Traits in Rust
Implicits in Scala
Protocols in Swift
Contracts in Go 2
Concepts in C++
Other languages approximate with subtype polymorphism (coming)
Overloading
Subtyping
Type Classes
A type class is a set of types for which implementations (instances) have been provided for various functions, called methods1.
Example (Numeric Types)
In Haskell, the types Int, Float, Double etc. are all instances of the type class Num, which has methods such as (+), negate, etc.
Example (Equality)
In Haskell, the Eq type class contains methods (==) and (/=) for computable equality. What types cannot be an instance of Eq?
5
1Nothing to do with OO methods.
Overloading
Subtyping
We write:
Notation
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.
Example
(+) :: ∀a. (Num a) ⇒ a → a → a (==) :: ∀a. (Eq a) ⇒ a → a → Bool
Is (1 :: Int) + 4.4 a well-typed expression?
No. The type of (+) requires its arguments to have the same type.
6
Overloading
Subtyping
7
Extending MinHS
Extending implicitly typed MinHS with type classes:
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|Γ⊢e:π
This set contains predicates for all type class instances known to the compiler.
Overloading
Subtyping
Typing Rules
The existing rules now just thread A through.
In order to use an overloaded type one must first show that the predicate is satisfied by the known axioms:
A|Γ⊢e:P⇒π A P
Inst
e:π
Right now, A P iff P ∈ A, but we will complicate this situation later.
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
8
Overloading
Subtyping
9
Example
Suppose we wanted to show that 3.2 + 4.4 :: Float.
1 (+)::∀a.(Numa)⇒a→a→a∈Γ.
2 Num Float ∈ A.
3 Using AllE (from previous lecture), we can conclude (+) :: (Num Float) ⇒ Float → Float → Float.
4 Using Inst (on previous slide) and 2 , we can conclude (+) :: Float → Float → Float
5 By the function application rule, we can conclude 3.2 + 4.4 :: Float as required.
Overloading
Subtyping
10
Dictionaries and Resolution
This is called ad-hoc polymorphism because the type checker removes it — it is not a fundamental language feature, but merely a naming convenience.
The type checker will convert ad-hoc polymorphism to parametric polymorphism. Type classes are converted to types:
class Eq a where
(==) : a → a → Bool (/=) : a → a → Bool
becomes
type EqDict a = (a → a → Bool × a → a → Bool)
A dictionary contains all the method implementations of a type class for a specific type.
Overloading
Subtyping
Dictionaries and Resolution
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)
11
eqBoolDict = ((==Bool), (/=Bool))
Overloading
Subtyping
12
Dictionaries and Resolution
Programs that rely on overloading now take dictionaries as parameters:
Becomes:
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) = (fst eq) x y ∧ same eq (y : xs)
Overloading
Subtyping
Generative Instances
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:
eqList :: EqDict a → EqDict [a]
Our set of axiom schema A now includes implications, like (Eq a) ⇒ (Eq [a]). This makes the relation A P much more complex to solve.
13
Overloading
Subtyping
14
Coherence
Some languages (such as Haskell and Rust) insist that there is only one instance per class per type in the entire program. It achieves this by requiring that all instances are either:
Defined along with the definition of the type class, or
Defined along with the definition of the type. This rules out so-called orphan instances.
There are a number of trade-offs with this decision:
Modularity has been compromised but,
Types like Data.Set can exploit this coherence to enforce invariants.
Overloading
Subtyping
15
Static Dispatch
Typically, the compiler can inline all dictionaries to their usage sites, thus eliminating all run-time cost for using type classes.
This is only not possible if the exact type being used cannot be determined at compile-time, such as with polymorphic recursion etc.
Overloading
Subtyping
Subtyping
16
Overloading
Subtyping
Subtyping
To add subtyping to a language, we define a partial order2 on types τ ≤ ρ and a rule of subsumption:
Γ⊢e:τ τ≤ρ Γ⊢e:ρ
To aid in type inference (as type inference with subtyping is undecidable in general), sometimes subsumptions (called upcasts) are made explicit (e.g. in OCaml):
Γ⊢e:τ τ≤ρ Γ ⊢ upcast ρ e : ρ
17
2Remember discrete maths, or check the glossary.
Overloading
Subtyping
18
What is Subtyping?
What this partial order τ ≤ ρ actually means is up to the language. There are two main approaches:
Most common: where upcasts do not have dynamic behaviour, i.e.
upcast v → v. This requires that any value of type τ could also be judged to have type ρ. If types are viewed as sets, this could be viewed as a subset relation.
Uncommon: where upcasts cause a coercion to occur, actually converting the value from τ to ρ at runtime.
Observation: By using an identity function as a coercion, the coercion view is more general.
Overloading
Subtyping
Desirable Properties
The coercion approach is the most general, but we might have some confusing results.
Example
Suppose Int ≤ Float, Float ≤ String and Int ≤ String. There are now two ways to coerce an Int to a String:
1 Directly: “3”
2 via Float: “3.0”
Typically, we would enforce that the subtype coercions are coherent, such that no matter which coercion is chosen, the same result is produced.
19
Overloading
Subtyping
Behavioural Subtyping
Another constraint is that the syntactic notion of subtyping should correspond to something semantically. In other words, if we know τ ≤ ρ, then it should be reasonable to replace any value of type ρ with an value of type τ without any observable difference.
Liskov Substitution Principle
Let φ(x) be a property provable about objects x of type ρ. Then φ(y) should be true for objects y of type τ where τ ≤ ρ.
Languages such as Java and C++, which allow for user-defined subtyping relationships (inheritance), put the onus on the user to ensure this condition is met.
20
Overloading
Subtyping
Product Types
Assuming a basic rule Int ≤ Float, how do we define subtyping for our compound data types?
What is the relationship between these types?
(Int × Int) (Float × Float) (Float × Int) (Int × Float)
τ1 ≤ ρ1 τ2 ≤ ρ2 (τ1 ×τ2)≤(ρ1 ×ρ2)
21
Overloading
Subtyping
Sum Types
What is the relationship between these types?
(Int + Int) (Float + Float) (Float + Int) (Int + Float)
τ1 ≤ ρ1 τ2 ≤ ρ2 (τ1 +τ2)≤(ρ1 +ρ2)
22
Any other compound types?
Overloading
Subtyping
Functions
What is the relationship between these types?
(Int → Int) (Float → Float) (Float → Int) (Int → Float)
The relation is flipped on the left hand side!
ρ1 ≤ τ1
(τ1 →τ2)≤(ρ1 →ρ2)
τ2 ≤ ρ2
23
Overloading
Subtyping
24
Variance
The way a type constructor (such as +, ×, Maybe or →) interacts with subtyping is called its variance. For a type constructor C, and τ ≤ ρ:
If C τ ≤ C ρ, then C is covariant.
Examples: Products (both arguments), Sums (both arguments), Function return type, …
If C ρ ≤ C τ, then C is contravariant. Examples: Function argument type, . . .
If it is neither covariant nor contravariant then it is (confusingly) called invariant. Examples: data Endo a = E (a → a)
Overloading
Subtyping
Stuffing it up
Many languages have famously stuffed this up, at the expense of type safety.
A few years later…
25
Overloading
Subtyping
26
Java too
Java (and its Seattle-based cousin, C♯) also broke type safety with incorrect variance in arrays.
We will demonstrate how this violates preservation, time permitting.