Visitors, Functors, GADTs, and Weak Type Variables

Learning
1

I am playing around with trying to define a “dependent” version of visitors (à la Pottier) for GADTs, and I am running into an issue with OCaml type inference that I can’t figure out. Hopefully someone out there can explain it to me.

To set the scene, I have some GADT definitions, e.g.

type _ t0 = Z

type (_,_) t1 =
| A : ('a, 'a) t1
| B : ('a, 'b) t1 -> ('a, 'b t0) t1

type _ t2 =
| C : 'a t2
| D : 'a t2 -> 'a t0 t2

Now, I can write a function that recurses on a value of type ('a, 'b) t1 in order to transform a value of type 'a t2 into one of type 'b t2, as follows.

let rec foo : type a b . (a, b) t1 -> a t2 -> b t2 =
  function
  | A ->
    (fun x -> x)
  | B v ->
    let f = foo v in
    (fun x -> D (f x))

Now, using a visitor class defined within a functor, I am trying to “abstract” the recursion over ('a, 'b) t1 values, to produce values of some abstract type ('a, 'b) t, which I can then instantiate to some concrete type by applying the functor.

module Reduce (X : sig type ('a, 'b) t end) =
struct
  class ['self] reduce = object (self : 'self)
    method reduce_A : type a . (a, a) X.t =
      failwith "Must be overridden"
    method reduce_B : type a b . (a, b) X.t -> (a, b t0) X.t =
      failwith "Must be overridden"
    method reduce_t1 : type a b . (a, b) t1 -> (a, b) X.t =
      function
      | A ->
        self#reduce_A
      | B v ->
        let f = self#reduce_t1 v in
        self#reduce_B f
  end
end

However, when I try to “implement” the foo function by applying the functor, creating an object that overrides the methods appropriately, and then “extracting” the appropriate method, OCaml infers a type using weak type variables, even though the methods in the type inferred for the object appear to be appropriately generalised.

(* Why does OCaml only infer a type with weak type variables here? *)
(*   ('_weak1, '_weak2) t1 -> '_weak1 t2 -> '_weak2 t2 *)
let bar =
  let module M = Reduce(struct type ('a, 'b) t = 'a t2 -> 'b t2 end) in
  let obj = object (self)
    inherit [_] M.reduce as super
    method! reduce_A   = (fun v -> v)
    method! reduce_B f = (fun x -> D (f x))
  end in
  (* This is the type inferred for the object, methods have generalised types
      < reduce_A : 'a. 'a t2 -> 'a t2;
        reduce_B : 'a 'b. ('a t2 -> 'b t2) -> 'a t2 -> 'b t0 t2;
        reduce_t1 : 'a 'b. ('a, 'b) t1 -> 'a t2 -> 'b t2 >
  *)
  obj#reduce_t1

Can someone explain to me why this is happening?

EDIT: I just figured it out, reading this post. The definition of the function needs to be eta-expanded.

let bar v x =
  let module M = Reduce(struct type ('a, 'b) t = 'a t2 -> 'b t2 end) in
  let obj = object (self)
    inherit [_] M.reduce as super
    method! reduce_A   = (fun v -> v)
    method! reduce_B f = (fun x -> D (f x))
  end in
  obj#reduce_t1 v x
1 Like