Chapter 6
Overloading

6.1 | Type Classes
6.2 | Functions Defined in Terms of Overloaded Functions
6.3 | Instances of Type Classes Defined in Terms of Overloaded Functions
6.4 | Type Constructor Classes
6.5 | Overlapping Instances
6.6 | Internal Overloading
6.7 | Defining Derived Members in a Class
6.8 | A Shorthand for Defining Overloaded Functions
6.9 | Classes Defined in Terms of Other Classes
6.10 | Exporting Type Classes
6.11 | Semantic Restrictions on Type Classes

C lean allows functions and operators to be overloaded. Type classes and type constructor classes are provided (which look similar to Haskell (Hudak et al. 1992) and Gofer (Jones, 1993), although our classes have slightly different semantics) with which a restricted context can be imposed on a type variable in a type specification.

If one defines a function it should in general have a name that is different from all other function names defined within the same scope and name space (see 2.1). However, it is sometimes very convenient to overload certain functions and operators (e.g. +, -, ==), i.e. use identical names for different functions or operators that perform similar tasks albeit on objects of different types.

In principle it is possible to simulate a kind of overloading by using records. One simply defines a record (see 5.2) in which a collection of functions are stored that somehow belong to each other. Now the field name of the record can be used as (overloaded) synonym for any concrete function stored on the corresponding position. The record can be regarded as a kind of dictionary in which the concrete function can be looked up.

Example of the use of a dictionary record to simulate overloading. sumlist can use the field name add as synonym for any concrete function obeying the type as specified in the record definition. The operators +., +^, -. and -^ are assumed to be predefined primitives operators for addition and subtraction on the basic types Real and Int.

::Arith a = { add :: a a -> a

, subtract :: a a -> a

}

ArithReal = { add = (+.), subtract = (-.) }

ArithInt = { add = (+^), subtract = (-^) }

sumlist:: (Arith a) [a] [a] -> [a]

sumlist arith [x:xs] [y:ys] = [arith.add x y:sumlist arith xs ys]

sumlist arith x y = []

Start = sumlist ArithInt [1..10] [11..20]

A disadvantage of such a dictionary record is that it is syntactically not so nice (e.g. one explicitly has to pass the record to the appropriate function) and that one has to pay a huge price for efficiency (due to the use of higher order functions) as well. C lean’s overloading system as introduced below enables the C lean system to automatically create and add dictionaries as argument to the appropriate function definitions and function applications. To avoid efficiency loss the C lean compiler will substitute the intended concrete function for the overloaded function application where possible. In worst case however C lean’s overloading system will indeed have to generate a dictionary record that is then automatically passed as additional parameter to the appropriate function.

## 6.1 Type Classes

In a type class definition one gives a name to a set of overloaded functions (this is similar to the definition of a type of the dictionary record as explained above). For each overloaded function or operator which is a member of the class the overloaded name and its overloaded type is specified. The type class variables are used to indicate how the different instantiations of the class vary from each other. C lean 2.0 offers multi-parameter type constructor classes, similar to those available in Haskell.

TypeClassDef | = | class ClassName TypeVariable+ [ClassContext]
|  | [[where] { {ClassMemberDef}+ }]
| | | class FunctionName TypeVariable+ :: FunctionType;
| | | class (FunctionName) [Fix][Prec] TypeVariable+ :: FunctionType;

ClassMemberDef | = | FunctionTypeDef
|  | [MacroDef]

Example of the definition of a type class; in this case the class named Arith contains two overloaded operators.

class Arith a

where

(+) infixl 6:: a a -> a

(-) infixl 6:: a a -> a

Example. Classes can have several type class variables.

class Arith2 a b c

where

(:+:) infixl 6:: a b -> c

With an instance .ib .instance; declaration an instance of a given class can be defined (this is similar to the creation of a dictionary record). When the instance is made one has to be specify for which concrete type an instance is created. For each overloaded function in the class an instance of the overloaded function or operator has to be defined. The type of the instance can be found via uniform substitution of the type class variables by the corresponding type instances specified in the instance definition.

TypeClassInstanceDef | = | instance ClassName Type+ [ClassContext]
|  | [[where] {{DefOfFunction}+ }] | // in implementation modules
|  | [special {TypeVariable = Type}+] | // in definition modules

Example of the definition of an instance of a type class Arith for type Int. The type of the concrete functions can be obtained via uniform substitution of the type class variable in the class definition by the corresponding type specified in the instance definition. One is not obliged to repeat the type of the concrete functions instantiated (nor the fixity or associativity in the case of operators).

instance Arith Int

where

(+):: Int Int -> Int

(+) x y = x +^ y

(-):: Int Int -> Int

(-) x y = x -^ y

