First class modules and GADT existentials

Learning
1

I’d like to pack a module operating on a type and a value of that type.

module type T = sig 
  type t 
  val op : t -> int
end

type t = V : (module T with type t = 'a) * 'a -> t

Now I’d like to provide an API that hides the fact that we are operating on the pack:

module M : sig
  type nonrec t = t
  val op : t -> int
end = struct
  type nonrec t = t 

  let _op (type r) t v = 
    let module M = (val t : T with type t = r) in
    M.op v 

  let op (V (t, v)) = _op t v  
end

Writing the implementation is a bit tedious, I only managed to write it by defining two functions for typing reasons. Is there a bit of syntax/annotation that I’m missing that could streamline this ?

2

What makes you think you need to annotate so much? This works fine:

module M : sig
  type nonrec t = t
  val op : t -> int
end = struct
  type nonrec t = t
  let op (V ((module M),v)) = M.op v 
end

That being said, you are emulating crapy objects by combining GADTs and first class modules. You would be better off just using the real deal. :slight_smile:

4 Likes
3

Ah thanks ! I was missing the fact I could directly match the (module M).

4

Even if you don’t, this would work fine as well:

let op (V (t,v)) = let module M = (val t) in M.op v

Type annotations on module unpacking is needed only when the typechecker doesn’t already know the type. But here, it comes from the argument of V, so the type is well known.

What you were missing is a way to grab the name of the existential type variable, which is indeed annoying … but you don’t need it here, you can rely on unification.

1 Like