Why the unbound type variables in OCAML object do not appear when class type is used?

Question

I'd like to understand the reason for this behavior of OCAML objects. Suppose I have a class A that calls methods of an object of another class B. Schematically, A#f calls B#g and B#h. The normal practice in OOP is that I would like to avoid using B as a fixed concrete class, but instead declare only an interface for B. What is the best way to do this in OCAML? I tried several options, and I do not quite understand the reason why some of them work while others don't. Here are the code samples.

Version 1:

 # class classA = object
    method f b = b#g + b#h 
   end ;;
 Error: Some type variables are unbound in this type:
     class a : object method f : < g : int; h : int; .. > -> int end
   The method f has type (< g : int; h : int; .. > as 'a) -> int where 'a
   is unbound

This behavior is well-known: OCAML correctly infers that b has the open object type <g:int;h:int;..> but then complains that my class does not declare any type variables. So it seems that classA is required to have type variables; I then introduced a type variable explicitly.

Version 2:

 # class ['a] classA2 = object
   method f (b:'a) = b#g + b#h
   end ;;
 class ['a] classA2 :
   object constraint 'a = < g : int; h : int; .. > method f : 'a -> int end

This works, but the class is now explicitly polymorphic with a type constraint, as OCAML shows. It is also confusing that the class type contains a type variable 'a, and yet I can still say let x = new classA2 without specifying a type value for 'a. Why is that possible?

Another drawback of classA2 is that an explicit type constraint (b:'a) contains a type variable. After all, I know that b must conform to a fixed interface rather than to an unknown type 'a. I want OCAML to verify that this interface is indeed correct.

So in version 3 I first declared an interface classB as a class type and then declared that b must be of this type:

 # class type classB = object method g:int method h:int end;;
 class type classB = object method g : int method h : int end
 # class classA3 = object method f (b:classB) = b#g + b#h end;;
 class classA3 : object method f : classB -> int end

This works too, but my puzzlement remains: why doesn't classA3 require explicit polymorphism any more?

Summary of questions:

• Why is it possible to use new classA2 without specifying a type for 'a even though classA2 is declared with a type variable 'a?
• Why does classA3 accept a type constraint (b:classB) and does not require a bound type variable any more?
• Is the functionality of classA2 and classA3 different in some subtle way, and if yes, how?

Answer 1

This is going to be a bit complex, so hold tight. First, let me add a classA4 variant, which happens to be what you actually need.

class classA4 = object
  method f : 'a. (#classB as 'a) -> int = fun b -> b#g + b#h
end

Classes classA2, classA3 and classA4 are all subtly different, and the difference lies in how OCaml treats type polymorphism and object polymorphism. Let's assume that two classes, b1 and b2, implement the classB type.

In terms of object polymorphism, this means that an expression of type b1 can be coerced to type classB using the coercion syntax (new b1 :> classB). This type coercion discards type information (you no longer know the object is of type b1), so it must be made explicit.

In terms of type polymorphism, this means that type b1 can be used in place of any type variable that has constraint #classB (or < g : int ; h : int ; .. >). This does not discard any type information (as the type variable is replaced by the actual type), so it is performed by the type inference algorithm.

Method f of classA3 expects a parameter of type classB, which means a type coercion is mandatory:

let b = new b1 
let a = new classA3
a # f b (* Type error, expected classB, found b1 *)
a # f (b :> classB) (* Ok ! *)

This also means that (as long as you coerce), any class implementing classB can be used.

Method f of classA2 expects a parameter of a type that matches constraint #classB, but OCaml mandates that such a type should not be unbound, so it is bound at the class level. This means that every instance of classA2 will accept parameters of a single arbitrary type that implements classB (and that type will be type-inferred).

let b1 = new b1 and b2 = new b2
let a  = new classA2 
a # f b1 (* 'a' is type-inferred to be 'b1 classA2' *)
a # f b2 (* Type error, because b1 != b2  *)

It is important to note that classA3 is equivalent to classB classA2, which is why it does not require a bound type variable, and also why it is strictly less expressive than classA2.

Method f of classA4 has been given an explicit type using the 'a. syntax, which binds the type variable at the method level instead of the class level. It's actually an universal quantifier, which means « this method can be called for any type 'a which implements #classB » :

let b1 = new b1 and b2 = new b2
let a  = new classA4
a # f b1 (* 'a is chosen to be b1 for this call *)
a # f b2 (* 'a is chosen to be b2 for this call *)

Answer 2

There is a solution that is slightly simpler than Victor's: you need not parametrize class2 over a type, just use class type classB:

class classA2bis = object
  method f (b: classB) = b#g + b#h
end ;;

Victor's solution (f : 'a . (#classB as 'a) -> int) works for any type that is a supertype of classB. Both are equally expressive: with Victor's solution, as he explain, the class used is instantiated at the call site: a#f b will work for any type of b bigger than classB, by implicit polymorphic instantiation. With this solution, the argument has to be of the exact type classB, so you must coerce it explicitely if b has a bigger type: a#f (b :> classB).

So both solutions make different complexity compromises: with Victor's solution, the method definition uses a sophisticated polymorphic types, and call sites are lightweight. With this equally expressive solution, the definition is simpler, but call sites have to use an explicit coercion. As there is only one definition site and several call sites, it is generally preferred to have more complexity on the definition side, which is done by a supposedly expert library designer. In practice you'll find both styles in the wild, so it can be important to understand them both.

An historic remark, in reaction to what you seem to say in comments to Victor's reply: subtyping via explicit coercions and explicit universally quantified type variables are not recent additions to OCaml. Have a look at the Changes file of the OCaml distribution; the object system dates from OCaml 1.00 (from about 1995), subtyping (with explicit coercions) is present since around that time, and polymorphic methods and structure fields have been added to OCaml 3.05, released in 2002.

Edit: a remark prompted by comments. You may also write the following, using an object type annotation rather than a class type:

class classA2bis = object
  method f (b: < g : int; h : int >) = b#g + b#h
end ;;

I only used classB as it was already defined in your example, so there was not much use in using a structural annotation. In this context (the class type is used as a type, not to define another class type) the two are equivalent. They do not reveal anything about the implementation of the object b taken as parameter; given that OCaml's object system uses structural typing, any object having those two methods with the right types can claim to fit this type annotation (potentially through an explicit subtyping step); it may have been defined by someone else with absolutely no reference to your own class definitions.

In the ocaml object system there are relatively subtle distinctions between object types and class types, that I don't know much about -- I don't use object-oriented programming. If you wish, you can learn the details in the reference manual or the U3 book.

Edit 2: Note that #classB as 'a and classB are not equivalently expressive in general: the first, more complex formulation is useful when you want to express sharing between different occurences of the type. For example, 'a . (#foo as 'a) -> 'a is a very different type from foo -> foo. It is strictly more general, because it preserves strictly more information on the return type. In your case, though, both type are equi-expressive because there is only one occurence of the class type, so no potential sharing.