```kotlin
val mutable x = x_init + 1
method get = x
method set y = x <- y
end;

class ['a] oref :
'a ->
object
  constraint 'a = int
  val mutable x : int
  method get : int
  method set : int -> unit
end
```

Let us consider a more complex example: define a circle, whose center may be any kind of point. We put an additional type constraint in method `move`, since no free variables must remain unaccounted for by the class type parameters.

```kotlin
# class ['a] circle (c : 'a) =
object
  val mutable center = c
  method center = center
  method set_center c = center <- c
  method move = (center#move : int -> unit)
end;

class ['a] circle :
'a ->
object
  constraint 'a = < move : int -> unit; .. >
  val mutable center : 'a
  method center : 'a
  method move : int -> unit
  method set_center : 'a -> unit
end
```

An alternate definition of `circle`, using a `constraint` clause in the class definition, is shown below. The type `#point` used below in the `constraint` clause is an abbreviation produced by the definition of class `point`. This abbreviation unifies with the type of any object belonging to a subclass of class `point`. It actually expands to `< get_x : int; move : int -> unit; .. >`. This leads to the following alternate definition of `circle`, which has slightly stronger constraints on its argument, as we now expect `center` to have a method `get_x`.

```kotlin
# class ['a] circle (c : 'a) =
object
  constraint 'a = #point
  val mutable center = c
  method center = center
  method set_center c = center <- c
  method move = center#move
end;
```
```kotlin
class ['a] circle :
    'a ->
object
    constraint 'a = #point
    val mutable center : 'a
    method center : 'a
    method move : int -> unit
    method set_center : 'a -> unit
end
```

The class `colored_circle` is a specialized version of class `circle` that requires the type of the center to unify with `#colored_point`, and adds a method `color`. Note that when specializing a parameterized class, the instance of type parameter must always be explicitly given. It is again written between `[` and `]`.

```kotlin
# class ['a] colored_circle c =
    object
        constraint 'a = #colored_point
        inherit ['a] circle c
        method color = center#color
end;
class ['a] colored_circle :
    'a ->
object
    constraint 'a = #colored_point
    val mutable center : 'a
    method center : 'a
    method color : string
    method move : int -> unit
    method set_center : 'a -> unit
end
```

## 3.11 Polymorphic methods

While parameterized classes may be polymorphic in their contents, they are not enough to allow polymorphism of method use.

A classical example is defining an iterator.

```kotlin
# List.fold_left;
- : ('acc -> 'a -> 'acc) -> 'acc -> 'a list -> 'acc = <fun>

# class ['a] intlist (l : int list) =
    object
        method empty = (l = [])
        method fold f (accu : 'a) = List.fold_left f accu l
end;
class ['a] intlist :
    int list ->
object method empty : bool method fold : ('a -> int -> 'a) -> 'a -> 'a end
```
```ocaml
class ['a] circle :
  'a ->
object
  constraint 'a = #point
  val mutable center : 'a
  method center : 'a
  method move : int -> unit
  method set_center : 'a -> unit
end
```

The class `colored_circle` is a specialized version of class `circle` that requires the type of the center to unify with `#colored_point`, and adds a method `color`. Note that when specializing a parameterized class, the instance of type parameter must always be explicitly given. It is again written between `[` and `]`.

```ocaml
# class ['a] colored_circle c =
object
  constraint 'a = #colored_point
  inherit ['a] circle c
  method color = center#color
end;;

class ['a] colored_circle :
  'a ->
object
  constraint 'a = #colored_point
  val mutable center : 'a
  method center : 'a
  method color : string
  method move : int -> unit
  method set_center : 'a -> unit
end
```

## 3.11 Polymorphic methods

While parameterized classes may be polymorphic in their contents, they are not enough to allow polymorphism of method use.

A classical example is defining an iterator.

```ocaml
# List.fold_left;;
- : ('acc -> 'a -> 'acc) -> 'acc -> 'a list -> 'acc = <fun>

# class ['a] intlist (l : int list) =
object
  method empty = (l = [])
  method fold f (accu : 'a) = List.fold_left f accu l
end;;

class ['a] intlist :
  int list ->
object method empty : bool method fold : ('a -> int -> 'a) -> 'a -> 'a end
```
At first look, we seem to have a polymorphic iterator, however this does not work in practice.

```ocaml
# let l = new intlist [1; 2; 3];;
```

```ocaml
val l : '_weak2 intlist = <obj>
```

```ocaml
# l#fold (fun x y -> x+y) 0;;
```

```ocaml
- : int = 6
```

```ocaml
# l;;
```

```ocaml
- : int intlist = <obj>
```

```ocaml
# l#fold (fun s x -> s ^ Int.to_string x ^ " ") "";;
```

```
Error: This expression has type int but an expression was expected of type
        string
```

Our iterator works, as shows its first use for summation. However, since objects themselves are not polymorphic (only their constructors are), using the `fold` method fixes its type for this individual object. Our next attempt to use it as a string iterator fails.

The problem here is that quantification was wrongly located: it is not the class we want to be polymorphic, but the `fold` method. This can be achieved by giving an explicitly polymorphic type in the method definition.

```ocaml
# class intlist (l : int list) =
```

object

method empty = (l = [])

method fold : 'a. ('a -> int -> 'a) -> 'a -> 'a =
fun f accu -> List.fold_left f accu l

end;;

class intlist :

int list ->

object method empty : bool method fold : ('a -> int -> 'a) -> 'a -> 'a end

```ocaml
# let l = new intlist [1; 2; 3];;
```

```ocaml
val l : intlist = <obj>
```

```ocaml
# l#fold (fun x y -> x+y) 0;;
```

```ocaml
- : int = 6
```

```ocaml
# l#fold (fun s x -> s ^ Int.to_string x ^ " ") "";;
```

```ocaml
- : string = "1 2 3"
```

As you can see in the class type shown by the compiler, while polymorphic method types must be fully explicit in class definitions (appearing immediately after the method name), quantified type variables can be left implicit in class descriptions. Why require types to be explicit? The problem is that `(int -> int -> int) -> int -> int` would also be a valid type for `fold`, and it happens to be incompatible with the polymorphic type we gave (automatic instantiation only works for toplevel types variables, not for inner quantifiers, where it becomes an undecidable problem.) So the compiler cannot choose between those two types, and must be helped.

However, the type can be completely omitted in the class definition if it is already known, through inheritance or type constraints on self. Here is an example of method overriding.
At first look, we seem to have a polymorphic iterator, however this does not work in practice.

```h
# let l = new intlist [1; 2; 3];;
val l : '_weak2 intlist = <obj>

# l#fold (fun x y -> x+y) 0;;
- : int = 6

# l;;
- : int intlist = <obj>

# l#fold (fun s x -> s ^ Int.to_string x ^ " ") "";;
```

Error: The value s has type int but an expression was expected of type string

Our iterator works, as shows its first use for summation. However, since objects themselves are not polymorphic (only their constructors are), using the `fold` method fixes its type for this individual object. Our next attempt to use it as a string iterator fails.

The problem here is that quantification was wrongly located: it is not the class we want to be polymorphic, but the `fold` method. This can be achieved by giving an explicitly polymorphic type in the method definition.

```h
# class intlist (l : int list) =
object
  method empty = (l = [])
  method fold : 'a. ('a -> int -> 'a) -> 'a -> 'a =
    fun f accu -> List.fold_left f accu l
end;;

class intlist :
  int list ->
  object method empty : bool method fold : ('a -> int -> 'a) -> 'a -> 'a end

# let l = new intlist [1; 2; 3];;
val l : intlist = <obj>

# l#fold (fun x y -> x+y) 0;;
- : int = 6

# l#fold (fun s x -> s ^ Int.to_string x ^ " ") "";;
- : string = "1 2 3"
```

As you can see in the class type shown by the compiler, while polymorphic method types must be fully explicit in class definitions (appearing immediately after the method name), quantified type variables can be left implicit in class descriptions. Why require types to be explicit? The problem is that `(int -> int -> int) -> int -> int` would also be a valid type for `fold`, and it happens to be incompatible with the polymorphic type we gave (automatic instantiation only works for toplevel types variables, not for inner quantifiers, where it becomes an undecidable problem.) So the compiler cannot choose between those two types, and must be helped.

However, the type can be completely omitted in the class definition if it is already known, through inheritance or type constraints on self. Here is an example of method overriding.
```python
# class intlist_rev 1 =
    object
        inherit intlist 1
        method! fold f accu = List.fold_left f accu (List.rev 1)
    end;;
```

The following idiom separates description and definition.

```python
# class type ['a] iterator =
    object method fold : ('b -> 'a -> 'b) -> 'b -> 'b end;;
```

```python
# class intlist' 1 =
    object (self : int #iterator)
        method empty = (1 = [])
        method fold f accu = List.fold_left f accu 1
    end;;
```

Note here the `(self : int #iterator)` idiom, which ensures that this object implements the interface `iterator`.

Polymorphic methods are called in exactly the same way as normal methods, but you should be aware of some limitations of type inference. Namely, a polymorphic method can only be called if its type is known at the call site. Otherwise, the method will be assumed to be monomorphic, and given an incompatible type.

```python
# let sum lst = lst#fold (fun x y -> x+y) 0;;
val sum : < fold : (int -> int -> int) -> int -> 'a; .. > -> 'a = <fun>
```

```python
# sum _ 1 ;;
```

```
Error: This expression has type intlist
but an expression was expected of type
  < fold : (int -> int -> int) -> int -> 'a; .. >
Types for method fold are incompatible
```

The workaround is easy: you should put a type constraint on the parameter.

```python
# let sum (lst : _ #iterator) = lst#fold (fun x y -> x+y) 0;;
val sum : int #iterator -> int = <fun>
```

Of course the constraint may also be an explicit method type. Only occurrences of quantified variables are required.

```python
# let sum lst =
    (lst : < fold : 'a. ('a -> _ -> 'a) -> 'a -> 'a; .. >)#fold (+) 0;;
val sum : < fold : 'a. ('a -> int -> 'a) -> 'a -> 'a; .. > -> int = <fun>
```

Another use of polymorphic methods is to allow some form of implicit subtyping in method arguments. We have already seen in section 3.8 how some functions may be polymorphic in the class of their argument. This can be extended to methods.

```python
# class type point0 = object method get_x : int end;;
    class type point0 = object method get_x : int end
```
``` OCaml
# class intlist_rev 1 =
    object
        inherit intlist 1
        method! fold f accu = List.fold_left f accu (List.rev 1)
    end;;
```

The following idiom separates description and definition.

``` OCaml
# class type ['a] iterator =
    object method fold : ('b -> 'a -> 'b) -> 'b -> 'b end;;
```

``` OCaml
# class intlist' 1 =
    object (self : int #iterator)
        method empty = (1 = [])
        method fold f accu = List.fold_left f accu 1
    end;;
```

Note here the `(self : int #iterator)` idiom, which ensures that this object implements the interface `iterator`.

Polymorphic methods are called in exactly the same way as normal methods, but you should be aware of some limitations of type inference. Namely, a polymorphic method can only be called if its type is known at the call site. Otherwise, the method will be assumed to be monomorphic, and given an incompatible type.

``` OCaml
# let sum lst = lst#fold (fun x y -> x+y) 0;;
val sum : < fold : (int -> int -> int) -> int -> 'a; .. > -> 'a = <fun>
```

``` OCaml
# sum _ 1;;
```

```
Error: The value 1 has type
       intlist = < empty : bool; fold : 'a. ('a -> int -> 'a) -> 'a -> 'a >
       but an expression was expected of type
       < fold : (int -> int -> int) -> int -> 'b; .. >
       The method fold has type 'a. ('a -> int -> 'a) -> 'a -> 'a,
       but the expected method type was (int -> int -> int) -> int -> 'b
```

The workaround is easy: you should put a type constraint on the parameter.

``` OCaml
# let sum (lst : _ #iterator) = lst#fold (fun x y -> x+y) 0;;
val sum : int #iterator -> int = <fun>
```

Of course the constraint may also be an explicit method type. Only occurrences of quantified variables are required.

``` OCaml
# let sum lst =
    (lst : < fold : 'a. ('a -> _ -> 'a) -> 'a -> 'a; .. >)#fold (+) 0;;
val sum : < fold : 'a. ('a -> int -> 'a) -> 'a -> 'a; .. > -> int = <fun>
```

Another use of polymorphic methods is to allow some form of implicit subtyping in method arguments. We have already seen in section 3.8 how some functions may be polymorphic in the class of their argument. This can be extended to methods.

``` OCaml
# class type point0 = object method get_x : int end;;

class type point0 = object method get_x : int end
```
```ocaml
# class distance_point x =
    object
        inherit point x
        method distance : 'a. (#point0 as 'a) -> int =
            fun other -> abs (other#get_x - x)
    end;

class distance_point :
    int ->
    object
        val mutable x : int
        method distance : #point0 -> int
        method get_offset : int
        method get_x : int
        method move : int -> unit
    end

# let p = new distance_point 3 in
    (p#distance (new point 8), p#distance (new colored_point 1 "blue"));
- : int * int = (5, 2)
```

Note here the special syntax (`#point0` as `'a'`) we have to use to quantify the extensible part of `#point0`. As for the variable binder, it can be omitted in class specifications. If you want polymorphism inside object field it must be quantified independently.

```ocaml
# class multidra =
    object
        method m1 : 'a. (< n1 : 'b. 'b -> 'b; .. > as 'a) -> _ =
            fun o -> o#n1 true, o#n1 "hello"
        method m2 : 'a 'b. (< n2 : 'b -> bool; .. > as 'a) -> 'b -> _ =
            fun o x -> o#n2 x
    end;
```

```python
class multidra :
    object
        method m1 : < n1 : 'b. 'b -> 'b; .. > -> bool * string
        method m2 : < n2 : 'b -> bool; .. > -> 'b -> bool
    end
```

In method `m1`, `o` must be an object with at least a method `n1`, itself polymorphic. In method `m2`, the argument of `n2` and `x` must have the same type, which is quantified at the same level as `'a`.

## 3.12 Using coercions

Subtyping is never implicit. There are, however, two ways to perform subtyping. The most general construction is fully explicit: both the domain and the codomain of the type coercion must be given.

We have seen that points and colored points have incompatible types. For instance, they cannot be mixed in the same list. However, a colored point can be coerced to a point, hiding its `color` method:

```ocaml
# let colored_point_to_point cp = (cp : colored_point -> point);
```
```kotlin
# class distance_point x =
    object
        inherit point x
        method distance: 'a. (#point0 as 'a) -> int =
            fun other -> abs (other#get_x - x)
        end;

class distance_point : 
    int ->
    object
        val mutable x: int
        method distance: #point0 -> int
        method get_offset: int
        method get_x: int
        method move: int -> unit
end

# let p = new distance_point 3 in
    (p#distance (new point 8), p#distance (new colored_point 1 "blue"));
    - : int * int = (5, 2)
```

Note here the special syntax (`#point0` as `'a'`) we have to use to quantify the extensible part of `#point0`. As for the variable binder, it can be omitted in class specifications. If you want polymorphism inside object field it must be quantified independently.

```kotlin
# class multidra =
    object
        method m1: 'a. (< n1: 'b. 'b -> 'b; .. > as 'a) -> _ =
            fun o -> o#n1 true, o#n1 "hello"
        method m2: 'a 'b. (< n2: 'b -> bool; .. > as 'a) -> 'b -> _ =
            fun o x -> o#n2 x
        end;
```

```kotlin
class multidra :
    object
        method m1: < n1: 'b. 'b -> 'b; .. > -> bool * string
        method m2: < n2: 'b -> bool; .. > -> 'b -> bool
end
```

In method `m1`, `o` must be an object with at least a method `n1`, itself polymorphic. In method `m2`, the argument of `n2` and `x` must have the same type, which is quantified at the same level as `'a`.

## 3.12 Using coercions

Subtyping is never implicit. There are, however, two ways to perform subtyping. The most general construction is fully explicit: both the domain and the codomain of the type coercion must be given.

We have seen that `points` and `colored points` have incompatible types. For instance, they cannot be mixed in the same list. However, a `colored point` can be coerced to a `point`, hiding its `color` method:

```kotlin
# let colored_point_to_point cp = (cp : colored_point :> point);
```
```h
val colored_point_to_point : colored_point -> point = <fun>
```

```h
# let p = new point 3 and q = new colored_point 4 "blue";;
val p : point = <obj>
val q : colored_point = <obj>
```

```h
# let l = [p; (colored_point_to_point q)];;
val l : point list = [<obj>; <obj>]
```

An object of type `t` can be seen as an object of type `t'` only if `t` is a subtype of `t'`. For instance, a point cannot be seen as a colored point.

```h
# (p : point :> colored_point);;
```

```
Error: Type point = < get_offset : int; get_x : int; move : int -> unit >
       is not a subtype of
       colored_point =
           < color : string; get_offset : int; get_x : int;
           move : int -> unit >
       The first object type has no method color
```

Indeed, narrowing coercions without runtime checks would be unsafe. Runtime type checks might raise exceptions, and they would require the presence of type information at runtime, which is not the case in the OCaml system. For these reasons, there is no such operation available in the language.

Be aware that subtyping and inheritance are not related. Inheritance is a syntactic relation between classes while subtyping is a semantic relation between types. For instance, the class of colored points could have been defined directly, without inheriting from the class of points; the type of colored points would remain unchanged and thus still be a subtype of points.

The domain of a coercion can often be omitted. For instance, one can define:

```h
# let to_point cp = (cp :> point);;
val to_point : #point -> point = <fun>
```

In this case, the function `colored_point_to_point` is an instance of the function `to_point`. This is not always true, however. The fully explicit coercion is more precise and is sometimes unavoidable. Consider, for example, the following class:

```h
# class c0 = object method m = {< >} method n = 0 end;;
class c0 : object ('a) method m : 'a method n : int end
```

The object type `c0` is an abbreviation for `<m : 'a; n : int> as 'a`. Consider now the type declaration:

```h
# class type c1 = object method m : c1 end;;
class type c1 = object method m : c1 end
```

The object type `c1` is an abbreviation for the type `<m : 'a> as 'a`. The coercion from an object of type `c0` to an object of type `c1` is correct:

```h
# fun (x:c0) -> (x : c0 :> c1);;
- : c0 -> c1 = <fun>
```
``` OCaml
val colored_point_to_point : colored_point -> point = <fun>
```

``` OCaml
# let p = new point 3 and q = new colored_point 4 "blue";;
val p : point = <obj>
val q : colored_point = <obj>
```

``` OCaml
# let l = [p; (colored_point_to_point q)];;
val l : point list = [<obj>; <obj>]
```

An object of type `t` can be seen as an object of type `t'` only if `t` is a subtype of `t'`. For instance, a point cannot be seen as a colored point.

``` OCaml
# (p : point -> colored_point);;
```

``` OCaml
Error: Type point = < get_offset : int; get_x : int; move : int -> unit >
is not a subtype of
  colored_point =
    < color : string; get_offset : int; get_x : int;
      move : int -> unit >
The first object type has no method color
```

Indeed, narrowing coercions without runtime checks would be unsafe. Runtime type checks might raise exceptions, and they would require the presence of type information at runtime, which is not the case in the OCaml system. For these reasons, there is no such operation available in the language.

Be aware that subtyping and inheritance are not related. Inheritance is a syntactic relation between classes while subtyping is a semantic relation between types. For instance, the class of colored points could have been defined directly, without inheriting from the class of points; the type of colored points would remain unchanged and thus still be a subtype of points.

The domain of a coercion can often be omitted. For instance, one can define:

``` OCaml
# let to_point cp = (cp :> point);;
val to_point : #point -> point = <fun>
```

In this case, the function `colored_point_to_point` is an instance of the function `to_point`. This is not always true, however. The fully explicit coercion is more precise and is sometimes unavoidable. Consider, for example, the following class:

``` OCaml
# class c0 = object method m = {< >} method n = 0 end;;
class c0 : object ('a) method m : 'a method n : int end
```

The object type `c0` is an abbreviation for `<m : 'a; n : int> as 'a`. Consider now the type declaration:

``` OCaml
# class type c1 = object method m : c1 end;;
class type c1 = object method m : c1 end
```

The object type `c1` is an abbreviation for the type `<m : 'a> as 'a`. The coercion from an object of type `c0` to an object of type `c1` is correct:

``` OCaml
# fun (x:c0) -> (x : c0 :> c1);;
- : c0 -> c1 = <fun>
```
However, the domain of the coercion cannot always be omitted. In that case, the solution is to use
the explicit form. Sometimes, a change in the class-type definition can also solve the problem

``` OCaml
# class type c2 = object ('a) method m : 'a end;;
class type c2 = object ('a) method m : 'a end
```

``` OCaml
# fun (x:c0) -> (x :> c2);;
- : c0 -> c2 = <fun>
```

While class types `c1` and `c2` are different, both object types `c1` and `c2` expand to the same object type (same method names and types). Yet, when the domain of a coercion is left implicit and its co-domain is an abbreviation of a known class type, then the class type, rather than the object type, is used to derive the coercion function. This allows leaving the domain implicit in most cases when coercing from a subclass to its superclass. The type of a coercion can always be seen as below:

``` OCaml
# let to_c1 x = (x :> c1);;
val to_c1 : <m : #c1; .. > -> c1 = <fun>
```

``` OCaml
# let to_c2 x = (x :> c2);;
val to_c2 : #c2 -> c2 = <fun>
```

Note the difference between these two coercions: in the case of `to_c2`, the type `#c2 = <m : 'a; .. > as 'a` is polymorphically recursive (according to the explicit recursion in the class type of `c2`); hence the success of applying this coercion to an object of class `c0`. On the other hand, in the first case, `c1` was only expanded and unrolled twice to obtain `<m : <m : c1; .. >; .. >` (remember `#c1 = <m : c1; .. >`), without introducing recursion. You may also note that the type of `to_c2` is `#c2 -> c2` while the type of `to_c1` is more general than `#c1 -> c1`. This is not always true, since there are class types for which some instances of `#c` are not subtypes of `c`, as explained in section 3.16. Yet, for parameterless classes the coercion (`_ :> c`) is always more general than (`_ : #c :> c`).

