When a language (where type checking is done before the program runs, like in Java or OCaml) introduces parametric polymorphism (Java's generics), it's sometimes possible to constrain type variables. For example:

class MyClass<T extends S> { ... }

We make MyClass generic by assuming that the type variable T is a subtype of S. The problem is that the constraint applies to the entire class. Yet sometimes, we’d like to have constraints apply only to certain methods. For example, let’s say we have a class MyList describing a list:

class MyList<A> extends ArrayList<A> {
   public int length() {
     return this.size();
   }
}

How can we define a flatten method that, for a list like [[1, 2, 3], [4, 5]], would produce the list [1, 2, 3, 4, 5]? If we place the constraint at the class level, we force our list to be "always a list of lists," which is very limiting. To implement such a method, we have three theoretical approaches available.

The first solution is the most obvious: simply "cheat" by moving the method outside the class body (for example, into the static context or a companion object):

class MyList<A> extends ArrayList<A> {
   public static <A> MyList<A> flatten(MyList<MyList<A>> list) {
   }
   public int length() {
     return this.size();
   }
}

This approach works and doesn’t require any special ceremony. However, it forces the developer to keep track of which methods are in the class body and which are in the static context. Moreover, it breaks the systematic approach of sending messages to an instance (often presented as one of the key arguments in favor of object-oriented programming).

The final approach is probably the most ideological, as it keeps the method definition within the class. It doesn't force any escaped abstractions. This is the idea of guarded methods, the ability to add constraints on the generic parameter at the method definition level. In an imaginary syntax (this code compiles because it's not syntactically invalid, but it doesn’t produce the intended effect):

class MyList<A> : ArrayList<A>() {
    fun length() = size
    fun <B> MyList<MyList<B>>.flatten() =
        }

Even though this doesn’t seem significantly different from classic extension methods (as evidenced by their syntax, which inside the class body seems sufficient), it addresses all the issues raised earlier:

• we can characterize the receiver more precisely than in a normal method
• we don’t break the regular message sending
• we still benefit from available members (so we don’t escape representations)

Although guarded methods seem necessary, unfortunately, I don’t know of any mainstream languages that allow their definition. That’s very sad. Fortunately, in OCaml, it is possible to encode them.

Let’s return to our example that provides an object API for a list. Here is its interface:

class type ['a] obj_list =
  object ('self)
    method length : int
    method append : 'a list -> 'a obj_list
    method uncons : ('a * 'self) option
    method flatten : ???
  end

To give a type to flatten, we want to impose that 'a (the type parameter of the obj_list class) is a list. In other words, we want a proof that 'a is of type 'b list. That is, to guarantee that 'a and 'b list, though syntactically different, are equal. It’s simple: just require a value of type ('a, 'b list) eq to be provided:

method flatten : ('a, 'b list) eq -> 'b list

Now that we have an interface describing a list with a flatten method that constrains the receiver to be a list of something, let’s concretely implement a class that implements obj_list.

The first methods (length, append, and uncons) are straightforward to implement:

let my_list (list : 'a list) =
  object (self : 'a obj_list)
    val l = list
    method length = List.length l
    method append x = {<l = List.append l x>}
    method uncons = match l with [] -> None | x :: xs -> Some (x, {<l = xs>})

    method flatten = ???
  end

Now, let’s focus on flatten. We will recursively traverse the list, concatenating each element to the previous one. For example, [[1]; [2]; [3]] will become [1] @ [2]; [3]. Beyond the somewhat noisy annotations, the entire trick lies in instantiating Refl to provide evidence that 'a = 'b list.

method flatten : 'b. ('a, 'b list) eq -> 'b list =
  let rec aux : type a b. a #obj_list -> (a, b list) eq -> b list =
  fun list witness -> match list#uncons with
    | None -> []
    | Some (head_list, xs) ->
        let flatten_list : b list =
          let Refl = witness  in head_list
        in flatten_list @ aux xs witness
  in aux self

Now that we’re able to constrain certain methods, let’s try adding a sum method that produces the sum of a list of integers! First, let’s add sum to our interface. This time, we want to constrain our type parameter to be int. To do that, we simply take ('a, int) eq as a type equality witness:

class type ['a] obj_list =
  object ('self)
    method length : int
    method append : 'a list -> 'a obj_list
    method uncons : ('a * 'self) option
    method flatten : ('a, 'b list) eq -> 'b list
    method sum : ('a, int) eq -> int
  end

Next, we can implement the sum method, which is just a use of the fold_left function.

method sum : ('a, int) eq -> int =
  let aux : type a. a list -> (a, int) eq -> int = fun list Refl ->
    List.fold_left (fun acc x -> acc + x) 0 list
  in aux l

The implementation of sum is logically simpler than that of flatten because it doesn’t introduce additional type variables. And we can test our different methods: we can invoke flatten on an object of type 'a list obj_list and sum on an object of type int obj_list.

let a = my_list [ [ 1 ]; [ 2 ]; [ 3 ] ]
let _ = assert ([ 1; 2; 3 ] = a#flatten Refl)
let b = my_list [ 1; 2; 3; 4 ]
let _ = assert (10 = b#sum Refl)

If we try to apply a guarded method with the wrong type, for example, trying to sum our list a (which is of type 'a list obj_list), the program will not compile. This makes sense, as we are trying to call a guarded method without respecting the imposed constraint.

1 | let _ = a#sum Refl
                  ^^^^
Error: This expression has type (int list, int list) eq
       but an expression was expected of type (int list, int) eq
       Type int list is not compatible with type int

Exactly the expected behavior! We can now define methods that constrain the receiver’s type by means of a type equality witness. Mission complete!