How to type a forwarding function?

I’m not sure if below is the minimal code example, but what I’m trying to accomplish is the function k below, which takes a function and a first-class module, and the function is just a forwarding function for something in the first-class module. I want to give these forwarding functions a type but I don’t want to expose the 't type variable because it is not really necessary, I’m just trying to enforce the relationship in the forwarding function.

Is this possible?

The error is:

This expression has type (module FOO with type t = F.t)
but an expression was expected of type (module FOO with type t = $V_'t)
Type F.t = t is not compatible with type $V_'t
module type FOO = sig
  type t
  val get : unit -> t
  val bar : t -> string
end

module Fimpl : FOO = struct
  type t = int
  let get () = 4
  let bar = string_of_int
end

type 'a f = V : ((module FOO with type t = 't) -> 't -> 'a) -> 'a f

let bar (type t) (module F : FOO with type t = t) (t:t) =
  F.bar t

let k (type t) (V f) (module F : FOO with type t = t) =
  let t = F.get () in
  f (module F) t

let () = ignore (k (V bar) (module Fimpl))
1 Like

The short answer is that you need a universal quantifier for 't, not an existential one. We can swap your GADT out for a record field to achieve that:

type 'a f = { f : 't. ((module FOO with type t = 't) -> 't -> 'a) }

let bar (type t) (module F : FOO with type t = t) (t:t) =
  F.bar t

let k (type t) { f } (module F : FOO with type t = t) =
  let t = F.get () in
  f (module F) t

let () = ignore (k { f = bar } (module Fimpl))

Your definition of f – with the existential binding for 't – means that any given 'a f is a forwarding function for values of some type 't that was known at construction time but is not recovered via pattern matching. The error message is complaining about this: the specific existentially-bound type $V_'t might not equal F.t as far as the type checker is concerned.

Switching 'a f to use a universal quantifier for 't flips this around: the consumer of the 'a f value gets to pick whichever instantiation they want, and the provider must show that they are compatible with any possible choice by passing a polymorphic function. (This seems to be the semantics you want.)

Hope this helps.

2 Likes

Thank you very much! I never would have come across that on my own. That solves my type issues! And thank you for the explanation.

1 Like