A common problem may occur when one tries to define a coercion to a class `c` while defining class `c`. The problem is due to the type abbreviation not being completely defined yet, and so its subtypes are not clearly known. Then, a coercion (`_ :> c`) or (`_ : #c :> c`) is taken to be the identity function, as in

``` OCaml
# fun x -> (x :> 'a);;
- : 'a -> 'a = <fun>
```

As a consequence, if the coercion is applied to `self`, as in the following example, the type of `self` is unified with the closed type `c` (a closed object type is an object type without ellipsis). This would constrain the type of `self` be closed and is thus rejected. Indeed, the type of `self` cannot be closed: this would prevent any further extension of the class. Therefore, a type error is generated when the unification of this type with another type would result in a closed object type.

``` OCaml
# class c = object method m = 1 end
and d = object (self)
    inherit c
    method n = 2
    method as_c = (self :> c)
end;;
```
However, the domain of the coercion cannot always be omitted. In that case, the solution is to use
the explicit form. Sometimes, a change in the class-type definition can also solve the problem

```h
# class type c2 = object ('a') method m : 'a end;;
class type c2 = object ('a') method m : 'a end
```

```h
# fun (x:c0) -> (x :> c2);;
- : c0 -> c2 = <fun>
```

While class types `c1` and `c2` are different, both object types `c1` and `c2` expand to the same object type (same method names and types). Yet, when the domain of a coercion is left implicit and its co-domain is an abbreviation of a known class type, then the class type, rather than the object type, is used to derive the coercion function. This allows leaving the domain implicit in most cases when coercing from a subclass to its superclass. The type of a coercion can always be seen as below:

```h
# let to_c1 x = (x :> c1);;
val to_c1 : < m : #c1; .. > -> c1 = <fun>
```

```h
# let to_c2 x = (x :> c2);;
val to_c2 : #c2 -> c2 = <fun>
```

Note the difference between these two coercions: in the case of `to_c2`, the type `#c2 = < m : 'a; .. > as 'a` is polymorphically recursive (according to the explicit recursion in the class type of `c2`); hence the success of applying this coercion to an object of class `c0`. On the other hand, in the first case, `c1` was only expanded and unrolled twice to obtain `< m : < m : c1; .. >; .. >` (remember `#c1 = < m : c1; .. >`), without introducing recursion. You may also note that the type of `to_c2` is `#c2 -> c2` while the type of `to_c1` is more general than `#c1 -> c1`. This is not always true, since there are class types for which some instances of `#c` are not subtypes of `c`, as explained in section 3.16. Yet, for parameterless classes the coercion (`_ :> c`) is always more general than (`_ : #c :> c`).

A common problem may occur when one tries to define a coercion to a class `c` while defining class `c`. The problem is due to the type abbreviation not being completely defined yet, and so its subtypes are not clearly known. Then, a coercion (`_ :> c`) or (`_ : #c :> c`) is taken to be the identity function, as in

```h
# fun x -> (x :> 'a);;
- : 'a -> 'a = <fun>
```

As a consequence, if the coercion is applied to `self`, as in the following example, the type of `self` is unified with the closed type `c` (a closed object type is an object type without ellipsis). This would constrain the type of `self` be closed and is thus rejected. Indeed, the type of `self` cannot be closed: this would prevent any further extension of the class. Therefore, a type error is generated when the unification of this type with another type would result in a closed object type.

```python
# class c = object method m = 1 end
and d = object (self)
    inherit c
    method n = 2
    method as_c = (self :> c)
end;;
```
```
Error: This expression cannot be coerced to type c = < m : int >; it has type
      < as_c : c; m : int; n : int; .. >
but is here used with type c
Self type cannot escape its class
```

However, the most common instance of this problem, coercing self to its current class, is detected as a special case by the type checker, and properly typed.

```python
# class c = object(self) method m = (self :> c) end;;
class c : object method m : c end
```

This allows the following idiom, keeping a list of all objects belonging to a class or its subclasses:

```python
# let all_c = ref [];;
val all_c : '_weak3 list ref = {contents = []}'

# class c (m : int) =
    object (self)
    method m = m
    initializer all_c := (self :> c) :: !all_c
end;;
class c : int -> object method m : int end
```

This idiom can in turn be used to retrieve an object whose type has been weakened:

```python
# let rec lookup_obj obj = function [] -> raise Not_found
| obj' :: l ->
    if (obj :> <>) = (obj' :> <>) then obj' else lookup_obj obj l ;;
val lookup_obj : < .. > -> (< .. > as 'a) list -> 'a = <fun>

# let lookup_c obj = lookup_obj obj !all_c;;
val lookup_c : < .. > -> < m : int > = <fun>
```

The type `< m : int >` we see here is just the expansion of `c`, due to the use of a reference; we have succeeded in getting back an object of type `c`.

The previous coercion problem can often be avoided by first defining the abbreviation, using a class type:

```python
# class type c' = object method m : int end;;
class type c' = object method m : int end

# class c : c' = object method m = 1 end
    and d = object (self)
    inherit c
    method n = 2
    method as_c = (self :> c')
end;;
class c : c'
    and d : object method as_c : c' method m : int method n : int end
```

It is also possible to use a virtual class. Inheriting from this class simultaneously forces all methods of `c` to have the same type as the methods of `c'`.
```
Error: This expression cannot be coerced to type c = < m : int >; it has type
       < as_c : c; m : int; n : int; .. >
but is here used with type c
Self type cannot escape its class
```

However, the most common instance of this problem, coercing self to its current class, is detected as a special case by the type checker, and properly typed.

```ocaml
# class c = object (self) method m = (self :> c) end;;
class c : object method m : c end
```

This allows the following idiom, keeping a list of all objects belonging to a class or its subclasses:

```ocaml
# let all_c = ref [];
val all_c : '_weak3 list ref = {contents = []}

# class c (m : int) =
    object (self)
        method m = m
        initializer all_c := (self :> c) :: !all_c
    end;;

class c : int -> object method m : int end
```

This idiom can in turn be used to retrieve an object whose type has been weakened:

```ocaml
# let rec lookup_obj obj = function [] -> raise Not_found
  | obj' :: l ->
    if (obj :> <>) = (obj' :> <>) then obj' else lookup_obj obj l ;;
val lookup_obj : < .. > -> (< .. > as 'a) list -> 'a = <fun>

# let lookup_c obj = lookup_obj obj !all_c;;
val lookup_c : < .. > -> < m : int > = <fun>
```

The type `< m : int >` we see here is just the expansion of `c`, due to the use of a reference; we have succeeded in getting back an object of type `c`.

The previous coercion problem can often be avoided by first defining the abbreviation, using a class type:

```ocaml
# class type c' = object method m : int end;;
class type c' = object method m : int end

# class c : c' = object method m = 1 end
and d = object (self)
    inherit c
    method n = 2
    method as_c = (self :> c')
end;;

class c : c'
and d : object method as_c : c' method m : int method n : int end
```

It is also possible to use a virtual class. Inheriting from this class simultaneously forces all methods of `c` to have the same type as the methods of `c'`.
```ocaml
# class virtual c' = object method virtual m : int end;;
```

```ocaml
class virtual c' : object method virtual m : int end
```

```ocaml
# class c = object (self) inherit c' method m = 1 end;;
```

```ocaml
class c : object method m : int end
```

One could think of defining the type abbreviation directly:

```ocaml
# type c' = <m : int>;;
```

However, the abbreviation `#c'` cannot be defined directly in a similar way. It can only be defined by a class or a class-type definition. This is because a `#-abbreviation` carries an implicit anonymous variable `..` that cannot be explicitly named. The closer you get to it is:

```ocaml
# type 'a c'_class = 'a constraint 'a = < m : int; .. >;;
```

with an extra type variable capturing the open object type.

## 3.13 Functional objects

It is possible to write a version of class `point` without assignments on the instance variables. The override construct `{{< ... >}}` returns a copy of "self" (that is, the current object), possibly changing the value of some instance variables.

```ocaml
# class functional_point y =
    object
        val x = y
        method get_x = x
        method move d = {{< x = x + d >}}
        method move_to x = {{< x >}}
    end;;
```

```ocaml
class functional_point :
    int ->
    object ('a)
        val x : int
        method get_x : int
        method move : int -> 'a
        method move_to : int -> 'a
    end
```

```ocaml
# let p = new functional_point 7;;
```

```ocaml
val p : functional_point = <obj>
```

```ocaml
# p#get_x;;
```

```ocaml
- : int = 7
```

```ocaml
# (p#move 3)#get_x;;
```

```ocaml
- : int = 10
```

```ocaml
# (p#move_to 15)#get_x;;
```

```ocaml
- : int = 15
```
```python
# class virtual c' = object method virtual m : int end;;
class virtual c' : object method virtual m : int end
```

```python
# class c = object (self) inherit c' method m = 1 end;;
class c : object method m : int end
```

One could think of defining the type abbreviation directly:

```python
# type c' = <m : int>;;
```

However, the abbreviation `#c'` cannot be defined directly in a similar way. It can only be defined by a class or a class-type definition. This is because a `#-abbreviation` carries an implicit anonymous variable `..` that cannot be explicitly named. The closer you get to it is:

```python
# type 'a c'_class = 'a constraint 'a = < m : int; .. >;;
with an extra type variable capturing the open object type.
```

## 3.13 Functional objects

It is possible to write a version of class `point` without assignments on the instance variables. The override construct `{{< ... >}}` returns a copy of `self` (that is, the current object), possibly changing the value of some instance variables.

```python
# class functional_point y =
object
    val x = y
    method get_x = x
    method move d = {{< x = x + d >}}
    method move_to x = {{< x >}}
end;;
class functional_point :
    int ->
    object ('a)
        val x : int
        method get_x : int
        method move : int -> 'a
        method move_to : int -> 'a
end
```

```python
# let p = new functional_point 7;;
val p : functional_point = <obj>
```

```python
# p#get_x;;
- : int = 7
```

```python
# (p#move 3)#get_x;;
- : int = 10
```

```python
# (p#move_to 15)#get_x;;
- : int = 15
```
```perl
# p#get_x;;
- : int = 7
```

As with records, the form `{< x >}` is an elided version of `{< x = x >}` which avoids the repetition of the instance variable name. Note that the type abbreviation `functional_point` is recursive, which can be seen in the class type of `functional_point`: the type of self is `'a'` and `'a'` appears inside the type of the method `move`.

The above definition of `functional_point` is not equivalent to the following:

```perl
# class bad_functional_point y =
object
    val x = y
    method get_x = x
    method move d = new bad_functional_point (x+d)
    method move_to x = new bad_functional_point x
end;;

class bad_functional_point :
    int ->
    object
        val x : int
        method get_x : int
        method move : int -> bad_functional_point
        method move_to : int -> bad_functional_point
end
```

While objects of either class will behave the same, objects of their subclasses will be different. In a subclass of `bad_functional_point`, the method `move` will keep returning an object of the parent class. On the contrary, in a subclass of `functional_point`, the method `move` will return an object of the subclass.

Functional update is often used in conjunction with binary methods as illustrated in section 8.2.1.

## 3.14 Cloning objects

Objects can also be cloned, whether they are functional or imperative. The library function `Oo.copy` makes a shallow copy of an object. That is, it returns a new object that has the same methods and instance variables as its argument. The instance variables are copied but their contents are shared. Assigning a new value to an instance variable of the copy (using a method call) will not affect instance variables of the original, and conversely. A deeper assignment (for example if the instance variable is a reference cell) will of course affect both the original and the copy.

The type of `Oo.copy` is the following:

```perl
# Oo.copy;;
- : (< .. > as 'a) -> 'a = <fun>
```

The keyword `as` in that type binds the type variable `'a` to the object type `< .. >`. Therefore, `Oo.copy` takes an object with any methods (represented by the ellipsis), and returns an object of the same type. The type of `Oo.copy` is different from type `< .. > -> < .. >` as each ellipsis represents a different set of methods. Ellipsis actually behaves as a type variable.
``` OCaml
# p#get_x;;
- : int = 7
```

As with records, the form `{< x >}` is an elided version of `{< x = x >}` which avoids the repetition of the instance variable name. Note that the type abbreviation `functional_point` is recursive, which can be seen in the class type of `functional_point`: the type of self is `'a` and `'a` appears inside the type of the method `move`.

The above definition of `functional_point` is not equivalent to the following:

``` OCaml
# class bad_functional_point y =
    object
        val x = y
        method get_x = x
        method move d = new bad_functional_point (x+d)
        method move_to x = new bad_functional_point x
    end;;

class bad_functional_point :
    int ->
    object
        val x : int
        method get_x : int
        method move : int -> bad_functional_point
        method move_to : int -> bad_functional_point
    end
```

While objects of either class will behave the same, objects of their subclasses will be different. In a subclass of `bad_functional_point`, the method `move` will keep returning an object of the parent class. On the contrary, in a subclass of `functional_point`, the method `move` will return an object of the subclass.

Functional update is often used in conjunction with binary methods as illustrated in section 8.2.1.

## 3.14 Cloning objects

Objects can also be cloned, whether they are functional or imperative. The library function `Oo.copy` makes a shallow copy of an object. That is, it returns a new object that has the same methods and instance variables as its argument. The instance variables are copied but their contents are shared. Assigning a new value to an instance variable of the copy (using a method call) will not affect instance variables of the original, and conversely. A deeper assignment (for example if the instance variable is a reference cell) will of course affect both the original and the copy.

The type of `Oo.copy` is the following:

``` OCaml
# Oo.copy;;
- : (< .. > as 'a) -> 'a = <fun>
```

The keyword `as` in that type binds the type variable `'a` to the object type `< .. >`. Therefore, `Oo.copy` takes an object with any methods (represented by the ellipsis), and returns an object of the same type. The type of `Oo.copy` is different from type `< .. > -> < .. >` as each ellipsis represents a different set of methods. Ellipsis actually behaves as a type variable.
```ocaml
# let p = new point 5;;
val p : point = <obj>

# let q = Oo.copy p;;
val q : point = <obj>

# q#move 7; (p#get_x, q#get_x);;
- : int * int = (5, 12)
```

In fact, `Oo.copy p` will behave as `p#copy` assuming that a public method `copy` with body `{< >}` has been defined in the class of p.

Objects can be compared using the generic comparison functions `=` and `<>`. Two objects are equal if and only if they are physically equal. In particular, an object and its copy are not equal.

```ocaml
# let q = Oo.copy p;;
val q : point = <obj>

# p = q, p = p;;
- : bool * bool = (false, true)
```

Other generic comparisons such as `<`, `<=`, ...) can also be used on objects. The relation `<` defines an unspecified but strict ordering on objects. The ordering relationship between two objects is fixed permanently once the two objects have been created, and it is not affected by mutation of fields.

Cloning and override have a non empty intersection. They are interchangeable when used within an object and without overriding any field:

```ocaml
# class copy =
  object
    method copy = {< >}
  end;;

class copy : object ('a') method copy : 'a end
```

```ocaml
# class copy =
  object (self)
    method copy = Oo.copy self
  end;;

class copy : object ('a') method copy : 'a end
```

Only the override can be used to actually override fields, and only the `Oo.copy` primitive can be used externally.

Cloning can also be used to provide facilities for saving and restoring the state of objects.

```ocaml
# class backup =
  object (self : 'mytype)
    val mutable copy = None
    method save = copy <- Some {< copy = None >}
    method restore = match copy with Some x -> x | None -> self
  end;;
```
```pascal
# let p = new point 5;;
```

```pascal
val p : point = <obj>
```

```pascal
# let q = Oo.copy p;;
```

```pascal
val q : point = <obj>
```

```pascal
# q#move 7; (p#get_x, q#get_x);;
```

```pascal
- : int * int = (5, 12)
```

In fact, `Oo.copy p` will behave as `p#copy` assuming that a public method `copy` with body `{< >}` has been defined in the class of `p`.

Objects can be compared using the generic comparison functions `=` and `<>`. Two objects are equal if and only if they are physically equal. In particular, an object and its copy are not equal.

```pascal
# let q = Oo.copy p;;
```

```pascal
val q : point = <obj>
```

```pascal
# p = q, p = p;;
```

```pascal
- : bool * bool = (false, true)
```

Other generic comparisons such as `<`, `<=`, ...) can also be used on objects. The relation `<` defines an unspecified but strict ordering on objects. The ordering relationship between two objects is fixed permanently once the two objects have been created, and it is not affected by mutation of fields.

Cloning and override have a non empty intersection. They are interchangeable when used within an object and without overriding any field:

```pascal
# class copy =
```

object

method copy = {< >}

end;;

```pascal
class copy : object ('a') method copy : 'a end
```

```pascal
# class copy =
```

object (self)

method copy = Oo.copy self

end;;

```pascal
class copy : object ('a') method copy : 'a end
```

Only the override can be used to actually override fields, and only the `Oo.copy` primitive can be used externally.

Cloning can also be used to provide facilities for saving and restoring the state of objects.

```pascal
# class backup =
```