Example of the definition of an instance of a type class Arith for type Real.

instance Arith Real

where

(+) x y = x +. y

(-) x y = x -. y

Example. Instantiation of Arith2 using the instantiations of Arith specified above.

instance Arith2 Int Int Int where (:+:) x y = x + y

instance Arith2 Int Real Real where (:+:) x y = toReal x + y

instance Arith2 Real Int Real where (:+:) x y = x + toReal y

instance Arith2 Real Real Real where (:+:) x y = x + y

One can define as many instances of a class as one likes. Instances can be added later on in any module that has imported the class one wants to instantiate.

When an instance of a class is defined a concrete definition has to be given for all the class members.

## 6.2 Functions Defined in Terms of Overloaded Functions

When an overloaded name is encountered in an expression, the compiler will determine which of the corresponding concrete functions/operators is meant by looking at the concrete type of the expression. This type is used to determine which concrete function to apply.

All instances of a type variable of a certain class have to be of a flat type (see the restrictions mentioned in 6.11).

If it is clear from the type of the expression which one of the concrete instantiations is meant the compiler will in principle substitute the concrete function for the overloaded one, such that no efficiency is lost.

Example of the substitution of a concrete function for an overloaded one. Given the definitions above the function

inc n = n + 1

will be internally transformed into

inc n = n +^ 1

However, it is very well possible that the compiler, given the type of the expression, cannot decide which one of the corresponding concrete functions to apply. The new function then becomes overloaded as well.

For instance, the function

add x y = x + y

becomes overloaded as well because it cannot be determined which concrete instances can be applied: add can be applied to arguments of any type, as long as addition (+) is defined on them.

This has as consequence that an additional restriction must be imposed on the type of such an expression. A class context has to be added to the function type to express that the function can only be applied provided that the appropriate type classes have been instantiated (in fact one specifies the type of the dictionary record which has to be passed to the function in worst case). Such a context can also be regarded as an additional restriction imposed on a type variable, introducing a kind of bounded polymorphism.

FunctionType | = | Type -> Type [ClassContext] [UnqTypeUnEqualities]
ClassContext | = | | ClassOrGenericName-list TypeVariable {& ClassName-list TypeVariable }
ClassOrGenericName | = | ClassName
| | | FunctionName TypeKind

Example of the use of a class context to impose a restriction on the instantiation of a type variable. The function add can be applied on arguments of any type under the condition that an instance of the class Arith is defined on them.

add:: a a -> a | Arith a

add x y = x + y

C lean’s type system can infer class contexts automatically. If a type class is specified as a restricted context the type system will check the correctness of the specification (as always a type specification can be more restrictive than is deduced by the compiler).

## 6.3 Instances of Type Classes Defined in Terms of Overloaded Functions

The concrete functions defined in a class instance definition can also be defined in terms of (other) overloaded functions. This is reflected in the type of the instantiated functions. Both the concrete type and the context restriction have to be specified.

Example of an instance declaration with a type which is depending on the same type class. The function + on lists can be defined in terms of the overloaded operator + on the list elements. With this definition + is defined not only on lists, but also on a list of lists etcetera.

instance Arith [a] | Arith a // on lists

where

(+) infixl 6:: [a] [a] -> [a] | Arith a

(+) [x:xs] [y:ys] = [x + y:xs + ys]

(+) _ _ = []

(-) infixl 6:: [a] [a] -> [a] | Arith a

(-) [x:xs] [y:ys] = [x - y:xs - ys]

(-) _ _ = []

Equality class.

class Eq a

where

(==) infix 2:: a a -> Bool

instance Eq [a] | Eq a // on lists

where

(==) infix 2:: [a] [a] -> Bool | Eq a

(==) [x:xs] [y:ys] = x == y && xs == ys

(==) [] [] = True

(==) _ _ = False

## 6.4 Type Constructor Classes

The C lean type system offers the possibility to use higher order types (see 3.7.1). This makes it possible to define type constructor classes (similar to constructor classes as introduced in Gofer, Jones (1993)). In that case the overloaded type variable of the type class is not of kind X, but of higher order, e.g. X -> X, X -> X -> X, etcetera. This offers the possibility to define overloaded functions that can be instantiated with type constructors of higher order (as usual, the overloaded type variable and a concrete instantiation of this type variable need to be of the same kind). This makes it possible to overload more complex functions like map and the like.

Example of a definition of a type constructor class. The class Functor including the overloaded function map which varies in type variable f of kind X -> X.

class Functor f

where

map:: (a -> b) (f a) -> (f b)

Example of an instantiation of a type constructor class. An instantiation of the well-known function map applied on lists ([] is of kind X -> X), and a map function defined on Tree’s (Tree is of kind X -> X).

