# First class modules and argument types

**URL:** https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210
**Category:** Learning
**Created:** [January 19, 2023, 7:33pm UTC](https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210 "2023-01-19T19:33:32Z")
**Posts on this page:** 6
**Page:** 1

<div class="post-metadata">

### Author: ![zbaylin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zbaylin/32/4047_2.png) [@zbaylin](https://discuss.ocaml.org/u/zbaylin)
#### Post date: [January 19, 2023, 7:33pm UTC](https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210/1 "2023-01-19T19:33:32Z")

</div>

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](https://discuss.ocaml.org/t/including-and-re-exporting-types-as-abstract/11183))

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

```ocaml
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:

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

```

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

```auto
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:

```ocaml
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:

```auto
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?

---

<div class="post-metadata">

### Author: ![yallop](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yallop/32/517_2.png) [@yallop](https://discuss.ocaml.org/u/yallop)
#### Post date: [January 19, 2023, 7:58pm UTC](https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210/2 "2023-01-19T19:58:11Z")

</div>

This is solved by [modular explicits](https://github.com/ocaml/ocaml/pull/9187):

```ocaml
let f {X: S} (E _ : X.existential) = ()

```

---

<div class="post-metadata">

### Author: ![zbaylin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zbaylin/32/4047_2.png) [@zbaylin](https://discuss.ocaml.org/u/zbaylin)
#### Post date: [January 19, 2023, 8:23pm UTC](https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210/3 "2023-01-19T20:23:19Z")

</div>

Ah thanks, @yallop 🙂 – 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?

---

<div class="post-metadata">

### Author: ![struktured](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/struktured/32/385_2.png) [@struktured](https://discuss.ocaml.org/u/struktured)
#### Post date: [January 19, 2023, 8:26pm UTC](https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210/4 "2023-01-19T20:26:36Z")

</div>

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

---

<div class="post-metadata">

### Author: ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)
#### Post date: [January 20, 2023, 12:50pm UTC](https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210/5 "2023-01-20T12:50:50Z")

</div>

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:

```ocaml
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:

```ocaml
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

```

---

<div class="post-metadata">

### Author: ![zbaylin](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/zbaylin/32/4047_2.png) [@zbaylin](https://discuss.ocaml.org/u/zbaylin)
#### Post date: [January 20, 2023, 2:54pm UTC](https://discuss.ocaml.org/t/first-class-modules-and-argument-types/11210/6 "2023-01-20T14:54:00Z")

</div>

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