object (self : 'mytype)

val mutable copy = None

method save = copy <- Some {< copy = None >}

method restore = match copy with Some x -> x | None -> self

end;;
```javascript
class backup :
    object ('a')
        val mutable copy : 'a option
    method restore : 'a
    method save : unit
end
```

The above definition will only backup one level. The backup facility can be added to any class by using multiple inheritance.

```javascript
# class ['a] backup_ref x = object inherit ['a] oref x inherit backup end;;
class ['a] backup_ref :
    'a ->
    object ('b')
        val mutable copy : 'b option
        val mutable x : 'a
    method get : 'a
    method restore : 'b
    method save : unit
    method set : 'a -> unit
end
```

```javascript
# let rec get p n = if n = 0 then p # get else get (p # restore) (n-1);
val get : (< get : 'b; restore : 'a; .. > as 'a) -> int -> 'b = <fun>

# let p = new backup_ref 0 in
    p # save; p # set 1; p # save; p # set 2;
    [get p 0; get p 1; get p 2; get p 3; get p 4];;
- : int list = [2; 1; 1; 1; 1]
```

We can define a variant of backup that retains all copies. (We also add a method `clear` to manually erase all copies.)

```javascript
# class backup =
    object (self : 'mytype)
        val mutable copy = None
        method save = copy <- Some {< >}
        method restore = match copy with Some x -> x | None -> self
        method clear = copy <- None
end;;
class backup :
    object ('a)
        val mutable copy : 'a option
    method clear : unit
    method restore : 'a
    method save : unit
end
```

```javascript
# class ['a] backup_ref x = object inherit ['a] oref x inherit backup end;;
```
```ocaml
class backup :
    object ('a)
        val mutable copy : 'a option
        method restore : 'a
        method save : unit
end
```

The above definition will only backup one level. The backup facility can be added to any class by using multiple inheritance.

```ocaml
# class ['a] backup_ref x = object inherit ['a] oref x inherit backup end;;
class ['a] backup_ref :
    'a ->
    object ('b)
        val mutable copy : 'b option
        val mutable x : 'a
        method get : 'a
        method restore : 'b
        method save : unit
        method set : 'a -> unit
end
```

```ocaml
# let rec get p n = if n = 0 then p # get else get (p # restore) (n-1);;
val get : (< get : 'b; restore : 'a; .. > as 'a) -> int -> 'b = <fun>

# let p = new backup_ref 0 in
    p # save; p # set 1; p # save; p # set 2;
    [get p 0; get p 1; get p 2; get p 3; get p 4];;
- : int list = [2; 1; 1; 1; 1]
```

We can define a variant of backup that retains all copies. (We also add a method `clear` to manually erase all copies.)

```ocaml
# class backup =
    object (self : 'mytype)
        val mutable copy = None
        method save = copy <- Some {< >}
        method restore = match copy with Some x -> x | None -> self
        method clear = copy <- None
    end;;
class backup :
    object ('a)
        val mutable copy : 'a option
        method clear : unit
        method restore : 'a
        method save : unit
end
```

```ocaml
# class ['a] backup_ref x = object inherit ['a] oref x inherit backup end;;
```
```ocaml
class ['a] backup_ref :
  'a ->
object ('b)
  val mutable copy : 'b option
  val mutable x : 'a
  method clear : unit
  method get : 'a
  method restore : 'b
  method save : unit
  method set : 'a -> unit
end

# let p = new backup_ref 0 in
p # save; p # set 1; p # save; p # set 2;
[get p 0; get p 1; get p 2; get p 3; get p 4];;
- : int list = [2; 1; 0; 0; 0]
```

## 3.15 Recursive classes

Recursive classes can be used to define objects whose types are mutually recursive.

```ocaml
# class window =
object
  val mutable topWidget = (None : widget option)
  method topWidget = topWidget
end

and widget (w : window) =
object
  val window = w
  method window = window
end;

class window :
object
  val mutable topWidget : widget option
  method topWidget : widget option
end

and widget : window -> object val window : window method window : window end
```

Although their types are mutually recursive, the classes `widget` and `window` are themselves independent.

## 3.16 Binary methods

A binary method is a method which takes an argument of the same type as self. The class `comparable` below is a template for classes with a binary method `leq` of type `'a -> bool` where the type variable `'a` is bound to the type of self. Therefore, `#comparable` expands to `< leq : 'a -> bool; .. > as 'a`. We see here that the binder `as` also allows writing recursive types.
```kotlin
class ['a] backup_ref :
    'a ->
    object ('b)
        val mutable copy : 'b option
        val mutable x : 'a
        method clear : unit
        method get : 'a
        method restore : 'b
        method save : unit
        method set : 'a -> unit
end

# let p = new backup_ref 0 in
    p # save; p # set 1; p # save; p # set 2;
    [get p 0; get p 1; get p 2; get p 3; get p 4];;
- : int list = [2; 1; 0; 0; 0]
```

## 3.15 Recursive classes

Recursive classes can be used to define objects whose types are mutually recursive.

```kotlin
# class window =
    object
        val mutable topWidget = (None : widget option)
        method topWidget = topWidget
end

and widget (w : window) =
    object
        val window = w
        method window = window
end;

class window :
    object
        val mutable topWidget : widget option
        method topWidget : widget option
end

and widget : window -> object val window : window method window : window end
```

Although their types are mutually recursive, the classes `widget` and `window` are themselves independent.

## 3.16 Binary methods

A binary method is a method which takes an argument of the same type as self. The class `comparable` below is a template for classes with a binary method `leq` of type `'a -> bool` where the type variable `'a` is bound to the type of self. Therefore, `#comparable` expands to `< leq : 'a -> bool; .. > as 'a`. We see here that the binder `as` also allows writing recursive types.
``` OCaml
# class virtual comparable =
  object (_ : 'a)
    method virtual leq : 'a -> bool
  end;;

class virtual comparable : object ('a) method virtual leq : 'a -> bool end
```

We then define a subclass `money` of `comparable`. The class `money` simply wraps floats as comparable objects.<fnref n="1" /> We will extend `money` below with more operations. We have to use a type constraint on the class parameter `x` because the primitive `<=` is a polymorphic function in OCaml. The `inherit` clause ensures that the type of objects of this class is an instance of `#comparable`.

``` OCaml
# class money (x : float) =
  object
    inherit comparable
    val repr = x
    method value = repr
    method leq p = repr <= p#value
  end;;

class money :
  float ->
  object ('a)
    val repr : float
    method leq : 'a -> bool
    method value : float
  end
```

Note that the type `money` is not a subtype of type `comparable`, as the self type appears in contravariant position in the type of method `leq`. Indeed, an object `m` of class `money` has a method `leq` that expects an argument of type `money` since it accesses its `value` method. Considering `m` of type `comparable` would allow a call to method `leq` on `m` with an argument that does not have a method `value`, which would be an error.

Similarly, the type `money2` below is not a subtype of type `money`.

``` OCaml
# class money2 x =
  object
    inherit money x
    method times k = {< repr = k *. repr >}
  end;;

class money2 :
  float ->
  object ('a)
    val repr : float
    method leq : 'a -> bool
    method times : float -> 'a
    method value : float
  end
```

<footnote n="1">¹floats are an approximation of decimal numbers, they are unsuitable for use in most monetary calculations as they may introduce errors.</footnote>
``` OCaml
# class virtual comparable =
object (_ : 'a)
  method virtual leq : 'a -> bool
end;;

class virtual comparable : object ('a) method virtual leq : 'a -> bool end
```

We then define a subclass `money` of `comparable`. The class `money` simply wraps floats as comparable objects.<fnref n="1" /> We will extend `money` below with more operations. We have to use a type constraint on the class parameter `x` because the primitive `<=` is a polymorphic function in OCaml. The `inherit` clause ensures that the type of objects of this class is an instance of `#comparable`.

``` OCaml
# class money (x : float) =
object
  inherit comparable
  val repr = x
  method value = repr
  method leq p = repr <= p#value
end;;

class money :
  float ->
  object ('a)
    val repr : float
    method leq : 'a -> bool
    method value : float
  end
```

Note that the type `money` is not a subtype of type `comparable`, as the self type appears in contravariant position in the type of method `leq`. Indeed, an object `m` of class `money` has a method `leq` that expects an argument of type `money` since it accesses its `value` method. Considering `m` of type `comparable` would allow a call to method `leq` on `m` with an argument that does not have a method `value`, which would be an error.

Similarly, the type `money2` below is not a subtype of type `money`.

``` OCaml
# class money2 x =
object
  inherit money x
  method times k = {< repr = k *. repr >}
end;;

class money2 :
  float ->
  object ('a)
    val repr : float
    method leq : 'a -> bool
    method times : float -> 'a
    method value : float
  end
```

<footnote n="1">¹floats are an approximation of decimal numbers, they are unsuitable for use in most monetary calculations as they may introduce errors.</footnote>
It is however possible to define functions that manipulate objects of type either `money` or `money2`: the function `min` will return the minimum of any two objects whose type unifies with `#comparable`. The type of `min` is not the same as `#comparable -> #comparable -> #comparable`, as the abbreviation `#comparable` hides a type variable (an ellipsis). Each occurrence of this abbreviation generates a new variable.

```ocaml
# let min (x : #comparable) y =
    if x#leq y then x else y;;
val min : (#comparable as 'a) -> 'a -> 'a = <fun>
```

This function can be applied to objects of type `money` or `money2`.

```ocaml
# (min (new money 1.3) (new money 3.1))#value;;
- : float = 1.3

# (min (new money2 5.0) (new money2 3.14))#value;;
- : float = 3.14
```

More examples of binary methods can be found in sections 8.2.1 and 8.2.4.

Note the use of override for method `times`. Writing `new money2 (k *. repr)` instead of `{< repr = k *. repr >}` would not behave well with inheritance: in a subclass `money3` of `money2` the `times` method would return an object of class `money2` but not of class `money3` as would be expected.

The class `money` could naturally carry another binary method. Here is a direct definition:

```ocaml
# class money x =
    object (self : 'a)
        val repr = x
        method value = repr
        method print = print_float repr
        method times k = {< repr = k *. x >}
        method leq (p : 'a) = repr <= p#value
        method plus (p : 'a) = {< repr = x +. p#value >}
    end;;

class money :
    float ->
    object ('a)
        val repr : float
        method leq : 'a -> bool
        method plus : 'a -> 'a
        method print : unit
        method times : float -> 'a
        method value : float
    end
```

## 3.17 Friends

The above class `money` reveals a problem that often occurs with binary methods. In order to interact with other objects of the same class, the representation of `money` objects must be revealed, using a
It is however possible to define functions that manipulate objects of type either `money` or `money2`: the function `min` will return the minimum of any two objects whose type unifies with `#comparable`. The type of `min` is not the same as `#comparable -> #comparable -> #comparable`, as the abbreviation `#comparable` hides a type variable (an ellipsis). Each occurrence of this abbreviation generates a new variable.

```hkl
# let min (x : #comparable) y =
    if x#leq y then x else y;;
val min : (#comparable as 'a) -> 'a -> 'a = <fun>
```

This function can be applied to objects of type `money` or `money2`.

```hkl
# (min (new money 1.3) (new money 3.1))#value;;
- : float = 1.3

# (min (new money2 5.0) (new money2 3.14))#value;;
- : float = 3.14
```

More examples of binary methods can be found in sections 8.2.1 and 8.2.4.

Note the use of override for method `times`. Writing `new money2 (k *. repr)` instead of `{< repr = k *. repr >}` would not behave well with inheritance: in a subclass `money3` of `money2` the `times` method would return an object of class `money2` but not of class `money3` as would be expected.

The class `money` could naturally carry another binary method. Here is a direct definition:

```hkl
# class money x =
    object (self : 'a)
        val repr = x
        method value = repr
        method print = print_float repr
        method times k = {< repr = k *. x >}
        method leq (p : 'a) = repr <= p#value
        method plus (p : 'a) = {< repr = x +. p#value >}
end;;

class money :
    float ->
    object ('a)
        val repr : float
        method leq : 'a -> bool
        method plus : 'a -> 'a
        method print : unit
        method times : float -> 'a
        method value : float
end
```

## 3.17 Friends

The above class `money` reveals a problem that often occurs with binary methods. In order to interact with other objects of the same class, the representation of `money` objects must be revealed, using a
method such as `value`. If we remove all binary methods (here `plus` and `leq`), the representation can easily be hidden inside objects by removing the method `value` as well. However, this is not possible as soon as some binary method requires access to the representation of objects of the same class (other than `self`).

```python
# class safeMoney x =
    object (self : 'a)
        val repr = x
        method print = print_float repr
        method times k = {< repr = k *. x >}
    end;

class safeMoney :
    float ->
    object ('a)
        val repr : float
        method print : unit
        method times : float -> 'a
    end
```

Here, the representation of the object is known only to a particular object. To make it available to other objects of the same class, we are forced to make it available to the whole world. However we can easily restrict the visibility of the representation using the module system.

```python
# module type MONEY =
    sig
type t
    class c : float ->
        object ('a)
            val repr : t
            method value : t
            method print : unit
            method times : float -> 'a
            method leq : 'a -> bool
            method plus : 'a -> 'a
        end
    end;

# module Euro : MONEY =
    struct
type t = float
class c x =
    object (self : 'a)
        val repr = x
        method value = repr
        method print = print_float repr
        method times k = {< repr = k *. x >}
        method leq (p : 'a) = repr <= p#value
        method plus (p : 'a) = {< repr = x +. p#value >}
```
method such as `value`. If we remove all binary methods (here `plus` and `leq`), the representation can easily be hidden inside objects by removing the method `value` as well. However, this is not possible as soon as some binary method requires access to the representation of objects of the same class (other than self).

``` OCaml
# class safeMoney x =
    object (self : 'a)
        val repr = x
        method print = print_float repr
        method times k = {< repr = k *. x >}
    end;

class safeMoney :
    float ->
    object ('a)
        val repr : float
        method print : unit
        method times : float -> 'a
    end
```

Here, the representation of the object is known only to a particular object. To make it available to other objects of the same class, we are forced to make it available to the whole world. However we can easily restrict the visibility of the representation using the module system.

``` OCaml
# module type MONEY =
    sig
        type t
        class c : float ->
            object ('a)
                val repr : t
                method value : t
                method print : unit
                method times : float -> 'a
                method leq : 'a -> bool
                method plus : 'a -> 'a
            end
    end;

# module Euro : MONEY =
    struct
        type t = float
        class c x =
            object (self : 'a)
                val repr = x
                method value = repr
                method print = print_float repr
                method times k = {< repr = k *. x >}
                method leq (p : 'a) = repr <= p#value
                method plus (p : 'a) = {< repr = x +. p#value >}
            end
```
end
end;;

Another example of friend functions may be found in section 8.2.4. These examples occur when a group of objects (here objects of the same class) and functions should see each others internal representation, while their representation should be hidden from the outside. The solution is always to define all friends in the same module, give access to the representation and use a signature constraint to make the representation abstract outside the module.
end
end;;

Another example of friend functions may be found in section 8.2.4. These examples occur when a group of objects (here objects of the same class) and functions should see each others internal representation, while their representation should be hidden from the outside. The solution is always to define all friends in the same module, give access to the representation and use a signature constraint to make the representation abstract outside the module.
# Chapter 4

## Labeled arguments

*(Chapter written by Jacques Garrigue)*

If you have a look at modules ending in `Labels` in the standard library, you will see that function types have annotations you did not have in the functions you defined yourself.

```hkl
# ListLabels.map;;
- : f:('a -> 'b) -> 'a list -> 'b list = <fun>

# StringLabels.sub;;
- : string -> pos:int -> len:int -> string = <fun>
```

Such annotations of the form `name:` are called *labels*. They are meant to document the code, allow more checking, and give more flexibility to function application. You can give such names to arguments in your programs, by prefixing them with a tilde `~`.

```hkl
# let f ~x ~y = x - y;;
val f : x:int -> y:int -> int = <fun>

# let x = 3 and y = 2 in f ~x ~y;;
- : int = 1
```

When you want to use distinct names for the variable and the label appearing in the type, you can use a naming label of the form `~name:`. This also applies when the argument is not a variable.

```hkl
# let f ~x:x1 ~y:y1 = x1 - y1;;
val f : x:int -> y:int -> int = <fun>

# f ~x:3 ~y:2;;
- : int = 1
```

Labels obey the same rules as other identifiers in OCaml, that is you cannot use a reserved keyword (like `in` or `to`) as a label.

Formal parameters and arguments are matched according to their respective labels, the absence of label being interpreted as the empty label. This allows commuting arguments in applications. One can also partially apply a function on any argument, creating a new function of the remaining parameters.

```hkl
# let f ~x ~y = x - y;;
```
# Chapter 4

## Labeled arguments

*(Chapter written by Jacques Garrigue)*

If you have a look at modules ending in `Labels` in the standard library, you will see that function types have annotations you did not have in the functions you defined yourself.

```hkl
# ListLabels.map;;
- : f:('a -> 'b) -> 'a list -> 'b list = <fun>
```

```hkl
# StringLabels.sub;;
- : string -> pos:int -> len:int -> string = <fun>
```

Such annotations of the form `name:` are called *labels*. They are meant to document the code, allow more checking, and give more flexibility to function application. You can give such names to arguments in your programs, by prefixing them with a tilde `~`.

```hkl
# let f ~x ~y = x - y;;
val f : x:int -> y:int -> int = <fun>
```

```hkl
# let x = 3 and y = 2 in f ~x ~y;;
- : int = 1
```

When you want to use distinct names for the variable and the label appearing in the type, you can use a naming label of the form `~name:`. This also applies when the argument is not a variable.

```hkl
# let f ~x:x1 ~y:y1 = x1 - y1;;
val f : x:int -> y:int -> int = <fun>
```

```hkl
# f ~x:3 ~y:2;;
- : int = 1
```

Labels obey the same rules as other identifiers in OCaml, that is you cannot use a reserved keyword (like `in` or `to`) as a label.

Formal parameters and arguments are matched according to their respective labels, the absence of label being interpreted as the empty label. This allows commuting arguments in applications. One can also partially apply a function on any argument, creating a new function of the remaining parameters.

```hkl
# let f ~x ~y = x - y;;
```
```h
val f : x:int -> y:int -> int = <fun>
```

```h
# f ~y:2 ~x:3;;
- : int = 1
```

```h
# ListLabels.fold_left;;
- : f('acc -> 'a -> 'acc) -> init:'acc -> 'a list -> 'acc = <fun>
```

```h
# ListLabels.fold_left [1;2;3] ~init:0 ~f:( + );;
- : int = 6
```

```h
# ListLabels.fold_left ~init:0;;
- : f(int -> 'a -> int) -> 'a list -> int = <fun>
```

If several arguments of a function bear the same label (or no label), they will not commute among themselves, and order matters. But they can still commute with other arguments.

```h
# let hline ~x:x1 ~x:x2 ~y = (x1, x2, y);;
val hline : x:'a -> x:'b -> y:'c -> 'a * 'b * 'c = <fun>
```

```h
# hline ~x:3 ~y:2 ~x:5;;
- : int * int * int = (3, 5, 2)
```

## 4.1 Optional arguments

An interesting feature of labeled arguments is that they can be made optional. For optional parameters, the question mark ? replaces the tilde ~ of non-optional ones, and the label is also prefixed by ? in the function type. Default values may be given for such optional parameters.

```h
# let bump ?(step = 1) x = x + step;;
val bump : ?step:int -> int -> int = <fun>
```

```h
# bump 2;;
- : int = 3
```

```h
# bump ~step:3 2;;
- : int = 5
```

A function taking some optional arguments must also take at least one non-optional argument. The criterion for deciding whether an optional argument has been omitted is the non-labeled application of an argument appearing after this optional argument in the function type. Note that if that argument is labeled, you will only be able to eliminate optional arguments by totally applying the function, omitting all optional arguments and omitting all labels for all remaining arguments.

```h
# let test ?(x = 0) ?(y = 0) () ?(z = 0) () = (x, y, z);;
val test : ?x:int -> ?y:int -> unit -> ?z:int -> unit -> int * int * int =
    <fun>
```

```h
# test ();;
```
```h
val f : x:int -> y:int -> int = <fun>

# f ~y:2 ~x:3;;
- : int = 1

# ListLabels.fold_left;;
- : f('acc -> 'a -> 'acc) -> init:'acc -> 'a list -> 'acc = <fun>

# ListLabels.fold_left [1;2;3] ~init:0 ~f:( + );;
- : int = 6

# ListLabels.fold_left ~init:0;;
- : f(int -> 'a -> int) -> 'a list -> int = <fun>
```

If several arguments of a function bear the same label (or no label), they will not commute among themselves, and order matters. But they can still commute with other arguments.

```h
# let hline ~x:x1 ~x:x2 ~y = (x1, x2, y);;
val hline : x:'a -> x:'b -> y:'c -> 'a * 'b * 'c = <fun>

# hline ~x:3 ~y:2 ~x:5;;
- : int * int * int = (3, 5, 2)
```

## 4.1 Optional arguments

An interesting feature of labeled arguments is that they can be made optional. For optional parameters, the question mark ? replaces the tilde ~ of non-optional ones, and the label is also prefixed by ? in the function type. Default values may be given for such optional parameters.

```h
# let bump ?(step = 1) x = x + step;;
val bump : ?step:int -> int -> int = <fun>

# bump 2;;
- : int = 3

# bump ~step:3 2;;
- : int = 5
```

A function taking some optional arguments must also take at least one non-optional argument. The criterion for deciding whether an optional argument has been omitted is the non-labeled application of an argument appearing after this optional argument in the function type. Note that if that argument is labeled, you will only be able to eliminate optional arguments by totally applying the function, omitting all optional arguments and omitting all labels for all remaining arguments.

```h
# let test ?(x = 0) ?(y = 0) () ?(z = 0) () = (x, y, z);;
val test : ?x:int -> ?y:int -> unit -> ?z:int -> unit -> int * int * int =
    <fun>

# test ();;
```
- : ?z:int -> unit -> int * int * int = <fun>

# test ~x:2 () ~z:3 ();;

- : int * int * int = (2, 0, 3)

Optional parameters may also commute with non-optional or unlabeled ones, as long as they are applied simultaneously. By nature, optional arguments do not commute with unlabeled arguments applied independently.

# test ~y:2 ~x:3 () ();;

- : int * int * int = (3, 2, 0)

# test () () ~z:1 ~y:2 ~x:3;;

- : int * int * int = (3, 2, 1)

# (test ()()) ~z:1 ;;

Error: This expression has type int * int * int
This is not a function; it cannot be applied.

Here (test ()()) is already (0,0,0) and cannot be further applied.

Optional arguments are actually implemented as option types. If you do not give a default value, you have access to their internal representation, `type 'a option = None | Some of 'a`. You can then provide different behaviors when an argument is present or not.

# let bump ?step x =
    match step with
    | None -> x * 2
    | Some y -> x + y

;;

val bump : ?step:int -> int -> int = <fun>

It may also be useful to relay an optional argument from a function call to another. This can be done by prefixing the applied argument with ?. This question mark disables the wrapping of optional argument in an option type.

# let test2 ?x ?y () = test ?x ?y () ();;

val test2 : ?x:int -> ?y:int -> unit -> int * int * int = <fun>

# test2 ?x:None;;

- : ?y:int -> unit -> int * int * int = <fun>

## 4.2 Labels and type inference

While they provide an increased comfort for writing function applications, labels and optional arguments have the pitfall that they cannot be inferred as completely as the rest of the language.

You can see it in the following two examples.

# let h' g = g ~y:2 ~x:3;;

val h' : (y:int -> x:int -> 'a) -> 'a = <fun>
- : ?z:int -> unit -> int * int * int = <fun>

# test ~x:2 () ~z:3 ();;
- : int * int * int = (2, 0, 3)

Optional parameters may also commute with non-optional or unlabeled ones, as long as they are
applied simultaneously. By nature, optional arguments do not commute with unlabeled arguments
applied independently.

# test ~y:2 ~x:3 () ();;
- : int * int * int = (3, 2, 0)

# test () () ~z:1 ~y:2 ~x:3;;
- : int * int * int = (3, 2, 1)

# (test ()()) ~z:1 ;;

Error: This expression has type int * int * int
This is not a function; it cannot be applied.

Here (test ()()) is already (0,0,0) and cannot be further applied.

Optional arguments are actually implemented as option types. If you do not give a default value, you have access to their internal representation, `type 'a option = None | Some of 'a`. You can then provide different behaviors when an argument is present or not.

# let bump ?step x =
  match step with
  | None -> x * 2
  | Some y -> x + y
;;
val bump : ?step:int -> int -> int = <fun>

It may also be useful to relay an optional argument from a function call to another. This can be done by prefixing the applied argument with ?. This question mark disables the wrapping of optional argument in an option type.

# let test2 ?x ?y () = test ?x ?y () ();;
val test2 : ?x:int -> ?y:int -> unit -> int * int * int = <fun>

# test2 ?x:None;;
- : ?y:int -> unit -> int * int * int = <fun>

## 4.2 Labels and type inference

While they provide an increased comfort for writing function applications, labels and optional arguments have the pitfall that they cannot be inferred as completely as the rest of the language.

You can see it in the following two examples.

# let h' g = g ~y:2 ~x:3;;
val h' : (y:int -> x:int -> 'a) -> 'a = <fun>
```h
# h' f ;;
```

```
Error: This expression has type x:int -> y:int -> int
       but an expression was expected of type y:int -> x:int -> 'a
```

```h
# let bump_it bump x =
       bump ~step:2 x;;
```

```
val bump_it : (step:int -> 'a -> 'b) -> 'a -> 'b = <fun>
```

```h
# bump_it bump 1 ;;
```

```
Error: This expression has type ?step:int -> int -> int
       but an expression was expected of type step:int -> 'a -> 'b
```

The first case is simple: `g` is passed `~y` and then `~x`, but `f` expects `~x` and then `~y`. This is correctly handled if we know the type of `g` to be `x:int -> y:int -> int` in advance, but otherwise this causes the above type clash. The simplest workaround is to apply formal parameters in a standard order.

The second example is more subtle: while we intended the argument `bump` to be of type `?step:int -> int -> int`, it is inferred as `step:int -> int -> 'a`. These two types being incompatible (internally normal and optional arguments are different), a type error occurs when applying `bump_it` to the real `bump`.

We will not try here to explain in detail how type inference works. One must just understand that there is not enough information in the above program to deduce the correct type of `g` or `bump`. That is, there is no way to know whether an argument is optional or not, or which is the correct order, by looking only at how a function is applied. The strategy used by the compiler is to assume that there are no optional arguments, and that applications are done in the right order.

The right way to solve this problem for optional parameters is to add a type annotation to the argument `bump`.

```h
# let bump_it (bump : ?step:int -> int -> int) x =
       bump ~step:2 x;;
```

```
val bump_it : (?step:int -> int -> int) -> int -> int = <fun>
```

```h
# bump_it bump 1;;
- : int = 3
```

In practice, such problems appear mostly when using objects whose methods have optional arguments, so writing the type of object arguments is often a good idea.

Normally the compiler generates a type error if you attempt to pass to a function a parameter whose type is different from the expected one. However, in the specific case where the expected type is a non-labeled function type, and the argument is a function expecting optional parameters, the compiler will attempt to transform the argument to have it match the expected type, by passing `None` for all optional parameters.