instance Functor []

where

map:: (a -> b) [a] -> [b]

map f [x:xs] = [f x : map f xs]

map f [] = []

::Tree a = (/\) infixl 0 (Tree a) (Tree a)

| Leaf a

instance Functor Tree

where

map:: (a -> b) (Tree a) -> (Tree b)

map f (l/\r) = map f l /\ map f r

map f (Leaf a) = Leaf (f a)

C lean 2.0 offers the possibility to define generic functions. With generic functions one is able to define a function like map once that works for any type (see ???).

## 6.5 Overlapping Instances

Identical instances of the same class are not allowed. The compiler would not know which instance to choose. However, it is not required that all instances are of different type. It is allowed to specify an instance of a class of which the types overlap with some other instance given for that class, i.e. the types of the different class instances are different but they can be unified with each other. It is even allowed to specify an instance that works for any type, just by instantiating with a type variable instead of instantiating with a concrete type. This can be handy to define a simple default case (see also the section one generic definitions). If more than one instance is applicable, the compiler will always choose the most specific instantiation.

Example of overlapping instances. Below there are three instances given for the class Eq: one for Int eger values, one for Real values, and one for objects of any type. The latter instance is more general and overlaps with both the other instances that are more specific. If Int egers or Real s are compared, the corresponding equality function will be chosen. For all other types for which no specific instances for equality are defined, the general instance will be chosen.

class Eq a

where

(==) infix 2:: a a -> Bool

instance Eq Int // on Integers

where

(==) x y = x ==^ y

instance Eq Real // on Reals

where

(==) x y = x ==. y

instance Eq a // generic instance for Eq

where

(==) x y = False

It is sometimes unclear which of the class instances is the most specific. In that case the lexicographic order is chosen looking at the specified instances (with type variables always <= type constructors).

Example of overlapping instances. The two instances of class C overlap with each other. In the Start rule the function f is applied to two Bool ean values. In this case any of the two instances of f could be chosen. They both can be applied (one has type f::Bool a -> Bool, the other f::a Bool -> Bool, Start requires f:: Bool Bool -> Bool). The compiler will choose the first instance, because in lexicographical order instance C Bool dontcare <= instance C dontcare Bool.

class C a1 a2

where

f:: a1 a2 -> Bool

instance C Bool dontcare

where

f b x = b

instance C dontcare Bool

where

f x b = b

Start = f True False // the result will yield True

## 6.6 Internal Overloading

It is possible that a C lean expression using overloaded functions is internally ambiguously overloaded. The problem can occur when an overloaded function is used which has on overloaded type in which an overloaded type variable appears on the right-hand side of the ->. If such a function is applied in such a way that the overloaded type does not appear in the resulting type of the application, any of the available instances of the overloaded function can be used.

In that case that an overloaded function is internally ambiguously overloaded the compiler cannot determine which instance to take: a type error is given.

Counter example (ambiguous internal overloaded expression). The function body of f is internally ambiguously overloaded which results in a type error. It is not possible to determine whether its argument should be converted to an Int or to a Bool.

class Read a:: a -> String

class Write a:: String -> a

instance Read Int, Bool // export of class instance, see 6.10

instance Write Int, Bool

f:: String -> String

f x = Write (Read x) // ! This results in a type error !

One can solve such an ambiguity by splitting up the expression in parts that are typed explicitly such that it becomes clear which of the instances should be used.

f:: String -> String

f x = Write (MyRead x)

where

MyRead:: Int -> String

MyRead x = Read x

Counter example (ambiguous internal overloaded expression). The function :+: is internally ambiguously overloaded which results in a type error. The compiler is not able to infer the result type c of the multi parameter type class Arith2 a b c. The reason is that the compiler will first do the type unification and then tries to solve the overloading. In this case solving the overloading will have consequences for other overloading situations. The system can only solve one overloaded situation at a time and solving the overloading may not have any effect on other unifications.

Start :: Int

Start = 2 :+: 3 :+: 4

Example (ambiguous internal overloaded expression). By explicitly specifying types the overloading can be solved. The following program is accepted.

Start:: Int

Start = 2 :+: more

where

more:: Int

more = 3 :+: 4

## 6.7 Defining Derived Members in a Class

The members of a class consist of a set of functions or operators that logically belong to each other. It is often the case that the effect of some members (derived members) can be expressed in others. For instance, <> can be regarded as synonym for not (==). For software engineering (the fixed relation is made explicit) and efficiency (one does not need to include such derived members in the dictionary record) it is good to make this relation explicit. In C lean the existing macro facilities (see Chapter 10.3) are used for this purpose.

Classes with macro definitions to specify derived members.

class Eq a

where

(==) infix 2:: a a -> Bool

