[Caml-list] GADT and local modules

[Thomas Braibant <thomas.braibant@gmail.com>]

Hi list,

I would like to find a way to name (or capture) the variables that are
existentially quantified in a GADT constructor, to put them inside a
module and apply a functor on the said module. Attached below is a
mockup of what I would like to have. (I can live without this coding
pattern, but I would like to know whether or not it is possible to
make it work, even if I suspect that the answer is no).

Best,
Thomas


type t = Pack : 'a * 'b list -> t

(* I want to unpack a t, and put its content in a module of signature S *)
module type S = sig
  type a
  type b
  val foo : (a * b) list
end

(* I want to apply the functor M on my module to produce a result,
whose type does not depend on the types in S.  I am using a functor as
a way to structure the computations that happen inside. I started with
a version without modules, which requires to write quite a few type
annotations... *)
module M (C:S) : sig val result : int end= struct

  include C

 (* Here I want bar to have type (a * b) list. Of course, I could have
bar s a function that takes two type variables as arguments, and a
list, and returns a list of the right type. *)
  let bar = List.rev foo
  let result = List.length bar

end

(* Here, I do not know of a way to retrieve the type variables
quantified in the GADT constructor Pack, to feed them in C *)
let f (t : t) =
  match t with
  | Pack l -> let module C = .... in M(C)

(* alternative with modules, which is not satisfying. *)

module type S = sig
  val t : t
end

module M (C:S) : sig val result : int end = struct

  include C

  (* Now, I can unpack the t locally in each function, but I cannot
     open the existential in the whole module, which is painful. *)

end