```h
# let twice f (x : int) = f(f x);;
```

```
val twice : (int -> int) -> int -> int = <fun>
```

```h
# twice bump 2;;
```
# h' f ;;

Error: The value f has type x:int -> y:int -> int
but an expression was expected of type y:int -> x:int -> 'a
Labels x and y do not match

# let bump_it bump x =

bump ~step:2 x;;

val bump_it : (step:int -> 'a -> 'b) -> 'a -> 'b = <fun>

# bump_it bump 1 ;;

Error: The value bump has type ?step:int -> int -> int
but an expression was expected of type step:int -> 'a -> 'b
The label ?step was expected to not be optional

The first case is simple: g is passed ~y and then ~x, but f expects ~x and then ~y. This is correctly handled if we know the type of g to be x:int -> y:int -> int in advance, but otherwise this causes the above type clash. The simplest workaround is to apply formal parameters in a standard order.

The second example is more subtle: while we intended the argument `bump` to be of type `?step:int -> int -> int`, it is inferred as `step:int -> int -> 'a`. These two types being incompatible (internally normal and optional arguments are different), a type error occurs when applying `bump_it` to the real `bump`.

We will not try here to explain in detail how type inference works. One must just understand that there is not enough information in the above program to deduce the correct type of `g` or `bump`. That is, there is no way to know whether an argument is optional or not, or which is the correct order, by looking only at how a function is applied. The strategy used by the compiler is to assume that there are no optional arguments, and that applications are done in the right order.

The right way to solve this problem for optional parameters is to add a type annotation to the argument `bump`.

# let bump_it (bump : ?step:int -> int -> int) x =

bump ~step:2 x;;

val bump_it : (?step:int -> int -> int) -> int -> int = <fun>

# bump_it bump 1;;

- : int = 3

In practice, such problems appear mostly when using objects whose methods have optional arguments, so writing the type of object arguments is often a good idea.

Normally the compiler generates a type error if you attempt to pass to a function a parameter whose type is different from the expected one. However, in the specific case where the expected type is a non-labeled function type, and the argument is a function expecting optional parameters, the compiler will attempt to transform the argument to have it match the expected type, by passing `None` for all optional parameters.

# let twice f (x : int) = f(f x);;

val twice : (int -> int) -> int -> int = <fun>
- : int = 8

This transformation is coherent with the intended semantics, including side-effects. That is, if the application of optional parameters shall produce side-effects, these are delayed until the received function is really applied to an argument.

## 4.3 Suggestions for labeling

Like for names, choosing labels for functions is not an easy task. A good labeling is one which

* makes programs more readable,

* is easy to remember,

* when possible, allows useful partial applications.

We explain here the rules we applied when labeling OCaml libraries.

To speak in an “object-oriented” way, one can consider that each function has a main argument, its *object*, and other arguments related with its action, the *parameters*. To permit the combination of functions through functionals in commuting label mode, the object will not be labeled. Its role is clear from the function itself. The parameters are labeled with names reminding of their nature or their role. The best labels combine nature and role. When this is not possible the role is to be preferred, since the nature will often be given by the type itself. Obscure abbreviations should be avoided.

ListLabels.map : f:('a -> 'b) -> 'a list -> 'b list

UnixLabels.write : file_descr -> buf:bytes -> pos:int -> len:int -> unit

When there are several objects of same nature and role, they are all left unlabeled.

ListLabels.iter2 : f:('a -> 'b -> unit) -> 'a list -> 'b list -> unit

When there is no preferable object, all arguments are labeled.

BytesLabels.blit :

src:bytes -> src_pos:int -> dst:bytes -> dst_pos:int -> len:int -> unit

However, when there is only one argument, it is often left unlabeled.

BytesLabels.create : int -> bytes

This principle also applies to functions of several arguments whose return type is a type variable, as long as the role of each argument is not ambiguous. Labeling such functions may lead to awkward error messages when one attempts to omit labels in an application, as we have seen with `ListLabels.fold_left`.

Here are some of the label names you will find throughout the libraries.
```h
# twice bump 2;;
- : int = 8
```

This transformation is coherent with the intended semantics, including side-effects. That is, if the application of optional parameters shall produce side-effects, these are delayed until the received function is really applied to an argument.

## 4.3 Suggestions for labeling

Like for names, choosing labels for functions is not an easy task. A good labeling is one which

* makes programs more readable,

* is easy to remember,

* when possible, allows useful partial applications.

We explain here the rules we applied when labeling OCaml libraries.

To speak in an “object-oriented” way, one can consider that each function has a main argument, its *object*, and other arguments related with its action, the *parameters*. To permit the combination of functions through functionals in commuting label mode, the object will not be labeled. Its role is clear from the function itself. The parameters are labeled with names reminding of their nature or their role. The best labels combine nature and role. When this is not possible the role is to be preferred, since the nature will often be given by the type itself. Obscure abbreviations should be avoided.

```
ListLabels.map : f:('a -> 'b) -> 'a list -> 'b list
UnixLabels.write : file_descr -> buf:bytes -> pos:int -> len:int -> unit
```

When there are several objects of same nature and role, they are all left unlabeled.

```
ListLabels.iter2 : f:('a -> 'b -> unit) -> 'a list -> 'b list -> unit
```

When there is no preferable object, all arguments are labeled.

```
BytesLabels.blit :
    src:bytes -> src_pos:int -> dst:bytes -> dst_pos:int -> len:int -> unit
```

However, when there is only one argument, it is often left unlabeled.

```
BytesLabels.create : int -> bytes
```

This principle also applies to functions of several arguments whose return type is a type variable, as long as the role of each argument is not ambiguous. Labeling such functions may lead to awkward error messages when one attempts to omit labels in an application, as we have seen with `ListLabels.fold_left`.

Here are some of the label names you will find throughout the libraries.
<table><thead><tr><td>Label</td><td>Meaning</td></tr></thead><tbody><tr><td>f:</td><td>a function to be applied</td></tr><tr><td>pos:</td><td>a position in a string, array or byte sequence</td></tr><tr><td>len:</td><td>a length</td></tr><tr><td>buf:</td><td>a byte sequence or string used as buffer</td></tr><tr><td>src:</td><td>the source of an operation</td></tr><tr><td>dst:</td><td>the destination of an operation</td></tr><tr><td>init:</td><td>the initial value for an iterator</td></tr><tr><td>cmp:</td><td>a comparison function, e.g. Stdlib compares</td></tr><tr><td>mode:</td><td>an operation mode or a flag list</td></tr></tbody></table>

All these are only suggestions, but keep in mind that the choice of labels is essential for readability. Bizarre choices will make the program harder to maintain.

In the ideal, the right function name with right labels should be enough to understand the function's meaning. Since one can get this information with OCamlBrowser or the ocaml toplevel, the documentation is only used when a more detailed specification is needed.
<table><thead><tr><td>Label</td><td>Meaning</td></tr></thead><tbody><tr><td>f:</td><td>a function to be applied</td></tr><tr><td>pos:</td><td>a position in a string, array or byte sequence</td></tr><tr><td>len:</td><td>a length</td></tr><tr><td>buf:</td><td>a byte sequence or string used as buffer</td></tr><tr><td>src:</td><td>the source of an operation</td></tr><tr><td>dst:</td><td>the destination of an operation</td></tr><tr><td>init:</td><td>the initial value for an iterator</td></tr><tr><td>cmp:</td><td>a comparison function, e.g. Stdlib compares</td></tr><tr><td>mode:</td><td>an operation mode or a flag list</td></tr></tbody></table>

All these are only suggestions, but keep in mind that the choice of labels is essential for readability. Bizarre choices will make the program harder to maintain.

In the ideal, the right function name with right labels should be enough to understand the function's meaning. Since one can get this information with OCamlBrowser or the ocaml toplevel, the documentation is only used when a more detailed specification is needed.
# Chapter 5

## Polymorphic variants

*(Chapter written by Jacques Garrigue)*

Variants as presented in section 1.4 are a powerful tool to build data structures and algorithms. However they sometimes lack flexibility when used in modular programming. This is due to the fact that every constructor is assigned to a unique type when defined and used. Even if the same name appears in the definition of multiple types, the constructor itself belongs to only one type. Therefore, one cannot decide that a given constructor belongs to multiple types, or consider a value of some type to belong to some other type with more constructors.

With polymorphic variants, this original assumption is removed. That is, a variant tag does not belong to any type in particular, the type system will just check that it is an admissible value according to its use. You need not define a type before using a variant tag. A variant type will be inferred independently for each of its uses.

### 5.1 Basic use