(<>) infix 2:: a a -> Bool | Eq a

(<>) x y :== not (x == y)

class Ord a

where

(<) infix 2:: a a -> Bool

(>) infix 2:: a a -> Bool | Ord a

(>) x y :== y < x

(<=) infix 2:: a a -> Bool | Ord a

(<=) x y :== not (y<x)

(>=) infix 2:: a a -> Bool | Ord a

(>=) x y :== not (x<y)

min:: a a -> a | Ord a

min x y :== if (x<y) x y

max:: a a -> a | Ord a

max x y :== if (x<y) y x

## 6.8 A Shorthand for Defining Overloaded Functions

A class definition seems sometimes a bit overdone when a class actually only consists of one member. Special syntax is provided for this case.

TypeClassDef | = | class ClassName TypeVariable [ClassContext]
|  | [[where] { {ClassMemberDef}+ }]
| | | class FunctionName TypeVariable :: FunctionType;
| | | class (FunctionName) [Fix][Prec] TypeVariable :: FunctionType;

Example of an overloaded function/operator.

class (+) infixl 6 a:: a a -> a

which is shorthand for:

class + a

where

(+) infixl 6:: a a -> a

The instantiation of such a simple one-member class is done in a similar way as with ordinary classes, using the name of the overloaded function as class name.

Example of an instantiation of an overloaded function/operator.

instance + Int

where

(+) x y = x +^ y

## 6.9 Classes Defined in Terms of Other Classes

In the definition of a class one can optionally specify that other classes that already have been defined elsewhere are included. The classes to include are specified as context after the overloaded type variable. It is not needed (but it is allowed) to define new members in the class body of the new class. In this way one can give a new name to a collection of existing classes creating a hierarchy of classes (cyclic dependencies are forbidden). Since one and the same class can be included in several other classes, one can combine classes in different kinds of meaningful ways. For an example have a closer look at the C lean standard library (see e.g. StdOverloaded and StdClass)

Example of defining classes in terms of existing classes. The class Arith consists of the class + and -.

class (+) infixl 6 a:: a a -> a

class (-) infixl 6 a:: a a -> a

class Arith a | +,- a

## 6.10 Exporting Type Classes

To export a class one simply repeats the class definition in the definition module (see Chapter 2). To export an instantiation of a class one simply repeats the instance definition in the definition module, however without revealing the concrete implementation (which can only be specified in the implementation module).

TypeClassInstanceDef | = | instance ClassName Type+ [ClassContext]
|  | [[where] {{DefOfFunction}+ }] | // only in implementation modules
|  | [special {{TypeVariable = Type}-list}+] | // only in definition modules

Exporting classes and instances.

definition module example

class Eq a // the class Eq is exported

where

(==) infix 2:: a a -> Bool

instance Eq [a] | Eq a // an instance of Eq on lists is exported

special a = Int // with an additional specialised version for [Int]

a = Real // and an additional specialised version for [real]

instance Eq a // a general instance of Eq is exported

For reasons of efficiency the compiler will always make specialized efficient versions of overloaded functions inside an implementation module. For each concrete application of an overloaded function a specialized version is made for the concrete type the overloaded function is applied to. So, when an overloaded function is used in the implementation module in which the overloaded function is defined, no overhead is introduced.

However, when an overloaded function is exported it is unknown with which concrete instances the function will be applied. So, a dictionary record is constructed in which the concrete function can be stored as is explained in the introduction of this Section. This approach can be very inefficient, especially in comparison to a specialized version. One can therefore ask the compiler to generate specialized versions of an overloaded function that is being exported. This can be done by using the keyword special. If the exported overloaded function will be used very frequently, we advise to specialize the function for the most important types it will be applied on.

A specialised function can only be generated if for all type variables which appear in the instance definition of a class a concrete type is defined.

## 6.11 Semantic Restrictions on Type Classes

Semantic restrictions:

When a class is instantiated a concrete definition must be given for each of the members in the class (not for derived members).

The type of a concrete function or operator must exactly match the overloaded type after uniform substitution of the overloaded type variable by the concrete type as specified in the corresponding type instance declaration.

The overloaded type variable and the concrete type must be of the same kind.

A type instance of an overloaded type must be a flat type, i.e. a type of the form T a1 … an where ai are type variables which are all different.

It is not allowed to use a type synonym as instance.

The start rule cannot have an overloaded type.

For the specification of derived members in a class the same restrictions hold as for defining macros.

A restricted context can only be imposed on one of the type variables appearing in the type of the expression.

The specification of the concrete functions can only be given in implementation modules.

A specialised function can only be generated if for all type variables which appear in the instance definition of a class a concrete type is defined.

A request to generate a specialised function for a class instance can only be defined in a definition module.