List of objects with a universally quantified method

Learning
1

The following code:

class foo =
  object
    method f : 'a. 'a -> string = fun _ -> "f"
  end

let bar : 'a. foo list -> 'a -> string list =
  fun foos x -> List.map (fun ff -> ff#f x) foos

yields the error message

This expression has type foo list but an expression was expected of type
  (< f : 'a -> 'c; .. > as 'b) list
Type foo = < f : 'a0. 'a0 -> string > is not compatible with type
  < f : 'a -> 'c; .. > as 'b 
The method f has type 'a. 'a -> string, but the expected method type was
'a -> 'b
The universal variable 'a would escape its scope

I don’t understand what the problem is. If I have a single foo, I can apply its method f to an argument of any type whatsoever, including the type 'a in bar. So why can’t I apply each element of a list of foos to an argument of that type?

2

I won’t claim to understand exactly what is going on but it’s a problem of the direction that type inference flows. If you just indicate that ff is of type foo it compiles fine.

class foo =
  object
    method f : 'a. 'a -> string = fun _ -> "f"
  end

let bar : 'a. foo list -> 'a -> string list =
  fun foos x -> List.map (fun (ff : foo) -> ff#f x) foos
3

Ok, that’s useful, thanks. The workaround I had found before was to define the mapped function separately, with a declared type, rather than inline.

4

Ah, and now with that hint I think I may also be able to guess why the first version doesn’t work. When the compiler sees a function that calls methods on some argument, it gives that function the most general possible type for the usages of those methods. So when it sees fun ff -> ff#f x, where x has type 'a, it infers that the method f must have type 'a -> 'c for some type 'c, and that therefore ff must be an object that has a method of this type, < f : 'a -> 'c; .. >. Thus the anonymous function has type < f : 'a -> 'c; .. > -> 'c. Then it infers from the known type of List.map that the second argument must have type < f : 'a -> 'c; .. > list.

The type variable 'c is existential and could get instantiated by anything, and the row variable .. could likewise get instantiated by any extra methods, so for instance we could supply here something of type < f : 'a -> string; g : int > list. But while the type < f : 'a -> 'c; .. > is “more general” than that of foo in an intuitive sense, since the method f of foo is required to be polymorphic rather than applying only to the type 'a in bar, this extra generality is not of the sort that the compiler knows how to deal with, so it complains. In other words, < f : 'a. 'a -> string > is not syntactically a subtype of < f : 'a -> string >, although semantically it could be.

(It probably would have been clearer to use different names for the essentially unrelated types 'a in foo and in bar; sorry about that.)

2 Likes