In programs, polymorphic variants work like usual ones. You just have to prefix their names with a backquote character `.

```hkl
# [`On; `Off];
- : [> `Off | `On ] list = [`On; `Off]
```

```hkl
# `Number 1;;
- : [> `Number of int ] = `Number 1
```

```hkl
# let f = function `On -> 1 | `Off -> 0 | `Number n -> n;;
val f : [< `Number of int | `Off | `On ] -> int = <fun>
```

```hkl
# List.map f [`On; `Off];;
- : int list = [1; 0]
```

``[> `Off | `On] list means that to match this list, you should at least be able to match `Off and `On, without argument. [<`On | `Off | `Number of int] means that f may be applied to `Off, `On (both without argument), or `Number n where n is an integer. The > and < inside the variant types show that they may still be refined, either by defining more tags or by allowing less. As such, they
# Chapter 5

## Polymorphic variants

*(Chapter written by Jacques Garrigue)*

Variants as presented in section 1.4 are a powerful tool to build data structures and algorithms. However they sometimes lack flexibility when used in modular programming. This is due to the fact that every constructor is assigned to a unique type when defined and used. Even if the same name appears in the definition of multiple types, the constructor itself belongs to only one type. Therefore, one cannot decide that a given constructor belongs to multiple types, or consider a value of some type to belong to some other type with more constructors.

With polymorphic variants, this original assumption is removed. That is, a variant tag does not belong to any type in particular, the type system will just check that it is an admissible value according to its use. You need not define a type before using a variant tag. A variant type will be inferred independently for each of its uses.

### 5.1 Basic use

In programs, polymorphic variants work like usual ones. You just have to prefix their names with a backquote character `.

```hkl
# [`On; `Off];
- : [> `Off | `On ] list = [`On; `Off]
```

```hkl
# `Number 1;;
- : [> `Number of int ] = `Number 1
```

```hkl
# let f = function `On -> 1 | `Off -> 0 | `Number n -> n;;
val f : [< `Number of int | `Off | `On ] -> int = <fun>
```

```hkl
# List.map f [`On; `Off];;
- : int list = [1; 0]
```

```
[> `Off | `On] list means that to match this list, you should at least be able to match `Off and
`On, without argument. [<`On | `Off | `Number of int] means that f may be applied to `Off, `On
(both without argument), or `Number n where n is an integer. The > and < inside the variant types
show that they may still be refined, either by defining more tags or by allowing less. As such, they
```
contain an implicit type variable. Because each of the variant types appears only once in the whole type, their implicit type variables are not shown.

The above variant types were polymorphic, allowing further refinement. When writing type annotations, one will most often describe fixed variant types, that is types that cannot be refined. This is also the case for type abbreviations. Such types do not contain < or >, but just an enumeration of the tags and their associated types, just like in a normal datatype definition.

```hkl
# type 'a vlist = [ `Nil | `Cons of 'a * 'a vlist];;

type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ]
```

```hkl
# let rec map f : 'a vlist -> 'b vlist = function
| `Nil -> `Nil
| `Cons(a, 1) -> `Cons(f a, map f 1)
;;
val map : ('a -> 'b) -> 'a vlist -> 'b vlist = <fun>
```

## 5.2 Advanced use

Type-checking polymorphic variants is a subtle thing, and some expressions may result in more complex type information.

```hkl
# let f = function `A -> `C | `B -> `D | x -> x;;
val f : ([> `A | `B | `C | `D ] as 'a) -> 'a = <fun>
```

```hkl
# f `E;;
- : [> `A | `B | `C | `D | `E ] = `E
```

Here we are seeing two phenomena. First, since this matching is open (the last case catches any tag), we obtain the type [> `A | `B] rather than [< `A | `B] in a closed matching. Then, since x is returned as is, input and return types are identical. The notation as 'a denotes such type sharing. If we apply f to yet another tag `E, it gets added to the list.

```hkl
# let f1 = function `A x -> x = 1 | `B -> true | `C -> false
let f2 = function `A x -> x = "a" | `B -> true ;;
val f1 : [< `A of int | `B | `C ] -> bool = <fun>
val f2 : [< `A of string | `B ] -> bool = <fun>
```

```hkl
# let f x = f1 x && f2 x;;
val f : [< `A of string & int | `B ] -> bool = <fun>
```

Here f1 and f2 both accept the variant tags `A and `B, but the argument of `A is int for f1 and string for f2. In f's type `C, only accepted by f1, disappears, but both argument types appear for `A as int & string. This means that if we pass the variant tag `A to f, its argument should be both int and string. Since there is no such value, f cannot be applied to `A, and `B is the only accepted input.

Even if a value has a fixed variant type, one can still give it a larger type through coercions. Coercions are normally written with both the source type and the destination type, but in simple cases the source type may be omitted.
contain an implicit type variable. Because each of the variant types appears only once in the whole type, their implicit type variables are not shown.

The above variant types were polymorphic, allowing further refinement. When writing type annotations, one will most often describe fixed variant types, that is types that cannot be refined. This is also the case for type abbreviations. Such types do not contain < or >, but just an enumeration of the tags and their associated types, just like in a normal datatype definition.

```hkl
# type 'a vlist = [ `Nil | `Cons of 'a * 'a vlist];;

type 'a vlist = [ `Cons of 'a * 'a vlist | `Nil ]
```

```hkl
# let rec map f : 'a vlist -> 'b vlist = function
| `Nil -> `Nil
| `Cons(a, 1) -> `Cons(f a, map f 1)
;;
val map : ('a -> 'b) -> 'a vlist -> 'b vlist = <fun>
```

## 5.2 Advanced use

Type-checking polymorphic variants is a subtle thing, and some expressions may result in more complex type information.

```hkl
# let f = function `A -> `C | `B -> `D | x -> x;;
val f : ([> `A | `B | `C | `D ] as 'a) -> 'a = <fun>
```

```hkl
# f `E;;
- : [> `A | `B | `C | `D | `E ] = `E
```

Here we are seeing two phenomena. First, since this matching is open (the last case catches any tag), we obtain the type [> `A | `B] rather than [< `A | `B] in a closed matching. Then, since x is returned as is, input and return types are identical. The notation as 'a denotes such type sharing. If we apply f to yet another tag `E, it gets added to the list.

```hkl
# let f1 = function `A x -> x = 1 | `B -> true | `C -> false
let f2 = function `A x -> x = "a" | `B -> true ;;
val f1 : [< `A of int | `B | `C ] -> bool = <fun>
val f2 : [< `A of string | `B ] -> bool = <fun>
```

```hkl
# let f x = f1 x && f2 x;;
val f : [< `A of string & int | `B ] -> bool = <fun>
```

Here f1 and f2 both accept the variant tags `A and `B, but the argument of `A is int for f1 and string for f2. In f's type `C, only accepted by f1, disappears, but both argument types appear for `A as int & string. This means that if we pass the variant tag `A to f, its argument should be both int and string. Since there is no such value, f cannot be applied to `A, and `B is the only accepted input.

Even if a value has a fixed variant type, one can still give it a larger type through coercions. Coercions are normally written with both the source type and the destination type, but in simple cases the source type may be omitted.
```h
# type 'a wlist = [ `Nil | `Cons of 'a * 'a wlist | `Snoc of 'a wlist * 'a] ;;
type 'a wlist = [ `Cons of 'a * 'a wlist | `Nil | `Snoc of 'a wlist * 'a ]
```

```h
# let wlist_of_vlist l = (l : 'a vlist :> 'a wlist);;
val wlist_of_vlist : 'a vlist -> 'a wlist = <fun>
```

```h
# let open_vlist l = (l : 'a vlist :> [> 'a vlist]);
val open_vlist : 'a vlist -> [> 'a vlist ] = <fun>
```

```h
# fun x -> (x :> [`A | `B | `C]);
- : [< `A | `B | `C ] -> [ `A | `B | `C ] = <fun>
```

You may also selectively coerce values through pattern matching.

```h
# let split_cases = function
| `Nil | `Cons _ as x -> `A x
| `Snoc _ as x -> `B x
;;
val split_cases :
[< `Cons of 'a | `Nil | `Snoc of 'b ] ->
[> `A of [> `Cons of 'a | `Nil ] | `B of [> `Snoc of 'b ] ] = <fun>
```

When an or-pattern composed of variant tags is wrapped inside an alias-pattern, the alias is given a type containing only the tags enumerated in the or-pattern. This allows for many useful idioms, like incremental definition of functions.

```h
# let num x = `Num x
let eval1 eval (`Num x) = x
let rec eval x = eval1 eval x ;;
val num : 'a -> [> `Num of 'a ] = <fun>
val eval1 : 'a -> [< `Num of 'b ] -> 'b = <fun>
val eval : [< `Num of 'a ] -> 'a = <fun>

# let plus x y = `Plus(x,y)
let eval2 eval = function
| `Plus(x,y) -> eval x + eval y
| `Num _ as x -> eval1 eval x
let rec eval x = eval2 eval x ;;
val plus : 'a -> 'b -> [> `Plus of 'a * 'b ] = <fun>
val eval2 : ('a -> int) -> [< `Num of int | `Plus of 'a * 'a ] -> int = <fun>
val eval : ([< `Num of int | `Plus of 'a * 'a ] as 'a) -> int = <fun>
```

To make this even more comfortable, you may use type definitions as abbreviations for or-patterns. That is, if you have defined `type myvariant = [`Tag1 of int | `Tag2 of bool], then the pattern `myvariant` is equivalent to writing (`Tag1(_ : int) | `Tag2(_ : bool)`).

Such abbreviations may be used alone,

```h
# let f = function
| #myvariant -> "myvariant"
| `Tag3 -> "Tag3";;
```
```h
# type 'a wlist = [ `Nil | `Cons of 'a * 'a wlist | `Snoc of 'a wlist * 'a];;
type 'a wlist = [ `Cons of 'a * 'a wlist | `Nil | `Snoc of 'a wlist * 'a ]
```

```h
# let wlist_of_vlist l = (l : 'a vlist :> 'a wlist);;
val wlist_of_vlist : 'a vlist -> 'a wlist = <fun>
```

```h
# let open_vlist l = (l : 'a vlist :> [> 'a vlist]);
val open_vlist : 'a vlist -> [> 'a vlist ] = <fun>
```

```h
# fun x -> (x :> [`A | `B | `C]);
- : [< `A | `B | `C ] -> [ `A | `B | `C ] = <fun>
```

You may also selectively coerce values through pattern matching.

```h
# let split_cases = function
| `Nil | `Cons _ as x -> `A x
| `Snoc _ as x -> `B x
;;
val split_cases :
[< `Cons of 'a | `Nil | `Snoc of 'b ] ->
[> `A of [> `Cons of 'a | `Nil ] | `B of [> `Snoc of 'b ] ] = <fun>
```

When an or-pattern composed of variant tags is wrapped inside an alias-pattern, the alias is given a type containing only the tags enumerated in the or-pattern. This allows for many useful idioms, like incremental definition of functions.

```h
# let num x = `Num x
let eval1 eval (`Num x) = x
let rec eval x = eval1 eval x ;;
val num : 'a -> [> `Num of 'a ] = <fun>
val eval1 : 'a -> [< `Num of 'b ] -> 'b = <fun>
val eval : [< `Num of 'a ] -> 'a = <fun>

# let plus x y = `Plus(x,y)
let eval2 eval = function
| `Plus(x,y) -> eval x + eval y
| `Num _ as x -> eval1 eval x
let rec eval x = eval2 eval x ;;
val plus : 'a -> 'b -> [> `Plus of 'a * 'b ] = <fun>
val eval2 : ('a -> int) -> [< `Num of int | `Plus of 'a * 'a ] -> int = <fun>
val eval : ([< `Num of int | `Plus of 'a * 'a ] as 'a) -> int = <fun>
```

To make this even more comfortable, you may use type definitions as abbreviations for or-patterns. That is, if you have defined `type myvariant = [`Tag1 of int | `Tag2 of bool], then the pattern `myvariant` is equivalent to writing (`Tag1(_ : int) | `Tag2(_ : bool)`).

Such abbreviations may be used alone,

```h
# let f = function
| #myvariant -> "myvariant"
| `Tag3 -> "Tag3";;
```
```javascript
val f: [< `Tag1` of `int` | `Tag2` of `bool` | `Tag3`] -> string = <fun>
```

or combined with with aliases.

```javascript
# let g1 = function `Tag1` _ -> "Tag1" | `Tag2` _ -> "Tag2";;
```

```javascript
val g1: [< `Tag1` of 'a' | `Tag2` of 'b'] -> string = <fun>
```

```javascript
# let g = function
| #myvariant as x -> g1 x
```

```javascript
| `Tag3` -> "Tag3";;
```

```javascript
val g: [< `Tag1` of `int` | `Tag2` of `bool` | `Tag3`] -> string = <fun>
```

## 5.3 Weaknesses of polymorphic variants

After seeing the power of polymorphic variants, one may wonder why they were added to core language variants, rather than replacing them.

The answer is twofold. The first aspect is that while being pretty efficient, the lack of static type information allows for less optimizations, and makes polymorphic variants slightly heavier than core language ones. However noticeable differences would only appear on huge data structures.

More important is the fact that polymorphic variants, while being type-safe, result in a weaker type discipline. That is, core language variants do actually much more than ensuring type-safety, they also check that you use only declared constructors, that all constructors present in a data-structure are compatible, and they enforce typing constraints to their parameters.

For this reason, you must be more careful about making types explicit when you use polymorphic variants. When you write a library, this is easy since you can describe exact types in interfaces, but for simple programs you are probably better off with core language variants.

Beware also that some idioms make trivial errors very hard to find. For instance, the following code is probably wrong but the compiler has no way to see it.

```javascript
# type abc = [ `A` | `B` | `C` ] ;;
type abc = [ `A` | `B` | `C` ]

# let f = function
| `As` -> "A"
| #abc -> "other" ;;
```

```javascript
val f: [< `A` | `As` | `B` | `C` ] -> string = <fun>
```

```javascript
val f: abc -> string = <fun>
```

You can avoid such risks by annotating the definition itself.

```javascript
# let f: abc -> string = function
```

```javascript
| `As` -> "A"
```

```javascript
| #abc -> "other" ;;
```

```
Error: This pattern matches values of type [? `As`
but a pattern was expected which matches values of type abc
The second variant type does not allow tag(s) `As
```
```h
val f : [< `Tag1 of int | `Tag2 of bool | `Tag3 ] -> string = <fun>
```

or combined with with aliases.

```h
# let g1 = function `Tag1 _ -> "Tag1" | `Tag2 _ -> "Tag2";;
```

```h
val g1 : [< `Tag1 of 'a | `Tag2 of 'b ] -> string = <fun>
```

```h
# let g = function
```

```h
| #myvariant as x -> g1 x
```

```h
| `Tag3 -> "Tag3";;
```

```h
val g : [< `Tag1 of int | `Tag2 of bool | `Tag3 ] -> string = <fun>
```

## 5.3 Weaknesses of polymorphic variants

After seeing the power of polymorphic variants, one may wonder why they were added to core language variants, rather than replacing them.

The answer is twofold. The first aspect is that while being pretty efficient, the lack of static type information allows for less optimizations, and makes polymorphic variants slightly heavier than core language ones. However noticeable differences would only appear on huge data structures.

More important is the fact that polymorphic variants, while being type-safe, result in a weaker type discipline. That is, core language variants do actually much more than ensuring type-safety, they also check that you use only declared constructors, that all constructors present in a data-structure are compatible, and they enforce typing constraints to their parameters.

For this reason, you must be more careful about making types explicit when you use polymorphic variants. When you write a library, this is easy since you can describe exact types in interfaces, but for simple programs you are probably better off with core language variants.

Beware also that some idioms make trivial errors very hard to find. For instance, the following code is probably wrong but the compiler has no way to see it.

```h
# type abc = [ `A | `B | `C] ;;
```

```h
type abc = [ `A | `B | `C ]
```

```h
# let f = function
```

```h
| `As -> "A"
```

```h
| #abc -> "other" ;;
```

```h
val f : [< `A | `As | `B | `C ] -> string = <fun>
```

```h
# let f : abc -> string = f ;;
```

```h
val f : abc -> string = <fun>
```

You can avoid such risks by annotating the definition itself.

```h
# let f : abc -> string = function
```

```h
| `As -> "A"
```

```h
| #abc -> "other" ;;
```

```
Error: This pattern matches values of type [? `As ]
but a pattern was expected which matches values of type abc
The second variant type does not allow tag(s) `As
```
# Chapter 6

## Polymorphism and its limitations

This chapter covers more advanced questions related to the limitations of polymorphic functions and types. There are some situations in OCaml where the type inferred by the type checker may be less generic than expected. Such non-genericity can stem either from interactions between side-effects and typing or the difficulties of implicit polymorphic recursion and higher-rank polymorphism.

This chapter details each of these situations and, if it is possible, how to recover genericity.

### 6.1 Weak polymorphism and mutation

#### 6.1.1 Weakly polymorphic types

Maybe the most frequent examples of non-genericity derive from the interactions between polymorphic types and mutation. A simple example appears when typing the following expression

``` OCaml
# let store = ref None ;;
val store : '_weak1 option ref = {contents = None}
```

Since the type of `None` is `'a option` and the function `ref` has type `'b -> 'b ref`, a natural deduction for the type of `store` would be `'a option ref`. However, the inferred type, `'weak1 option ref'`, is different. Type variables whose names start with a `_weak` prefix like `'weak1` are weakly polymorphic type variables, sometimes shortened to "weak type variables". A weak type variable is a placeholder for a single type that is currently unknown. Once the specific type `t` behind the placeholder type `'weak1'` is known, all occurrences of `'weak1'` will be replaced by `t`. For instance, we can define another option reference and store an `int` inside:

``` OCaml
# let another_store = ref None ;;
val another_store : '_weak2 option ref = {contents = None}

# another_store := Some 0;
another_store ;;
- : int option ref = {contents = Some 0}
```

After storing an `int` inside `another_store`, the type of `another_store` has been updated from `'weak2 option ref` to `int option ref`. This distinction between weakly and generic polymorphic type variable protects OCaml programs from unsoundness and runtime errors. To understand from
# Chapter 6

## Polymorphism and its limitations

This chapter covers more advanced questions related to the limitations of polymorphic functions and types. There are some situations in OCaml where the type inferred by the type checker may be less generic than expected. Such non-genericity can stem either from interactions between side-effects and typing or the difficulties of implicit polymorphic recursion and higher-rank polymorphism.

This chapter details each of these situations and, if it is possible, how to recover genericity.

### 6.1 Weak polymorphism and mutation

#### 6.1.1 Weakly polymorphic types

Maybe the most frequent examples of non-genericity derive from the interactions between polymorphic types and mutation. A simple example appears when typing the following expression

``` OCaml
# let store = ref None ;;
val store : '_weak1 option ref = {contents = None}
```

Since the type of `None` is `'a option` and the function `ref` has type `'b -> 'b ref`, a natural deduction for the type of `store` would be `'a option ref`. However, the inferred type, `'weak1 option ref'`, is different. Type variables whose names start with a `_weak` prefix like `'weak1` are weakly polymorphic type variables, sometimes shortened to "weak type variables". A weak type variable is a placeholder for a single type that is currently unknown. Once the specific type `t` behind the placeholder type `'weak1'` is known, all occurrences of `'weak1'` will be replaced by `t`. For instance, we can define another option reference and store an `int` inside:

``` OCaml
# let another_store = ref None ;;
val another_store : '_weak2 option ref = {contents = None}

# another_store := Some 0;
another_store ;;
- : int option ref = {contents = Some 0}
```

After storing an `int` inside `another_store`, the type of `another_store` has been updated from `'weak2 option ref` to `int option ref`. This distinction between weakly and generic polymorphic type variable protects OCaml programs from unsoundness and runtime errors. To understand from
where unsoundness might come, consider this simple function which swaps a value `x` with the value stored inside a `store` reference, if there is such value:

```hkl
# let swap store x = match !store with
| None -> store := Some x; x
| Some y -> store := Some x; y;;
val swap : 'a option ref -> 'a -> 'a = <fun>
```

We can apply this function to our store

```hkl
# let one = swap store 1
let oneAgain = swap store 2
let two = swap store 3;;
val one : int = 1
val oneAgain : int = 1
val two : int = 2
```

After these three swaps the stored value is 3. Everything is fine up to now. We can then try to swap 3 with a more interesting value, for instance a function:

```hkl
# let error = swap store (fun x -> x);;
Error: This expression should not be a function, the expected type is int
```

At this point, the type checker rightfully complains that it is not possible to swap an integer and a function, and that an `int` should always be traded for another `int`. Furthermore, the type checker prevents us from manually changing the type of the value stored by `store`:

```hkl
# store := Some (fun x -> x);;
Error: This expression should not be a function, the expected type is int
```

Indeed, looking at the type of `store`, we see that the weak type `_weak1` has been replaced by the type `int`

```hkl
# store;;
- : int option ref = {contents = Some 3}
```

Therefore, after placing an `int` in `store`, we cannot use it to store any value other than an `int`. More generally, weak types protect the program from undue mutation of values with a polymorphic type.

Moreover, weak types cannot appear in the signature of toplevel modules: types must be known at compilation time. Otherwise, different compilation units could replace the weak type with different and incompatible types. For this reason, compiling the following small piece of code

```hkl
let option_ref = ref None
```

yields a compilation error

```hkl
Error: The type of this expression, '_weak1 option ref,
contains type variables that cannot be generalized
```

To solve this error, it is enough to add an explicit type annotation to specify the type at declaration time:
where unsoundness might come, consider this simple function which swaps a value `x` with the value stored inside a `store` reference, if there is such value:

```hkl
# let swap store x = match !store with
| None -> store := Some x; x
| Some y -> store := Some x; y;;
val swap : 'a option ref -> 'a -> 'a = <fun>
```

We can apply this function to our store

```hkl
# let one = swap store 1
let one_again = swap store 2
let two = swap store 3;;
val one : int = 1
val one_again : int = 1
val two : int = 2
```

After these three swaps the stored value is 3. Everything is fine up to now. We can then try to swap 3 with a more interesting value, for instance a function:

```hkl
# let error = swap store (fun x -> x);;
Error: This expression should not be a function, the expected type is int
```

At this point, the type checker rightfully complains that it is not possible to swap an integer and a function, and that an `int` should always be traded for another `int`. Furthermore, the type checker prevents us from manually changing the type of the value stored by `store`:

```hkl
# store := Some (fun x -> x);;
Error: This expression should not be a function, the expected type is int
```

Indeed, looking at the type of `store`, we see that the weak type `_weak1` has been replaced by the type `int`

```hkl
# store;;
- : int option ref = {contents = Some 3}
```

Therefore, after placing an `int` in `store`, we cannot use it to store any value other than an `int`. More generally, weak types protect the program from undue mutation of values with a polymorphic type.

Moreover, weak types cannot appear in the signature of toplevel modules: types must be known at compilation time. Otherwise, different compilation units could replace the weak type with different and incompatible types. For this reason, compiling the following small piece of code

```hkl
let option_ref = ref None
```

yields a compilation error

```hkl
Error: The type of this expression, '_weak1 option ref,
contains type variables that cannot be generalized
```

To solve this error, it is enough to add an explicit type annotation to specify the type at declaration time:
let option_ref: int option ref = ref None

This is in any case a good practice for such global mutable variables. Otherwise, they will pick
out the type of first use. If there is a mistake at this point, it can result in confusing type errors
when later, correct uses are flagged as errors.

6.1.2 The value restriction

Identifying the exact context in which polymorphic types should be replaced by weak types in
a modular way is a difficult question. Indeed the type system must handle the possibility that
functions may hide persistent mutable states. For instance, the following function uses an internal
reference to implement a delayed identity function

```h
# let make_fake_id () =
    let store = ref None in
    fun x -> swap store x ;;
val make_fake_id : unit -> 'a -> 'a = <fun>

# let fake_id = make_fake_id();;
val fake_id : '_weak3 -> '_weak3 = <fun>
```

It would be unsound to apply this `fake_id` function to values with different types. The function `fake_id` is therefore rightfully assigned the type `'_weak3 -> '_weak3` rather than `'a -> 'a`. At the same time, it ought to be possible to use a local mutable state without impacting the type of a function.

To circumvent these dual difficulties, the type checker considers that any value returned by a
function might rely on persistent mutable states behind the scene and should be given a weak type.
This restriction on the type of mutable values and the results of function application is called the
value restriction. Note that this value restriction is conservative: there are situations where the
value restriction is too cautious and gives a weak type to a value that could be safely generalized to
a polymorphic type:

```h
# let not_id = (fun x -> x) (fun x -> x);;
val not_id : '_weak4 -> '_weak4 = <fun>
```

Quite often, this happens when defining functions using higher order functions. To avoid this
problem, a solution is to add an explicit argument to the function:

```h
# let idAgain = fun x -> (fun x -> x) (fun x -> x) x;;
val idAgain : 'a -> 'a = <fun>
```

With this argument, `idAgain` is seen as a function definition by the type checker and can therefore
be generalized. This kind of manipulation is called eta-expansion in lambda calculus and is sometimes
referred under this name.

6.1.3 The relaxed value restriction

There is another partial solution to the problem of unnecessary weak types, which is implemented
directly within the type checker. Briefly, it is possible to prove that weak types that only appear as
type parameters in covariant positions –also called positive positions– can be safely generalized to
polymorphic types. For instance, the type `'a list` is covariant in `'a`:
let option_ref: int option ref = ref None

This is in any case a good practice for such global mutable variables. Otherwise, they will pick out the type of first use. If there is a mistake at this point, it can result in confusing type errors when later, correct uses are flagged as errors.

### 6.1.2 The value restriction

Identifying the exact context in which polymorphic types should be replaced by weak types in a modular way is a difficult question. Indeed the type system must handle the possibility that functions may hide persistent mutable states. For instance, the following function uses an internal reference to implement a delayed identity function

```h
# let make_fake_id () =
    let store = ref None in
    fun x -> swap store x ;;
val make_fake_id : unit -> 'a -> 'a = <fun>

# let fake_id = make_fake_id();;
val fake_id : '_weak3 -> '_weak3 = <fun>
```

It would be unsound to apply this `fake_id` function to values with different types. The function `fake_id` is therefore rightfully assigned the type `'_weak3 -> '_weak3` rather than `'a -> 'a`. At the same time, it ought to be possible to use a local mutable state without impacting the type of a function.

To circumvent these dual difficulties, the type checker considers that any value returned by a function might rely on persistent mutable states behind the scene and should be given a weak type. This restriction on the type of mutable values and the results of function application is called the value restriction. Note that this value restriction is conservative: there are situations where the value restriction is too cautious and gives a weak type to a value that could be safely generalized to a polymorphic type:

```h
# let not_id = (fun x -> x) (fun x -> x);;
val not_id : '_weak4 -> '_weak4 = <fun>
```

Quite often, this happens when defining functions using higher order functions. To avoid this problem, a solution is to add an explicit argument to the function:

```h
# let idAgain = fun x -> (fun x -> x) (fun x -> x) x;;
val idAgain : 'a -> 'a = <fun>
```

With this argument, `idAgain` is seen as a function definition by the type checker and can therefore be generalized. This kind of manipulation is called eta-expansion in lambda calculus and is sometimes referred under this name.

### 6.1.3 The relaxed value restriction

There is another partial solution to the problem of unnecessary weak types, which is implemented directly within the type checker. Briefly, it is possible to prove that weak types that only appear as type parameters in covariant positions –also called positive positions– can be safely generalized to polymorphic types. For instance, the type `'a list` is covariant in `'a`:
```h
# let f () = [];;
val f : unit -> 'a list = <fun>
```

```h
# let empty = f ();;
val empty : 'a list = []
```

Note that the type inferred for `empty` is `'a list` and not the `'_weak5 list'` that should have occurred with the value restriction.

The value restriction combined with this generalization for covariant type parameters is called the relaxed value restriction.

### 6.1.4 Variance and value restriction

Variance describes how type constructors behave with respect to subtyping. Consider for instance a pair of type `x` and `xy` with `x` a subtype of `xy`, denoted `x -> xy`:

```h
# type x = [ `X ];;
```
```
type x = [ `X ]
```

```h
# type xy = [ `X | `Y ];;
```
```
type xy = [ `X | `Y ]
```

As `x` is a subtype of `xy`, we can convert a value of type `x` to a value of type `xy`:

```h
# let x:x = `X;;
val x : x = `X
```

```h
# let x' = ( x :> xy );;
val x' : xy = `X
```

Similarly, if we have a value of type `x list`, we can convert it to a value of type `xy list`, since we could convert each element one by one:

```h
# let l:x list = [ `X; `X ];;
val l : x list = [ `X; `X ]
```

```h
# let l' = ( l :> xy list );;
val l' : xy list = [ `X; `X ]
```

In other words, `x :> xy` implies that `x list :> xy list`, therefore the type constructor `'a list'` is covariant (it preserves subtyping) in its parameter `'a'.

Contrarily, if we have a function that can handle values of type `xy`

```h
# let f: xy -> unit = function
| `X -> ()
| `Y -> ();;
val f : xy -> unit = <fun>
```

it can also handle values of type `x`:

```h
# let f' = (f :> x -> unit);;
val f' : x -> unit = <fun>
```
```h
# let f () = [];;
val f : unit -> 'a list = <fun>
```

```h
# let empty = f ();;
val empty : 'a list = []
```

Note that the type inferred for `empty` is `'a list` and not the `'_weak5 list'` that should have occurred with the value restriction.

The value restriction combined with this generalization for covariant type parameters is called the relaxed value restriction.

### 6.1.4 Variance and value restriction

Variance describes how type constructors behave with respect to subtyping. Consider for instance a pair of type `x` and `xy` with `x` a subtype of `xy`, denoted `x -> xy`:

```h
# type x = [ `X ];;
type x = [ `X ]
```

```h
# type xy = [ `X | `Y ];;
type xy = [ `X | `Y ]
```

As `x` is a subtype of `xy`, we can convert a value of type `x` to a value of type `xy`:

```h
# let x:x = `X;;
val x : x = `X
```

```h
# let x' = ( x :> xy );;
val x' : xy = `X
```

Similarly, if we have a value of type `x list`, we can convert it to a value of type `xy list`, since we could convert each element one by one:

```h
# let l:x list = [ `X; `X ];;
val l : x list = [ `X; `X ]
```

```h
# let l' = ( l :> xy list );;
val l' : xy list = [ `X; `X ]
```

In other words, `x :> xy` implies that `x list :> xy list`, therefore the type constructor `'a list'` is covariant (it preserves subtyping) in its parameter `'a`.

Contrarily, if we have a function that can handle values of type `xy`

```h
# let f: xy -> unit = function
| `X -> ()
| `Y -> ();;
val f : xy -> unit = <fun>
```

it can also handle values of type `x`:

```h
# let f' = (f :> x -> unit);;
val f' : x -> unit = <fun>
```
Note that we can rewrite the type of `f` and `f'` as

```h
# type 'a proc = 'a -> unit
let f' = (f: xy proc :> x proc);;
type 'a proc = 'a -> unit
val f' : x proc = <fun>
```

In this case, we have `x :> xy` implies `xy proc :> x proc`. Notice that the second subtyping relation reverse the order of `x` and `xy`: the type constructor `'a proc` is contravariant in its parameter `'a`. More generally, the function type constructor `'a -> 'b` is covariant in its return type `'b` and contravariant in its argument type `'a`.

A type constructor can also be invariant in some of its type parameters, neither covariant nor contravariant. A typical example is a reference:

```h
# let x: x ref = ref `X;;
val x : x ref = {contents = `X}
```

If we were able to coerce `x` to the type `xy ref` as a variable `xy`, we could use `xy` to store the value `Y` inside the reference and then use the `x` value to read this content as a value of type `x`, which would break the type system.

More generally, as soon as a type variable appears in a position describing mutable state it becomes invariant. As a corollary, covariant variables will never denote mutable locations and can be safely generalized. For a better description, interested readers can consult the original article by Jacques Garrigue on http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf

Together, the relaxed value restriction and type parameter covariance help to avoid eta-expansion in many situations.

### 6.1.5 Abstract data types

Moreover, when the type definitions are exposed, the type checker is able to infer variance information on its own and one can benefit from the relaxed value restriction even unknowingly. However, this is not the case anymore when defining new abstract types. As an illustration, we can define a module type collection as:

```h
# module type COLLECTION = sig
  type 'a t
  val empty: unit -> 'a t
end

module Implementation = struct
  type 'a t = 'a list
  let empty ()= []
end;;

module type COLLECTION = sig type 'a t val empty : unit -> 'a t end
module Implementation :
  sig type 'a t = 'a list val empty : unit -> 'a list end
```

```h
# module List2: COLLECTION = Implementation;;
module List2 : COLLECTION
```
Note that we can rewrite the type of `f` and `f'` as

```h
# type 'a proc = 'a -> unit
let f' = (f: xy proc :> x proc);;
type 'a proc = 'a -> unit
val f' : x proc = <fun>
```

In this case, we have `x -> xy` implies `xy proc :> x proc`. Notice that the second subtyping relation reverse the order of `x` and `xy`: the type constructor `'a proc` is contravariant in its parameter `'a`. More generally, the function type constructor `'a -> 'b` is covariant in its return type `'b` and contravariant in its argument type `'a`.

A type constructor can also be invariant in some of its type parameters, neither covariant nor contravariant. A typical example is a reference:

```h
# let x: x ref = ref `X;;
val x : x ref = {contents = `X}
```

If we were able to coerce `x` to the type `xy ref` as a variable `xy`, we could use `xy` to store the value `Y` inside the reference and then use the `x` value to read this content as a value of type `x`, which would break the type system.

More generally, as soon as a type variable appears in a position describing mutable state it becomes invariant. As a corollary, covariant variables will never denote mutable locations and can be safely generalized. For a better description, interested readers can consult the original article by Jacques Garrigue on http://www.math.nagoya-u.ac.jp/~garrigue/papers/morepoly-long.pdf

Together, the relaxed value restriction and type parameter covariance help to avoid eta-expansion in many situations.

### 6.1.5 Abstract data types

Moreover, when the type definitions are exposed, the type checker is able to infer variance information on its own and one can benefit from the relaxed value restriction even unknowingly. However, this is not the case anymore when defining new abstract types. As an illustration, we can define a module type collection as:

```h
# module type COLLECTION = sig
  type 'a t
  val empty: unit -> 'a t
end

module Implementation = struct
  type 'a t = 'a list
  let empty () = []
end;;

module type COLLECTION = sig type 'a t val empty : unit -> 'a t end
module Implementation :
  sig type 'a t = 'a list val empty : unit -> 'a list end
```

```h
# module List2: COLLECTION = Implementation;;
module List2 : COLLECTION
```
In this situation, when coercing the module `List2` to the module type `COLLECTION`, the type checker forgets that `'a List2.t` was covariant in `'a`. Consequently, the relaxed value restriction does not apply anymore:

```hkl
# List2.empty();
- : '_weak5 List2.t = <abstr>
```

To keep the relaxed value restriction, we need to declare the abstract type `'a COLLECTION.t` as covariant in `'a`:

```hkl
# module type COLLECTION = sig
    type + 'a t
    val empty: unit -> 'a t
end

module List2: COLLECTION = Implementation;;
module type COLLECTION = sig type + 'a t val empty : unit -> 'a t end
module List2 : COLLECTION
```

We then recover polymorphism:

```hkl
# List2.empty();
- : 'a List2.t = <abstr>
```

## 6.2 Polymorphic recursion

The second major class of non-genericity is directly related to the problem of type inference for polymorphic functions. In some circumstances, the type inferred by OCaml might be not general enough to allow the definition of some recursive functions, in particular for recursive functions acting on non-regular algebraic data types.

With a regular polymorphic algebraic data type, the type parameters of the type constructor are constant within the definition of the type. For instance, we can look at arbitrarily nested list defined as:

```hkl
# type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list
let l = Nested[ List [1]; Nested [List[2;3]]; Nested[Nested[]] ];
type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list
val l : int regular_nested = Nested [List [1]; Nested [List [2; 3]]; Nested [Nested []]]
```

Note that the type constructor `regular_nested` always appears as `'a regular_nested` in the definition above, with the same parameter `'a`. Equipped with this type, one can compute a maximal depth with a classic recursive function

```hkl
# let rec maximal_depth = function
  | List _ -> 1
  | Nested [] -> 0
  | Nested (a::q) -> 1 + max (maximal_depth a) (maximal_depth (Nested q));
val maximal_depth : 'a regular_nested -> int = <fun>
```
In this situation, when coercing the module `List2` to the module type `COLLECTION`, the type checker forgets that `'a List2.t` was covariant in `'a`. Consequently, the relaxed value restriction does not apply anymore:

```hhl
# List2.empty();
- : '_weak5 List2.t = <abstr>
```

To keep the relaxed value restriction, we need to declare the abstract type `'a COLLECTION.t` as covariant in `'a`:

```hhl
# module type COLLECTION = sig
  type + 'a t
  val empty: unit -> 'a t
end

module List2: COLLECTION = Implementation;;
module type COLLECTION = sig type + 'a t val empty : unit -> 'a t end
module List2 : COLLECTION
```

We then recover polymorphism:

```hhl
# List2.empty();
- : 'a List2.t = <abstr>
```

## 6.2 Polymorphic recursion

The second major class of non-genericity is directly related to the problem of type inference for polymorphic functions. In some circumstances, the type inferred by OCaml might be not general enough to allow the definition of some recursive functions, in particular for recursive functions acting on non-regular algebraic data types.

With a regular polymorphic algebraic data type, the type parameters of the type constructor are constant within the definition of the type. For instance, we can look at arbitrarily nested list defined as:

```hhl
# type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list;;
type 'a regular_nested = List of 'a list | Nested of 'a regular_nested list

# let l = Nested[ List [1]; Nested [List[2;3]]; Nested[Nested[]] ];;
val l : int regular_nested =
    Nested [List [1]; Nested [List [2; 3]]; Nested [Nested []]]
```

Note that the type constructor `regular_nested` always appears as `'a regular_nested` in the definition above, with the same parameter `'a`. Equipped with this type, one can compute a depth with a classic recursive function

```hhl
# let rec regular_depth = function
  | List _ -> 1
  | Nested n -> 1 + List.fold_left max 1 (List.map regular_depth n);;
val regular_depth : 'a regular_nested -> int = <fun>
```
Non-regular recursive algebraic data types correspond to polymorphic algebraic data types whose
parameter types vary between the left and right side of the type definition. For instance, it might
be interesting to define a datatype that ensures that all lists are nested at the same depth:

```hkl
# type 'a nested = List of 'a list | Nested of 'a list nested;;
```

```hkl
type 'a nested = List of 'a list | Nested of 'a list nested
```

Intuitively, a value of type `'a nested` is a list of list ... of list of elements `a` with `k` nested list. We can then adapt the `maximal_depth` function defined on `regular_depth` into a `depth` function that computes this `k`. As a first try, we may define

```hkl
# let rec depth = function
```

```hkl
| List _ -> 1
```

```hkl
| Nested n -> 1 + depth n;;
```

```
Error: This expression has type 'a list nested
but an expression was expected of type 'a nested
The type variable 'a occurs inside 'a list
```

The type error here comes from the fact that during the definition of `depth`, the type checker first assigns to `depth` the type `'a -> 'b`. When typing the pattern matching, `'a -> 'b` becomes `'a nested -> 'b`, then `'a nested -> int` once the `List` branch is typed. However, when typing the application `depth n` in the `Nested` branch, the type checker encounters a problem: `depth n` is applied to `'a list nested`, it must therefore have the type `'a list nested -> 'b`. Unifying this constraint with the previous one leads to the impossible constraint `'a list nested = 'a nested'`. In other words, within its definition, the recursive function `depth` is applied to values of type `'a t` with different types `'a` due to the non-regularity of the type constructor `nested`. This creates a problem because the type checker had introduced a new type variable `'a` only at the *definition* of the function `depth` whereas, here, we need a different type variable for every *application* of the function `depth`.

### 6.2.1 Explicitly polymorphic annotations

The solution of this conundrum is to use an explicitly polymorphic type annotation for the type `'a`:

```hkl
# let rec depth: 'a. 'a nested -> int = function
```

```hkl
| List _ -> 1
```

```hkl
| Nested n -> 1 + depth n;;
```

```hkl
val depth : 'a nested -> int = <fun>
```

```hkl
# depth ( Nested(List [ [7]; [8] ])) ;;
```

```hkl
- : int = 2
```

In the type of `depth`, `'a. 'a nested -> int`, the type variable `'a` is universally quantified. In other words, `'a. 'a nested -> int` reads as "for all type `'a`, `depth` maps `'a nested` values to integers". Whereas the standard type `'a nested -> int` can be interpreted as "let be a type variable `'a`, then `depth` maps `'a nested` values to integers". There are two major differences with these two type expressions. First, the explicit polymorphic annotation indicates to the type checker that it
Non-regular recursive algebraic data types correspond to polymorphic algebraic data types whose parameter types vary between the left and right side of the type definition. For instance, it might be interesting to define a datatype that ensures that all lists are nested at the same depth:

```hkl
# type 'a nested = List of 'a list | Nested of 'a list nested;;
```

```hkl
type 'a nested = List of 'a list | Nested of 'a list nested
```

Intuitively, a value of type `'a nested` is a list of list ...of list of elements `a` with `k` nested list. We can then adapt the `regular_depth` function defined on `regular_nested` into a `depth` function that computes this `k`. As a first try, we may define

```hkl
# let rec depth = function
```

```hkl
| List _ -> 1
```

```hkl
| Nested n -> 1 + depth n;;
```

```
Error: The value n has type 'a list nested
but an expression was expected of type 'a nested
The type variable 'a occurs inside 'a list
```

The type error here comes from the fact that during the definition of `depth`, the type checker first assigns to `depth` the type `'a -> 'b'`. When typing the pattern matching, `'a -> 'b` becomes `'a nested -> 'b`, then `'a nested -> int` once the `List` branch is typed. However, when typing the application `depth n` in the `Nested` branch, the type checker encounters a problem: `depth n` is applied to `'a list nested`, it must therefore have the type `'a list nested -> 'b'`. Unifying this constraint with the previous one leads to the impossible constraint `'a list nested = 'a nested'`. In other words, within its definition, the recursive function `depth` is applied to values of type `'a t` with different types `'a` due to the non-regularity of the type constructor `nested`. This creates a problem because the type checker had introduced a new type variable `'a` only at the *definition* of the function `depth` whereas, here, we need a different type variable for every *application* of the function `depth`.

### 6.2.1 Explicitly polymorphic annotations

The solution of this conundrum is to use an explicitly polymorphic type annotation for the type `'a`:

```hkl
# let rec depth: 'a. 'a nested -> int = function
```

```hkl
| List _ -> 1
```

```hkl
| Nested n -> 1 + depth n;;
```

```hkl
val depth : 'a nested -> int = <fun>
```

```hkl
# depth ( Nested(List [ [7]; [8] ]) );;
```

```hkl
- : int = 2
```

In the type of `depth`, `'a.' 'a nested -> int`, the type variable `'a` is universally quantified. In other words, `'a.' 'a nested -> int` reads as "for all type `'a`, `depth` maps `'a nested` values to integers". Whereas the standard type `'a nested -> int` can be interpreted as "let be a type variable `'a`, then `depth` maps `'a nested` values to integers". There are two major differences with these two type expressions. First, the explicit polymorphic annotation indicates to the type checker that it
needs to introduce a new type variable every time the function `depth` is applied. This solves our problem with the definition of the function `depth`.

Second, it also notifies the type checker that the type of the function should be polymorphic. Indeed, without explicit polymorphic type annotation, the following type annotation is perfectly valid

```hkl
# let sum: 'a -> 'b -> 'c = fun x y -> x + y;;
val sum : int -> int -> int = <fun>
```

since `'a'` and `'b'` and `'c'` denote type variables that may or may not be polymorphic. Whereas, it is an error to unify an explicitly polymorphic type with a non-polymorphic type:

```hkl
# let sum: 'a 'b 'c. 'a -> 'b -> 'c = fun x y -> x + y;;
Error: This definition has type int -> int -> int which is less general than
        'a 'b 'c. 'a -> 'b -> 'c
```

An important remark here is that it is not needed to explicit fully the type of `depth`: it is sufficient to add annotations only for the universally quantified type variables:

```hkl
# let rec depth: 'a. 'a nested -> _ = function
| List _ -> 1
| Nested n -> 1 + depth n;;
val depth : 'a nested -> int = <fun>
```

```hkl
# depth (Nested(List [ [7]; [8] ]));
- : int = 2
```

### 6.2.2 More examples

With explicit polymorphic annotations, it becomes possible to implement any recursive function that depends only on the structure of the nested lists and not on the type of the elements. For instance, a more complex example would be to compute the total number of elements of the nested lists:

```hkl
# let len nested =
  let map_and_sum f = List.fold_left (fun acc x -> acc + f x) 0 in
  let rec len: 'a. ('a list -> int ) -> 'a nested -> int =
    fun nested_len n ->
      match n with
      | List l -> nested_len l
      | Nested n -> len (map_and_sum nested_len) n
      in
    len List.length nested;;
val len : 'a nested -> int = <fun>
```

```hkl
# len (Nested(Nested(List [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ))));
- : int = 7
```

Similarly, it may be necessary to use more than one explicitly polymorphic type variables, like for computing the nested list of list lengths of the nested list:
needs to introduce a new type variable every time the function `depth` is applied. This solves our problem with the definition of the function `depth`.

Second, it also notifies the type checker that the type of the function should be polymorphic. Indeed, without explicit polymorphic type annotation, the following type annotation is perfectly valid

```hkl
# let sum: 'a -> 'b -> 'c = fun x y -> x + y;;
val sum : int -> int -> int = <fun>
```

since `'a'` and `'b'` and `'c'` denote type variables that may or may not be polymorphic. Whereas, it is an error to unify an explicitly polymorphic type with a non-polymorphic type:

```hkl
# let sum: 'a 'b 'c. 'a -> 'b -> 'c = fun x y -> x + y;;
Error: This definition has type int -> int -> int which is less general than
       'a 'b 'c. 'a -> 'b -> 'c
```

An important remark here is that it is not needed to explicit fully the type of `depth`: it is sufficient to add annotations only for the universally quantified type variables:

```hkl
# let rec depth: 'a. 'a nested -> _ = function
| List _ -> 1
| Nested n -> 1 + depth n;;
val depth : 'a nested -> int = <fun>
```

```hkl
# depth (Nested(List [ [7]; [8] ]));
- : int = 2
```

### 6.2.2 More examples

With explicit polymorphic annotations, it becomes possible to implement any recursive function that depends only on the structure of the nested lists and not on the type of the elements. For instance, a more complex example would be to compute the total number of elements of the nested lists:

```hkl
# let len nested =
  let map_and_sum f = List.fold_left (fun acc x -> acc + f x) 0 in
  let rec len: 'a. ('a list -> int ) -> 'a nested -> int =
    fun nested_len n ->
      match n with
      | List l -> nested_len l
      | Nested n -> len (map_and_sum nested_len) n
      in
    len List.length nested;;
val len : 'a nested -> int = <fun>

# len (Nested(Nested(List [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ))));
- : int = 7
```

Similarly, it may be necessary to use more than one explicitly polymorphic type variables, like for computing the nested list of list lengths of the nested list:
```h
# let shape n =
    let rec shape: 'a 'b. ('a nested -> int nested) ->
        ('b list list -> 'a list) -> 'b nested -> int nested
    = fun nest nestedShape ->
        function
        | List l -> raise
          (Invalid_argument "shape requires nested_list of depth greater than 1")
        | Nested (List l) -> nest @@ List (nestedShape l)
        | Nested n ->
            let nestedShape = List.map nestedShape in
            let nest x = nest (Nested x) in
            shape nest nestedShape n in
        shape (fun n -> n) (fun l -> List.map List.length l ) n;;
val shape : 'a nested -> int nested = <fun>
```

```h
# shape (Nested(Nested(List [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ))));
- : int nested = Nested (List [[2; 1]; [0; 1; 3]; [0]])
```

## 6.3 Higher-rank polymorphic functions

Explicit polymorphic annotations are however not sufficient to cover all the cases where the inferred type of a function is less general than expected. A similar problem arises when using polymorphic functions as arguments of higher-order functions. For instance, we may want to compute the average depth or length of two nested lists:

```h
# let average_depth x y = (depth x + depth y) / 2;;
val average_depth : 'a nested -> 'b nested -> int = <fun>
```

```h
# let average_len x y = (len x + len y) / 2;;
val average_len : 'a nested -> 'b nested -> int = <fun>
```

```h
# let one = average_len (List [2]) (List [[]]);;
val one : int = 1
```

It would be natural to factorize these two definitions as:

```h
# let average f x y = (f x + f y) / 2;;
val average : ('a -> int) -> 'a -> 'a -> int = <fun>
```

However, the type of `average_len` is less generic than the type of `average_len`, since it requires the type of the first and second argument to be the same:

```h
# average_len (List [2]) (List [[]]);;
- : int = 1
```

```h
# average len (List [2]) (List [[]]);;
```

```
Error: This expression has type 'a list
but an expression was expected of type int
```
```h
# let shape n =
    let rec shape: 'a 'b. ('a nested -> int nested) ->
        ('b list list -> 'a list) -> 'b nested -> int nested
    = fun nest nestedShape ->
        function
        | List l -> raise
          (Invalid_argument "shape requires nested_list of depth greater than 1")
        | Nested (List l) -> nest @@ List (nestedShape l)
        | Nested n ->
            let nestedShape = List.map nestedShape in
            let nest x = nest (Nested x) in
            shape nest nestedShape n in
        shape (fun n -> n) (fun l -> List.map List.length l ) n;;

val shape : 'a nested -> int nested = <fun>
```

```h
# shape (Nested(Nested(List [ [1;2]; [3] ]; [ []; [4]; [5;6;7]]; [[]] ))));
- : int nested = Nested (List [[2; 1]; [0; 1; 3]; [0]])
```

## 6.3 Higher-rank polymorphic functions

Explicit polymorphic annotations are however not sufficient to cover all the cases where the inferred type of a function is less general than expected. A similar problem arises when using polymorphic functions as arguments of higher-order functions. For instance, we may want to compute the average depth or length of two nested lists:

```h
# let average_depth x y = (depth x + depth y) / 2;;
val average_depth : 'a nested -> 'b nested -> int = <fun>
```

```h
# let average_len x y = (len x + len y) / 2;;
val average_len : 'a nested -> 'b nested -> int = <fun>
```

```h
# let one = average_len (List [2]) (List [[]]);;
val one : int = 1
```

It would be natural to factorize these two definitions as:

```h
# let average f x y = (f x + f y) / 2;;
val average : ('a -> int) -> 'a -> 'a -> int = <fun>
```

However, the type of `average_len` is less generic than the type of `average_len`, since it requires the type of the first and second argument to be the same:

```h
# average_len (List [2]) (List [[]]);;
- : int = 1
```

```h
# average len (List [2]) (List [[]]);;
```

```
Error: The constructor [] has type 'a list
but an expression was expected of type int
```
As previously with polymorphic recursion, the problem stems from the fact that type variables are introduced only at the start of the `let` definitions. When we compute both `f x` and `f y`, the type of `x` and `y` are unified together. To avoid this unification, we need to indicate to the type checker that `f` is polymorphic in its first argument. In some sense, we would want `average` to have type

```hkl
val average: ('a. 'a nested -> int) -> 'a nested -> 'b nested -> int
```

Note that this syntax is not valid within OCaml: `average` has an universally quantified type `'a` inside the type of one of its argument whereas for polymorphic recursion the universally quantified type was introduced before the rest of the type. This position of the universally quantified type means that `average` is a second-rank polymorphic function. This kind of higher-rank functions is not directly supported by OCaml: type inference for second-rank polymorphic function and beyond is undecidable; therefore using this kind of higher-rank functions requires to handle manually these universally quantified types.

In OCaml, there are two ways to introduce this kind of explicit universally quantified types: universally quantified record fields,

```hkl
# type 'a nested_reduction = { f:'elt. 'elt nested -> 'a };;
type 'a nested_reduction = { f : 'elt. 'elt nested -> 'a; }
```

```hkl
# let boxed_len = { f = len };;
val boxed_len : int nested_reduction = {f = <fun>}
```

and universally quantified object methods:

```hkl
# let obj_len = object method f:'a. 'a nested -> 'b = len end;;
val obj_len : <f : 'a. 'a nested -> int > = <obj>
```

To solve our problem, we can therefore use either the record solution:

```hkl
# let average nsm x y = (nsm.f x + nsm.f y) / 2 ;;
val average : int nested_reduction -> 'a nested -> 'b nested -> int = <fun>
```

or the object one:

```hkl
# let average (obj:<f:'a. 'a nested -> _ > ) x y = (obj#f x + obj#f y) / 2 ;;
val average : <f : 'a. 'a nested -> int > -> 'b nested -> 'c nested -> int =
<fun>
```
As previously with polymorphic recursion, the problem stems from the fact that type variables
are introduced only at the start of the `let` definitions. When we compute both `f x` and `f y`, the
type of `x` and `y` are unified together. To avoid this unification, we need to indicate to the type
checker that `f` is polymorphic in its first argument. In some sense, we would want `average` to have
type

```hkl
val average: ('a. 'a nested -> int) -> 'a nested -> 'b nested -> int
```

Note that this syntax is not valid within OCaml: `average` has an universally quantified type `'a` inside the type of one of its argument whereas for polymorphic recursion the universally quantified type was introduced before the rest of the type. This position of the universally quantified type means that `average` is a second-rank polymorphic function. This kind of higher-rank functions is not directly supported by OCaml: type inference for second-rank polymorphic function and beyond is undecidable; therefore using this kind of higher-rank functions requires to handle manually these universally quantified types.

In OCaml, there are two ways to introduce this kind of explicit universally quantified types: universally quantified record fields,

```hkl
# type 'a nested_reduction = { f:'elt. 'elt nested -> 'a };;
type 'a nested_reduction = { f : 'elt. 'elt nested -> 'a; }
```

```hkl
# let boxed_len = { f = len };;
val boxed_len : int nested_reduction = {f = <fun>}
```

and universally quantified object methods:

```hkl
# let obj_len = object method f:'a. 'a nested -> 'b = len end;;
val obj_len : <f : 'a. 'a nested -> int > = <obj>
```

To solve our problem, we can therefore use either the record solution:

```hkl
# let average nsm x y = (nsm.f x + nsm.f y) / 2 ;;
val average : int nested_reduction -> 'a nested -> 'b nested -> int = <fun>
```

or the object one:

```hkl
# let average (obj:<f:'a. 'a nested -> _ > ) x y = (obj#f x + obj#f y) / 2 ;;
val average : <f : 'a. 'a nested -> int > -> 'b nested -> 'c nested -> int =
<fun>
```
# Chapter 7

## Generalized algebraic datatypes

Generalized algebraic datatypes, or GADTs, extend usual sum types in two ways: constraints on type parameters may change depending on the value constructor, and some type variables may be existentially quantified. Adding constraints is done by giving an explicit return type, where type parameters are instantiated:

```h
type _ term =
| Int : int -> int term
| Add : (int -> int -> int) term
| App : ('b -> 'a) term * 'b term -> 'a term
```

This return type must use the same type constructor as the type being defined, and have the same number of parameters. Variables are made existential when they appear inside a constructor's argument, but not in its return type. Since the use of a return type often eliminates the need to name type parameters in the left-hand side of a type definition, one can replace them with anonymous types _ in that case.

The constraints associated to each constructor can be recovered through pattern-matching. Namely, if the type of the scrutinee of a pattern-matching contains a locally abstract type, this type can be refined according to the constructor used. These extra constraints are only valid inside the corresponding branch of the pattern-matching. If a constructor has some existential variables, fresh locally abstract types are generated, and they must not escape the scope of this branch.

### 7.1 Recursive functions

We write an `eval` function:

```h
let rec eval : type a. a term -> a = function
| Int n      -> n          (* a = int *)
| Add       -> (fun x y -> x+y) (* a = int -> int -> int *)
| App(f,x)  -> (eval f) (eval x)

(* eval called at types (b->a) and b for fresh b *)
```

And use it:

```h
let two = eval (App (App (Add, Int 1), Int 1))
val two : int = 2
```
# Chapter 7

## Generalized algebraic datatypes

Generalized algebraic datatypes, or GADTs, extend usual sum types in two ways: constraints on type parameters may change depending on the value constructor, and some type variables may be existentially quantified. Adding constraints is done by giving an explicit return type, where type parameters are instantiated:

```h
type _ term =
| Int : int -> int term
| Add : (int -> int -> int) term
| App : ('b -> 'a) term * 'b term -> 'a term
```

This return type must use the same type constructor as the type being defined, and have the same number of parameters. Variables are made existential when they appear inside a constructor's argument, but not in its return type. Since the use of a return type often eliminates the need to name type parameters in the left-hand side of a type definition, one can replace them with anonymous types _ in that case.

The constraints associated to each constructor can be recovered through pattern-matching. Namely, if the type of the scrutinee of a pattern-matching contains a locally abstract type, this type can be refined according to the constructor used. These extra constraints are only valid inside the corresponding branch of the pattern-matching. If a constructor has some existential variables, fresh locally abstract types are generated, and they must not escape the scope of this branch.

### 7.1 Recursive functions

We write an eval function:

```h
let rec eval : type a. a term -> a = function
| Int n -> n (* a = int *)
| Add -> (fun x y -> x+y) (* a = int -> int -> int *)
| App(f,x) -> (eval f) (eval x)
(* eval called at types (b->a) and b for fresh b *)
```

And use it:

```h
let two = eval (App (App (Add, Int 1), Int 1))
val two : int = 2
```
It is important to remark that the function `eval` is using the polymorphic syntax for locally abstract types. When defining a recursive function that manipulates a GADT, explicit polymorphic recursion should generally be used. For instance, the following definition fails with a type error:

```haskell
let rec eval (type a) : a term -> a = function
| Int n      -> n
| Add       -> (fun x y -> x+y)
| App(f,x)  -> (eval f) (eval x)
```

```
Error: This expression has type ($App_'b -> a) term
but an expression was expected of type 'a
The type constructor $App_'b would escape its scope
```

In absence of an explicit polymorphic annotation, a monomorphic type is inferred for the recursive function. If a recursive call occurs inside the function definition at a type that involves an existential GADT type variable, this variable flows to the type of the recursive function, and thus escapes its scope. In the above example, this happens in the branch `App(f,x)` when `eval` is called with `f` as an argument. In this branch, the type of `f` is `($App_'b -> a) term`. The prefix `$` in `$App_'b` denotes an existential type named by the compiler (see 7.5). Since the type of `eval` is `'a term -> 'a`, the call `eval f` makes the existential type `$App_'b` flow to the type variable `'a` and escape its scope. This triggers the above error.

## 7.2 Type inference

Type inference for GADTs is notoriously hard. This is due to the fact some types may become ambiguous when escaping from a branch. For instance, in the `Int` case above, `n` could have either type `int` or `a`, and they are not equivalent outside of that branch. As a first approximation, type inference will always work if a pattern-matching is annotated with types containing no free type variables (both on the scrutinee and the return type). This is the case in the above example, thanks to the type annotation containing only locally abstract types.

In practice, type inference is a bit more clever than that: type annotations do not need to be immediately on the pattern-matching, and the types do not have to be always closed. As a result, it is usually enough to only annotate functions, as in the example above. Type annotations are propagated in two ways: for the scrutinee, they follow the flow of type inference, in a way similar to polymorphic methods; for the return type, they follow the structure of the program, they are split on functions, propagated to all branches of a pattern matching, and go through tuples, records, and sum types. Moreover, the notion of ambiguity used is stronger: a type is only seen as ambiguous if it was mixed with incompatible types (equated by constraints), without type annotations between them. For instance, the following program types correctly.

```haskell
let rec sum : type a. a term -> _ = fun x ->
let y =
  match x with
  | Int n -> n
  | Add -> 0
  | App(f,x) -> sum f + sum x
  in y + 1
```
It is important to remark that the function `eval` is using the polymorphic syntax for locally abstract types. When defining a recursive function that manipulates a GADT, explicit polymorphic recursion should generally be used. For instance, the following definition fails with a type error:

```haskell
let rec eval (type a) : a term -> a = function
| Int n      -> n
| Add       -> (fun x y -> x+y)
| App(f,x)  -> (eval f) (eval x)
```

```
Error: The value f has type ($b -> a) term
but an expression was expected of type 'a
The type constructor $b would escape its scope
Hint: $b is an existential type bound by the constructor App.
```

In absence of an explicit polymorphic annotation, a monomorphic type is inferred for the recursive function. If a recursive call occurs inside the function definition at a type that involves an existential GADT type variable, this variable flows to the type of the recursive function, and thus escapes its scope. In the above example, this happens in the branch `App(f,x)` when `eval` is called with `f` as an argument. In this branch, the type of `f` is `($App_'b -> a)` term. The prefix `$` in `$App_'b`` denotes an existential type named by the compiler (see 7.5). Since the type of `eval` is `'a` term -> `'a`, the call `eval f` makes the existential type `$App_'b` flow to the type variable `'a` and escape its scope. This triggers the above error.

## 7.2 Type inference

Type inference for GADTs is notoriously hard. This is due to the fact some types may become ambiguous when escaping from a branch. For instance, in the `Int` case above, `n` could have either type `int` or `a`, and they are not equivalent outside of that branch. As a first approximation, type inference will always work if a pattern-matching is annotated with types containing no free type variables (both on the scrutinee and the return type). This is the case in the above example, thanks to the type annotation containing only locally abstract types.

In practice, type inference is a bit more clever than that: type annotations do not need to be immediately on the pattern-matching, and the types do not have to be always closed. As a result, it is usually enough to only annotate functions, as in the example above. Type annotations are propagated in two ways: for the scrutinee, they follow the flow of type inference, in a way similar to polymorphic methods; for the return type, they follow the structure of the program, they are split on functions, propagated to all branches of a pattern matching, and go through tuples, records, and sum types. Moreover, the notion of ambiguity used is stronger: a type is only seen as ambiguous if it was mixed with incompatible types (equated by constraints), without type annotations between them. For instance, the following program types correctly.

```haskell
let rec sum : type a. a term -> _ = fun x ->
let y =
  match x with
  | Int n -> n
  | Add   -> 0
  | App(f,x) -> sum f + sum x
  in y + 1
```
```h
val sum : 'a term -> int = <fun>
```

Here the return type `int` is never mixed with `a`, so it is seen as non-ambiguous, and can be inferred. When using such partial type annotations we strongly suggest specifying the `-principal` mode, to check that inference is principal.

The exhaustiveness check is aware of GADT constraints, and can automatically infer that some cases cannot happen. For instance, the following pattern matching is correctly seen as exhaustive (the `Add` case cannot happen).

```h
let get_int : int term -> int = function
| Int n      -> n
| App(..., ...) -> 0
```

## 7.3 Refutation cases

Usually, the exhaustiveness check only tries to check whether the cases omitted from the pattern matching are typable or not. However, you can force it to try harder by adding *refutation cases*, written as a full stop. In the presence of a refutation case, the exhaustiveness check will first compute the intersection of the pattern with the complement of the cases preceding it. It then checks whether the resulting patterns can really match any concrete values by trying to type-check them. Wild cards in the generated patterns are handled in a special way: if their type is a variant type with only GADT constructors, then the pattern is split into the different constructors, in order to check whether any of them is possible (this splitting is not done for arguments of these constructors, to avoid non-termination). We also split tuples and variant types with only one case, since they may contain GADTs inside. For instance, the following code is deemed exhaustive:

```h
type _ t =
| Int : int t
| Bool : bool t
```

```h
let deep : (char t * int) option -> char = function
| None -> 'c'
| _ ->
```

Namely, the inferred remaining case is `Some _`, which is split into `Some (Int, _)` and `Some (Bool, _)`), which are both untypable because `deep` expects a non-existing `char t` as the first element of the tuple. Note that the refutation case could be omitted here, because it is automatically added when there is only one case in the pattern matching.

Another addition is that the redundancy check is now aware of GADTs: a case will be detected as redundant if it could be replaced by a refutation case using the same pattern.

## 7.4 Advanced examples

The `term` type we have defined above is an *indexed type*, where a type parameter reflects a property of the value contents. Another use of GADTs is *singleton types*, where a GADT value represents exactly one type. This value can be used as runtime representation for this type, and a function receiving it can have a polytypic behavior.
```h
val sum : 'a term -> int = <fun>
```

Here the return type `int` is never mixed with `a`, so it is seen as non-ambiguous, and can be inferred. When using such partial type annotations we strongly suggest specifying the `-principal` mode, to check that inference is principal.

The exhaustiveness check is aware of GADT constraints, and can automatically infer that some cases cannot happen. For instance, the following pattern matching is correctly seen as exhaustive (the `Add` case cannot happen).

```h
let get_int : int term -> int = function
| Int n      -> n
| App(_,_)-> 0
```

## 7.3 Refutation cases

Usually, the exhaustiveness check only tries to check whether the cases omitted from the pattern matching are typable or not. However, you can force it to try harder by adding *refutation cases*, written as a full stop. In the presence of a refutation case, the exhaustiveness check will first compute the intersection of the pattern with the complement of the cases preceding it. It then checks whether the resulting patterns can really match any concrete values by trying to type-check them. Wild cards in the generated patterns are handled in a special way: if their type is a variant type with only GADT constructors, then the pattern is split into the different constructors, in order to check whether any of them is possible (this splitting is not done for arguments of these constructors, to avoid non-termination). We also split tuples and variant types with only one case, since they may contain GADTs inside. For instance, the following code is deemed exhaustive:

```h
type _ t =
| Int : int t
| Bool : bool t
```

```h
let deep : (char t * int) option -> char = function
| None -> 'c'
| _ -> .
```

Namely, the inferred remaining case is `Some _`, which is split into `Some (Int, _)` and `Some (Bool, _)`), which are both untypable because `deep` expects a non-existing `char t` as the first element of the tuple. Note that the refutation case could be omitted here, because it is automatically added when there is only one case in the pattern matching.

Another addition is that the redundancy check is now aware of GADTs: a case will be detected as redundant if it could be replaced by a refutation case using the same pattern.

## 7.4 Advanced examples

The `term` type we have defined above is an *indexed type*, where a type parameter reflects a property of the value contents. Another use of GADTs is *singleton types*, where a GADT value represents exactly one type. This value can be used as runtime representation for this type, and a function receiving it can have a polytypic behavior.
Here is an example of a polymorphic function that takes the runtime representation of some
type `t` and a value of the same type, then pretty-prints the value as a string:

```h
type _ typ =
| Int : int typ
| String : string typ
| Pair : 'a typ * 'b typ -> ('a * 'b) typ

let rec to_string: type t. t typ -> t -> string =
fun t x ->
match t with
| Int -> Int.to_string x
| String -> Printf.sprintf "%S" x
| Pair(t1,t2) ->
  let (x1, x2) = x in
  Printf.sprintf "(%S, %S)" (to_string t1 x1) (to_string t2 x2)
```

Another frequent application of GADTs is equality witnesses.

```h
type (_,_) eq = Eq : ('a, 'a) eq
```

```h
let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x
```

Here type `eq` has only one constructor, and by matching on it one adds a local constraint allowing the conversion between `a` and `b`. By building such equality witnesses, one can make equal types which are syntactically different.

Here is an example using both singleton types and equality witnesses to implement dynamic types.

```h
let rec eq_type : type a b. a typ -> b typ -> (a,b) eq option =
fun a b ->
match a, b with
| Int, Int -> Some Eq
| String, String -> Some Eq
| Pair(a1,a2), Pair(b1,b2) ->
  begin match eq_type a1 b1, eq_type a2 b2 with
  | Some Eq, Some Eq -> Some Eq
  | _ -> None
  end
| _ -> None
```

```h
type dyn = Dyn : 'a typ * 'a -> dyn
```

```h
let get_dyn : type a. a typ -> dyn -> a option =
fun a (Dyn(b,x)) ->
match eq_type a b with
| None -> None
| Some Eq -> Some x
```
Here is an example of a polymorphic function that takes the runtime representation of some
type `t` and a value of the same type, then pretty-prints the value as a string:

```h
type _ typ =
| Int : int typ
| String : string typ
| Pair : 'a typ * 'b typ -> ('a * 'b) typ

let rec to_string: type t. t typ -> t -> string =
fun t x ->
match t with
| Int -> Int.to_string x
| String -> Printf.sprintf "%S" x
| Pair(t1,t2) ->
  let (x1, x2) = x in
  Printf.sprintf "%S,%S" (to_string t1 x1) (to_string t2 x2)
```

Another frequent application of GADTs is equality witnesses.

```h
type (_,_) eq = Eq : ('a,'a) eq
```

```h
let cast : type a b. (a,b) eq -> a -> b = fun Eq x -> x
```

Here type `eq` has only one constructor, and by matching on it one adds a local constraint allowing the conversion between `a` and `b`. By building such equality witnesses, one can make equal types which are syntactically different.

Here is an example using both singleton types and equality witnesses to implement dynamic types.

```h
let rec eq_type : type a b. a typ -> b typ -> (a,b) eq option =
fun a b ->
match a, b with
| Int, Int -> Some Eq
| String, String -> Some Eq
| Pair(a1,a2), Pair(b1,b2) ->
  begin match eq_type a1 b1, eq_type a2 b2 with
  | Some Eq, Some Eq -> Some Eq
  | _ -> None
  end
| _ -> None
```

```h
type dyn = Dyn : 'a typ * 'a -> dyn
```

```h
let get_dyn : type a. a typ -> dyn -> a option =
fun a (Dyn(b,x)) ->
match eq_type a b with
| None -> None
| Some Eq -> Some x
```
## 7.5 Existential type names in error messages

The typing of pattern matching in the presence of GADTs can generate many existential types. When necessary, error messages refer to these existential types using compiler-generated names. Currently, the compiler generates these names according to the following nomenclature:

* First, types whose name starts with a `$` are existentials.

* `$Constr_'a` denotes an existential type introduced for the type variable `'a` of the GADT constructor `Constr`:

```hkl
type any = Any : 'name -> any
let escape (Any x) = x
```

```
Error: This expression has type $Any_'name
but an expression was expected of type 'a
The type constructor $Any_'name would escape its scope
```

* `$Constr` denotes an existential type introduced for an anonymous type variable in the GADT constructor `Constr`:

```hkl
type any = Any : _ -> any
let escape (Any x) = x
```

```
Error: This expression has type $Any but an expression was expected of type
'a
The type constructor $Any would escape its scope
```

* `$'a` if the existential variable was unified with the type variable `'a` during typing:

```hkl
type ('arg,'result,'aux) fn =
| Fun: ('a -> 'b) -> ('a,'b,unit) fn
| Mem1: ('a -> 'b) * 'a * 'b -> ('a, 'b, 'a * 'b) fn
let apply: ('arg,'result,_) fn -> 'arg -> 'result = fun f x ->
match f with
| Fun f -> f x
| Mem1 (f,y,fy) -> if x = y then fy else f x
```

```
Error: This pattern matches values of type
($'arg, 'result, $'arg * 'result) fn
but a pattern was expected which matches values of type
($'arg, 'result, unit) fn
The type constructor $'arg would escape its scope
```

* `$n` (a number) is an internally generated existential which could not be named using one of the previous schemes.

As shown by the last item, the current behavior is imperfect and may be improved in future versions.
## 7.5 Existential type names in error messages

The typing of pattern matching in the presence of GADTs can generate many existential types. When necessary, error messages refer to these existential types using compiler-generated names. Currently, the compiler generates these names according to the following nomenclature:

* First, types whose name starts with a `$` are existentials.

* `$a` denotes an existential type introduced for the type variable `'a` of a GADT constructor:

```hhl
type any = Any : 'name -> any
```

```hhl
let escape (Any x) = x
```

```
Error: The value x has type $name but an expression was expected of type 'a
The type constructor $name would escape its scope
Hint: $name is an existential type bound by the constructor Any.
```

* `$'a` if the existential variable was unified with the type variable `'a` during typing:

```hhl
type ('arg', 'result', 'aux') fn =
```

```hhl
| Fun: ('a -> 'b) -> ('a, 'b, unit) fn
```

```hhl
| Mem1: ('a -> 'b) * 'a * 'b -> ('a, 'b, 'a * 'b) fn
```

```hhl
let apply: ('arg', 'result', ...) fn -> 'arg -> 'result = fun f x ->
```

```hhl
match f with
```

```hhl
| Fun f -> f x
```

```hhl
| Mem1 (f,y, fy) -> if x = y then fy else f x
```

```
Error: This pattern matches values of type
($'arg, 'result, $'arg * 'result) fn
but a pattern was expected which matches values of type
($'arg, 'result, unit) fn
The type constructor $'arg would escape its scope
```

* `$n` (a number) is an internally generated existential which could not be named using one of the previous schemes.

As shown by the last item, the current behavior is imperfect and may be improved in future versions.

## 7.6 Explicit naming of existentials

As explained above, pattern-matching on a GADT constructor may introduce existential types. Syntax has been introduced which allows them to be named explicitly. For instance, the following code names the type of the argument of `f` and uses this name.

```hhl
type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure
```

```hhl
let eval = fun (Closure (type a) (f, x : (a -> ...) * _)) -> f (x : a)
```

All existential type variables of the constructor must be introduced by the `(type ...)` construct and bound by a type annotation on the outside of the constructor argument.

One can additionally bind existentials that were freshly introduced by the refinement of another existential type, if they appear in the type of the arguments.
## 7.6 Explicit naming of existentials

As explained above, pattern-matching on a GADT constructor may introduce existential types. Syntax has been introduced which allows them to be named explicitly. For instance, the following code names the type of the argument of `f` and uses this name.

```hhl
type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure
let eval = fun (Closure (type a) (f, x : (a -> ...) * _)) -> f (x : a)
```

All existential type variables of the constructor must by introduced by the `(type ...)` construct and bound by a type annotation on the outside of the constructor argument.

## 7.7 Equations on non-local abstract types

GADT pattern-matching may also add type equations to non-local abstract types. The behaviour is the same as with local abstract types. Reusing the above `eq` type, one can write:

```hhl
module M : sig type t val x : t val e : (t,int) eq end = struct
    type t = int
    let x = 33
    let e = Eq
end
```

```hhl
let x : int = let Eq = M.e in M.x
```

Of course, not all abstract types can be refined, as this would contradict the exhaustiveness check. Namely, builtin types (those defined by the compiler itself, such as `int` or `array`), and abstract types defined by the local module, are non-instantiable, and as such cause a type error rather than introduce an equation.
```h
    type _ ty =
    | Int : int ty
    | Pair : 'b ty * 'c ty -> ('b * 'c) ty

let rec default : type a. a ty -> a = function
| Int -> 0
| Pair (type b c) (b, c : b ty * c ty) ->
    (default b : b), (default c : c)
```

## 7.7 Equations on non-local abstract types

GADT pattern-matching may also add type equations to non-local abstract types. The behaviour is the same as with local abstract types. Reusing the above `eq` type, one can write:

```h
module M : sig type t val x : t val e : (t,int) eq end = struct
    type t = int
    let x = 33
    let e = Eq
end
```

```h
let x : int = let Eq = M.e in M.x
```

Of course, not all abstract types can be refined, as this would contradict the exhaustiveness check. Namely, builtin types (those defined by the compiler itself, such as `int` or `array`), and abstract types defined by the local module, are non-instantiable, and as such cause a type error rather than introduce an equation.
# Chapter 8

## Advanced examples with classes and modules

*(Chapter written by Didier Rémy)*

In this chapter, we show some larger examples using objects, classes and modules. We review many of the object features simultaneously on the example of a bank account. We show how modules taken from the standard library can be expressed as classes. Lastly, we describe a programming pattern known as *virtual types* through the example of window managers.

### 8.1 Extended example: bank accounts

In this section, we illustrate most aspects of Object and inheritance by refining, debugging, and specializing the following initial naive definition of a simple bank account. (We reuse the module `Euro` defined at the end of chapter 3.)

```python
# let euro = new Euro.c;;
val euro : float -> Euro.c = <fun>

# let zero = euro 0.;;
val zero : Euro.c = <obj>

# let neg x = x#times (-1).;;
val neg : < times : float -> 'a; .. > -> 'a = <fun>

# class account =
object
    val mutable balance = zero
    method balance = balance
    method deposit x = balance <- balance # plus x
    method withdraw x =
        if x#leq balance then (balance <- balance # plus (neg x); x) else zero
    end;
```
# Chapter 8

## Advanced examples with classes and modules

*(Chapter written by Didier Rémy)*

In this chapter, we show some larger examples using objects, classes and modules. We review many of the object features simultaneously on the example of a bank account. We show how modules taken from the standard library can be expressed as classes. Lastly, we describe a programming pattern known as *virtual types* through the example of window managers.

### 8.1 Extended example: bank accounts

In this section, we illustrate most aspects of Object and inheritance by refining, debugging, and specializing the following initial naive definition of a simple bank account. (We reuse the module `Euro` defined at the end of chapter 3.)

```python
# let euro = new Euro.c;;
val euro : float -> Euro.c = <fun>

# let zero = euro 0.;;
val zero : Euro.c = <obj>

# let neg x = x#times (-1).;;
val neg : < times : float -> 'a; .. > -> 'a = <fun>

# class account =
object
    val mutable balance = zero
    method balance = balance
    method deposit x = balance <- balance # plus x
    method withdraw x =
        if x#leq balance then (balance <- balance # plus (neg x); x) else zero
end;;
```
```kotlin
class account :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method withdraw : Euro.c -> Euro.c
end
```

```kotlin
# let c = new account in c # deposit (euro 100.); c # withdraw (euro 50.);
- : Euro.c = <obj>
```

We now refine this definition with a method to compute interest.

```kotlin
# class account_with_interests =
    object (self)
        inherit account
        method private interest = self # deposit (self # balance # times 0.03)
end;

class account_with_interests :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method private interest : unit
        method withdraw : Euro.c -> Euro.c
end
```

We make the method `interest` private, since clearly it should not be called freely from the outside. Here, it is only made accessible to subclasses that will manage monthly or yearly updates of the account.

We should soon fix a bug in the current definition: the deposit method can be used for withdrawing money by depositing negative amounts. We can fix this directly:

```kotlin
# class safe_account =
    object
        inherit account
        method deposit x = if zero#leq x then balance <- balance#plus x
end;

class safe_account :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method withdraw : Euro.c -> Euro.c
end
```

However, the bug might be fixed more safely by the following definition:

```kotlin
# class safe_account =
    object
        inherit account as unsafe
```
```python
class account :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method withdraw : Euro.c -> Euro.c
end
```

```python
# let c = new account in c # deposit (euro 100.); c # withdraw (euro 50.);
- : Euro.c = <obj>
```

We now refine this definition with a method to compute interest.

```python
# class account_with_interests =
    object (self)
        inherit account
        method private interest = self # deposit (self # balance # times 0.03)
end;

class account_with_interests :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method private interest : unit
        method withdraw : Euro.c -> Euro.c
end
```

We make the method `interest` private, since clearly it should not be called freely from the outside. Here, it is only made accessible to subclasses that will manage monthly or yearly updates of the account.

We should soon fix a bug in the current definition: the `deposit` method can be used for withdrawing money by depositing negative amounts. We can fix this directly:

```python
# class safe_account =
    object
        inherit account
        method deposit x = if zero#leq x then balance <- balance#plus x
end;

class safe_account :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method withdraw : Euro.c -> Euro.c
end
```

However, the bug might be fixed more safely by the following definition:

```python
# class safe_account =
    object
        inherit account as unsafe
```
```python
method deposit x =
    if zero#leq x then unsafe # deposit x
    else raise (Invalid_argument "deposit")
end;

class safe_account :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method withdraw : Euro.c -> Euro.c
end
```

In particular, this does not require the knowledge of the implementation of the method `deposit`.

To keep track of operations, we extend the class with a mutable field `history` and a private method `trace` to add an operation in the log. Then each method to be traced is redefined.

```python
# type 'a operation = Deposit of 'a | Retrieval of 'a;;
type 'a operation = Deposit of 'a | Retrieval of 'a

type 'a account_with_history =
    object (self)
        inherit safe_account as super
        val mutable history = []
        method private trace x = history <- x :: history
        method deposit x = self#trace (Deposit x); super#deposit x
        method withdraw x = self#trace (Retrieval x); super#withdraw x
        method history = List.rev history
end;

class account_with_history :
    object
        val mutable balance : Euro.c
        val mutable history : Euro.c operation list
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method history : Euro.c operation list
        method private trace : Euro.c operation -> unit
        method withdraw : Euro.c -> Euro.c
end
```

One may wish to open an account and simultaneously deposit some initial amount. Although the initial implementation did not address this requirement, it can be achieved by using an initializer.

```python
# class account_with_deposit x =
    object
        inherit account_with_history
        initializer balance <- x
end;

class account_with_deposit :
    Euro.c ->
    object
```
8.1. Extended example: bank accounts

```ksharp
method deposit x =
    if zero#leq x then unsafe # deposit x
    else raise (Invalid_argument "deposit")
end;;

class safe_account :
    object
        val mutable balance : Euro.c
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method withdraw : Euro.c -> Euro.c
end
```

In particular, this does not require the knowledge of the implementation of the method `deposit`.

To keep track of operations, we extend the class with a mutable field `history` and a private method `trace` to add an operation in the log. Then each method to be traced is redefined.

```ksharp
# type 'a operation = Deposit of 'a | Retrieval of 'a;;
type 'a operation = Deposit of 'a | Retrieval of 'a

# class account_with_history =
    object (self)
        inherit safe_account as super
        val mutable history = []
        method private trace x = history <- x :: history
        method deposit x = self#trace (Deposit x); super#deposit x
        method withdraw x = self#trace (Retrieval x); super#withdraw x
        method history = List.rev history
end;;

class account_with_history :
    object
        val mutable balance : Euro.c
        val mutable history : Euro.c operation list
        method balance : Euro.c
        method deposit : Euro.c -> unit
        method history : Euro.c operation list
        method private trace : Euro.c operation -> unit
        method withdraw : Euro.c -> Euro.c
end
```

One may wish to open an account and simultaneously deposit some initial amount. Although the initial implementation did not address this requirement, it can be achieved by using an initializer.

```ksharp
# class account_with_deposit x =
    object
        inherit account_with_history
        initializer balance <- x
end;;

class account_with_deposit :
    Euro.c ->
    object
```
```h
val mutable balance : Euro.c
val mutable history : Euro.c operation list
method balance : Euro.c
method deposit : Euro.c -> unit
method history : Euro.c operation list
method private trace : Euro.c operation -> unit
method withdraw : Euro.c -> Euro.c
end
```

A better alternative is:

```h
# class account_with_deposit x =
object (self)
    inherit account_with_history
    initializer self#deposit x
end;

class account_with_deposit :
    Euro.c ->
object
    val mutable balance : Euro.c
    val mutable history : Euro.c operation list
    method balance : Euro.c
    method deposit : Euro.c -> unit
    method history : Euro.c operation list
    method private trace : Euro.c operation -> unit
    method withdraw : Euro.c -> Euro.c
end
```

Indeed, the latter is safer since the call to `deposit` will automatically benefit from safety checks and from the trace. Let's test it:

```h
# let ccp = new account_with_deposit (euro 100.) in
let _balance = ccp#withdraw (euro 50.) in
ccp#history;;
- : Euro.c operation list = [Deposit <obj>; Retrieval <obj>]
```

Closing an account can be done with the following polymorphic function:

```h
# let close c = c#withdraw c#balance;;
val close : < balance : 'a; withdraw : 'a -> 'b; .. > -> 'b = <fun>
```

Of course, this applies to all sorts of accounts.

Finally, we gather several versions of the account into a module `Account` abstracted over some currency.

```h
# let today () = (01,01,2000) (* an approximation *)
module Account (M:MONEY) =
    struct
        type m = M.c
        let m = new M.c
        let zero = m 0.
```
```python
val mutable balance : Euro.c
val mutable history : Euro.c operation list
method balance : Euro.c
method deposit : Euro.c -> unit
method history : Euro.c operation list
method private trace : Euro.c operation -> unit
method withdraw : Euro.c -> Euro.c
end
```

A better alternative is:

```python
# class account_with_deposit x =
object (self)
    inherit account_with_history
    initializer self#deposit x
end;

class account_with_deposit :
    Euro.c ->
object
    val mutable balance : Euro.c
    val mutable history : Euro.c operation list
    method balance : Euro.c
    method deposit : Euro.c -> unit
    method history : Euro.c operation list
    method private trace : Euro.c operation -> unit
    method withdraw : Euro.c -> Euro.c
end
```

Indeed, the latter is safer since the call to `deposit` will automatically benefit from safety checks and from the trace. Let's test it:

```python
# let ccp = new account_with_deposit (euro 100.) in
let _balance = ccp#withdraw (euro 50.) in
ccp#history;;
- : Euro.c operation list = [Deposit <obj>; Retrieval <obj>]
```

Closing an account can be done with the following polymorphic function:

```python
# let close c = c#withdraw c#balance;;
val close : < balance : 'a; withdraw : 'a -> 'b; .. > -> 'b = <fun>
```

Of course, this applies to all sorts of accounts.

Finally, we gather several versions of the account into a module `Account` abstracted over some currency.

```python
# let today () = (01,01,2000) (* an approximation *)
module Account (M:MONEY) =
    struct
        type m = M.c
        let m = new M.c
        let zero = m 0.
```
```python
class bank =
    object (self)
        val mutable balance = zero
        method balance = balance
        val mutable history = []
        method private trace x = history <- x::history
        method deposit x =
            self#trace (Deposit x);
            if zero#leq x then balance <- balance # plus x
            else raise (Invalid_argument "deposit")
        method withdraw x =
            if x#leq balance then
                (balance <- balance # plus (neg x); self#trace (Retrieval x); x)
            else zero
        method history = List.rev history
end
```

```python
class type client_view =
    object
        method deposit : m -> unit
        method history : m operation list
        method withdraw : m -> m
        method balance : m
end
```

```python
class virtual check_client x =
    let y = if (m 100.)#leq x then x
        else raise (Failure "Insufficient initial deposit") in
    object (self)
        initializer self#deposit y
        method virtual deposit: m -> unit
end
```

```python
module Client (B : sig class bank : client_view end) =
    struct
        class account x : client_view =
            object
                inherit B.bank
                inherit check_client x
            end

        let discount x =
            let c = new account x in
                if today() < (1998,10,30) then c # deposit (m 100.); c
end
```
```python
class bank =
object (self)
    val mutable balance = zero
    method balance = balance
    val mutable history = []
    method private trace x = history <- x::history
    method deposit x =
        self#trace (Deposit x);
        if zero#leq x then balance <- balance # plus x
        else raise (Invalid_argument "deposit")
    method withdraw x =
        if x#leq balance then
            (balance <- balance # plus (neg x); self#trace (Retrieval x); x)
        else zero
    method history = List.rev history
end
```

```python
class type client_view =
object
    method deposit : m -> unit
    method history : m operation list
    method withdraw : m -> m
    method balance : m
end
```

```python
class virtual check_client x =
    let y = if (m 100.)#leq x then x
        else raise (Failure "Insufficient initial deposit") in
    object (self)
        initializer self#deposit y
        method virtual deposit: m -> unit
end
```

```python
module Client (B : sig class bank : client_view end) =
struct
    class account x : client_view =
        object
            inherit B.bank
            inherit check_client x
        end

    let discount x =
        let c = new account x in
            if today() < (1998,10,30) then c # deposit (m 100.); c
end
```
end;;

This shows the use of modules to group several class definitions that can in fact be thought of as a
single unit. This unit would be provided by a bank for both internal and external uses. This is
implemented as a functor that abstracts over the currency so that the same code can be used to
provide accounts in different currencies.

The class `bank` is the *real* implementation of the bank account (it could have been inlined). This is the one that will be used for further extensions, refinements, etc. Conversely, the client will only be given the client view.

# module Euro_account = Account(Euro);;

# module Client = Euro_account.Client (Euro_account);;

# new Client account (new Euro.c 100.);;

Hence, the clients do not have direct access to the `balance`, nor the `history` of their own accounts.
Their only way to change their balance is to deposit or withdraw money. It is important to give
the clients a class and not just the ability to create accounts (such as the promotional `discount`
account), so that they can personalize their account. For instance, a client may refine the `deposit`
and `withdraw` methods so as to do his own financial bookkeeping, automatically. On the other
hand, the function `discount` is given as such, with no possibility for further personalization.

It is important to provide the client's view as a functor `Client` so that client accounts can still
be built after a possible specialization of the `bank`. The functor `Client` may remain unchanged and
be passed the new definition to initialize a client's view of the extended account.

# module Investment_account (M : MONEY) =

struct

type m = M.c

module A = Account(M)

class bank =

object

inherit A.bank as super

method deposit x =

if (new M.c 1000.)#leq x then

print_string "Would you like to invest?";

super#deposit x

end

module Client = A.Client

end;;

The functor `Client` may also be redefined when some new features of the account can be given to
the client.

# module Internet_account (M : MONEY) =

struct

type m = M.c

module A = Account(M)
end;;

This shows the use of modules to group several class definitions that can in fact be thought of as a
single unit. This unit would be provided by a bank for both internal and external uses. This is
implemented as a functor that abstracts over the currency so that the same code can be used to
provide accounts in different currencies.

The class `bank` is the *real* implementation of the bank account (it could have been inlined). This is the one that will be used for further extensions, refinements, etc. Conversely, the client will only be given the client view.

```python
# module Euro_account = Account(Euro);;

# module Client = Euro_account.Client (Euro_account);;

# new Client account (new Euro.c 100.);;
```

Hence, the clients do not have direct access to the `balance`, nor the `history` of their own accounts.
Their only way to change their balance is to deposit or withdraw money. It is important to give
the clients a class and not just the ability to create accounts (such as the promotional `discount`
account), so that they can personalize their account. For instance, a client may refine the `deposit`
and `withdraw` methods so as to do his own financial bookkeeping, automatically. On the other
hand, the function `discount` is given as such, with no possibility for further personalization.

It is important to provide the client's view as a functor `Client` so that client accounts can still
be built after a possible specialization of the `bank`. The functor `Client` may remain unchanged and
be passed the new definition to initialize a client's view of the extended account.

```python
# module Investment_account (M : MONEY) =
    struct
        type m = M.c
        module A = Account(M)

    class bank =
        object
            inherit A.bank as super
            method deposit x =
                if (new M.c 1000.)#leq x then
                    print_string "Would you like to invest?";
                    super#deposit x
                end

    module Client = A.Client
end;;
```

The functor `Client` may also be redefined when some new features of the account can be given to
the client.

```python
# module Internet_account (M : MONEY) =
    struct
        type m = M.c
        module A = Account(M)
```
```python
class bank =
    object
        inherit A.bank
        method mail s = print_string s
    end
```

```python
class type client_view =
    object
        method deposit : m -> unit
        method history : m operation list
        method withdraw : m -> m
        method balance : m
        method mail : string -> unit
    end
```

```python
module Client (B : sig class bank : client_view end) =
    struct
        class account x : client_view =
            object
                inherit B.bank
                inherit A.check_client x
            end
        end
    end;
```

## 8.2 Simple modules as classes

One may wonder whether it is possible to treat primitive types such as integers and strings as objects. Although this is usually uninteresting for integers or strings, there may be some situations where this is desirable. The class `money` above is such an example. We show here how to do it for strings.

### 8.2.1 Strings

A naive definition of strings as objects could be:

```python
# class ostring s =
    object
        method get n = String.get s n
        method print = print_string s
        method escaped = new ostring (String.escaped s)
    end;

class ostring :
    string ->
    object
        method escaped : ostring
```
```python
class bank =
    object
        inherit A.bank
        method mail s = print_string s
    end
```

```python
class type client_view =
    object
        method deposit : m -> unit
        method history : m operation list
        method withdraw : m -> m
        method balance : m
        method mail : string -> unit
    end
```

```python
module Client (B : sig class bank : client_view end) =
    struct
        class account x : client_view =
            object
                inherit B.bank
                inherit A.check_client x
            end
    end
end;
```

## 8.2 Simple modules as classes

One may wonder whether it is possible to treat primitive types such as integers and strings as objects. Although this is usually uninteresting for integers or strings, there may be some situations where this is desirable. The class `money` above is such an example. We show here how to do it for strings.

### 8.2.1 Strings

A naive definition of strings as objects could be:

```python
# class ostring s =
    object
        method get n = String.get s n
        method print = print_string s
        method escaped = new ostring (String.escaped s)
    end;

class ostring :
    string ->
    object
        method escaped : ostring
```
```kotlin
method get : int -> char
method print : unit
end
```

However, the method `escaped` returns an object of the class `ostring`, and not an object of the current class. Hence, if the class is further extended, the method `escaped` will only return an object of the parent class.

```kotlin
# class sub_string s =
object
    inherit ostring s
    method sub start len = new sub_string (String.sub s start len)
end;

class sub_string :
    string ->
    object
        method escaped : ostring
        method get : int -> char
        method print : unit
        method sub : int -> int -> sub_string
end
```

As seen in section 3.16, the solution is to use functional update instead. We need to create an instance variable containing the representation `s` of the string.

```kotlin
# class better_string s =
object
    val repr = s
    method get n = String.get repr n
    method print = print_string repr
    method escaped = {< repr = String.escaped repr >}
    method sub start len = {< repr = String.sub s start len >}
end;

class better_string :
    string ->
    object ('a)
        val repr : string
        method escaped : 'a
        method get : int -> char
        method print : unit
        method sub : int -> int -> 'a
end
```

As shown in the inferred type, the methods `escaped` and `sub` now return objects of the same type as the one of the class.

Another difficulty is the implementation of the method `concat`. In order to concatenate a string with another string of the same class, one must be able to access the instance variable externally. Thus, a method `repr` returning `s` must be defined. Here is the correct definition of strings:

```kotlin
# class ostring s =
object (self : 'mytype)
```
```python
method get : int -> char
method print : unit
end
```

However, the method `escaped` returns an object of the class `ostring`, and not an object of the current class. Hence, if the class is further extended, the method `escaped` will only return an object of the parent class.

```python
# class sub_string s =
    object
        inherit ostring s
        method sub start len = new sub_string (String.sub s start len)
    end;

class sub_string :
    string ->
    object
        method escaped : ostring
        method get : int -> char
        method print : unit
        method sub : int -> int -> sub_string
    end
```

As seen in section 3.16, the solution is to use functional update instead. We need to create an instance variable containing the representation `s` of the string.

```python
# class better_string s =
    object
        val repr = s
        method get n = String.get repr n
        method print = print_string repr
        method escaped = {< repr = String.escaped repr >}
        method sub start len = {< repr = String.sub s start len >}
    end;

class better_string :
    string ->
    object ('a')
        val repr : string
        method escaped : 'a
        method get : int -> char
        method print : unit
        method sub : int -> int -> 'a
    end
```

As shown in the inferred type, the methods `escaped` and `sub` now return objects of the same type as the one of the class.

Another difficulty is the implementation of the method `concat`. In order to concatenate a string with another string of the same class, one must be able to access the instance variable externally. Thus, a method `repr` returning `s` must be defined. Here is the correct definition of strings:

```python
# class ostring s =
    object (self : 'mytype)
```
```kotlin
val repr = s
method repr = repr
method get n = String.get repr n
method print = print_string repr
method escaped = {< repr = String.escaped repr >}
method sub start len = {< repr = String.sub s start len >}
method concat (t : 'mytype) = {< repr = repr ^ t#repr >}
end;

class ostring :
    string ->
    object ('a)
        val repr : string
        method concat : 'a -> 'a
        method escaped : 'a
        method get : int -> char
        method print : unit
        method repr : string
        method sub : int -> int -> 'a
end
```

Another constructor of the class string can be defined to return a new string of a given length:

```kotlin
# class cstring n = ostring (String.make n ' ');
class cstring : int -> ostring
```

Here, exposing the representation of strings is probably harmless. We do could also hide the representation of strings as we hid the currency in the class `money` of section 3.17.

## 8.2.2 Stacks

There is sometimes an alternative between using modules or classes for parametric data types. Indeed, there are situations when the two approaches are quite similar. For instance, a stack can be straightforwardly implemented as a class:

```kotlin
# exception Empty;
exception Empty

class ['a] stack =
    object
        val mutable l = ([] : 'a list)
        method push x = l <- x::l
        method pop = match l with [] -> raise Empty | a::l' -> l <- l'; a
        method clear = l <- []
        method length = List.length l
end;

class ['a] stack :
    object
        val mutable l : 'a list
        method clear : unit
        method length : int
```
```kotlin
val repr = s
method repr = repr
method get n = String.get repr n
method print = print_string repr
method escaped = {< repr = String.escaped repr >}
method sub start len = {< repr = String.sub s start len >}
method concat (t : 'mytype) = {< repr = repr ^ t#repr >}
end;

class ostring :
    string ->
    object ('a)
        val repr : string
        method concat : 'a -> 'a
        method escaped : 'a
        method get : int -> char
        method print : unit
        method repr : string
        method sub : int -> int -> 'a
end
```

Another constructor of the class string can be defined to return a new string of a given length:

```kotlin
# class cstring n = ostring (String.make n ' ');
class cstring : int -> ostring
```

Here, exposing the representation of strings is probably harmless. We do could also hide the representation of strings as we hid the currency in the class `money` of section 3.17.

### 8.2.2 Stacks

There is sometimes an alternative between using modules or classes for parametric data types. Indeed, there are situations when the two approaches are quite similar. For instance, a stack can be straightforwardly implemented as a class:

```kotlin
# exception Empty;
exception Empty

class ['a] stack =
    object
        val mutable l = ([] : 'a list)
        method push x = l <- x::l
        method pop = match l with [] -> raise Empty | a::l' -> l <- l'; a
        method clear = l <- []
        method length = List.length l
end;

class ['a] stack :
    object
        val mutable l : 'a list
        method clear : unit
        method length : int
```
```ksharp
method pop : 'a
method push : 'a -> unit
end
```

However, writing a method for iterating over a stack is more problematic. A method `fold` would have type `( 'b -> 'a -> 'b ) -> 'b -> 'b`. Here `'a` is the parameter of the stack. The parameter `'b` is not related to the class `'a stack` but to the argument that will be passed to the method `fold`. A naive approach is to make `'b` an extra parameter of class `stack`:

```ksharp
# class ['a, 'b] stack2 =
    object
        inherit ['a] stack
        method fold f (x : 'b) = List.fold_left f x 1
    end;;

class ['a, 'b] stack2 :
    object
        val mutable l : 'a list
        method clear : unit
        method fold : ('b -> 'a -> 'b) -> 'b -> 'b
        method length : int
        method pop : 'a
        method push : 'a -> unit
end
```

However, the method `fold` of a given object can only be applied to functions that all have the same type:

```ksharp
# let s = new stack2;;
val s : ('_weak1, '_weak2) stack2 = <obj>

# s#fold ( + ) 0;;
- : int = 0

# s;;
- : (int, int) stack2 = <obj>
```

A better solution is to use polymorphic methods, which were introduced in OCaml version 3.05. Polymorphic methods make it possible to treat the type variable `'b` in the type of `fold` as universally quantified, giving `fold` the polymorphic type `forall 'b. ('b -> 'a -> 'b) -> 'b -> 'b`. An explicit type declaration on the method `fold` is required, since the type checker cannot infer the polymorphic type by itself.

```ksharp
# class ['a] stack3 =
    object
        inherit ['a] stack
        method fold : 'b. ('b -> 'a -> 'b) -> 'b -> 'b
            = fun f x -> List.fold_left f x 1
    end;;

class ['a] stack3 :
    object
```
```python
method pop : 'a
method push : 'a -> unit
end
```

However, writing a method for iterating over a stack is more problematic. A method `fold` would have type `( 'b -> 'a -> 'b ) -> 'b -> 'b`. Here `'a` is the parameter of the stack. The parameter `'b` is not related to the class `'a stack'` but to the argument that will be passed to the method `fold`. A naive approach is to make `'b` an extra parameter of class `stack`:

```python
# class ['a, 'b] stack2 =
object
    inherit ['a] stack
    method fold f (x : 'b) = List.fold_left f x l
end;

class ['a, 'b] stack2 :
    object
        val mutable l : 'a list
        method clear : unit
        method fold : ('b -> 'a -> 'b) -> 'b -> 'b
        method length : int
        method pop : 'a
        method push : 'a -> unit
end
```

However, the method `fold` of a given object can only be applied to functions that all have the same type:

```python
# let s = new stack2;
val s : ('_weak1, '_weak2) stack2 = <obj>

# s#fold ( + ) 0;
- : int = 0

# s;
- : (int, int) stack2 = <obj>
```

A better solution is to use polymorphic methods, which were introduced in OCaml version 3.05. Polymorphic methods make it possible to treat the type variable `'b` in the type of `fold` as universally quantified, giving `fold` the polymorphic type `forall 'b. ('b -> 'a -> 'b) -> 'b -> 'b`. An explicit type declaration on the method `fold` is required, since the type checker cannot infer the polymorphic type by itself.

```python
# class ['a] stack3 =
object
    inherit ['a] stack
    method fold : 'b. ('b -> 'a -> 'b) -> 'b -> 'b
        = fun f x -> List.fold_left f x l
end;

class ['a] stack3 :
    object
```