First class modules and argument types

Learning
1

I’ve been playing around more with first-class modules and came across this particular use case (briefly mentioned in Including and re-exporting types as abstract)

If you have a module signature with a non-abstract type, i.e.

module type S = sig
  type 'a t
  type existential = E : 'a t -> existential
end

and you want to write a function that takes a module S and an S.existential, there are a couple of ways that I thought about achieving this:

let f (module M : S) (v : M.existential) = ()

This seems like it should work, but doesn’t:

Error: This pattern matches values of type M.existential
but a pattern was expected which matches values of type 'a
The type constructor M.existential would escape its scope

And it’s kind of easy to see why: how would one write a type signature for this function? I don’t think it’s doable.

Another thought I had was to use locally abstract types:

let (type e) (module M : S with type existential = e) (v : e) = ()

This also doesn’t work, since M.existential is not abstract, and so we get:

Error: In this `with' constraint, the new definition of existential
does not match its original definition in the constrained signature:
Type declarations do not match:
  type existential
is not included in
  type existential = E : 'a t -> existential
Their kinds differ.

Is there any way to write the function like this without packing the arguments into another module?

2

This is solved by modular explicits:

let f {X: S} (E _ : X.existential) = ()
2 Likes
3

Ah thanks, @yallop :slight_smile: – that seems to be exactly what I’m looking for. I assume this wouldn’t get backported to 4.x versions of the compiler if and when it gets merged?

4

Based on the fact the PR is 90+ commits, I seriously doubt they will backport it.

1 Like
5

It is a new feature, we don’t backport new features to old versions of the compiler. Also this is not the kind of work that converges quickly, I don’t think it really makes sense to mention it as a solution for a current issue.

A current work-around is to decompose the equations on the exported type of the packed modules in two:

type (_,_) eq = Refl: ('a,'a) eq
module type S = sig
  type 'a t
  type existential = E: 'a t -> existential
  type export
  val eq: (export,existential) eq
  val print: 'a t -> unit
end
let f (type x) (module M: S with type export = x) (x:x) =
  let Refl = M.eq in
  let E x = x in
  M.print x

However, beware that for this toy example this is complexity for the sake of complexity. The code above is equivalent in term of features to the much simpler version where we erase all information about 'a t from the packed module:

module type S = sig
  type existential
  val print: existential -> int
end
let f  (type x) (module M: S with type existential=x) x = M.print x
3 Likes
6

Thanks @octachron! Using equality witnesses is a simple solution I hadn’t considered :slight_smile: