Including and re-exporting types as abstract

Learning
1

As a follow up to this discussion: Returning abstract types - #3 by zbaylin

Again, let’s say I have a similar GADT as before:

type 'a s =
  | Int : int s 
  | Float : float s

If I write a module type that contains a GADT wrapper for this type like so

module type S0 = sig 
  type t = A : 'a s -> t
end

and then write a function that takes an instance of one of these wrappers:

let f0 (type a) (module M : S0 with type t = a) (x : a) = ...

This fails to compile with the following error message:

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

This makes sense to me. I then tried making t private, which gives a similar error. This code, however, works as one would expect, since S0 is a subtype of S1:

module type S1 = sig
  type t
end

let f1 (type a) (module M : S1 with type t = a) (x : a) = ()

Is there a way to rewrite S1 such that it includes S0 but makes t abstract?

2

Your module S1 already includes S0, as you can check with

module M = struct
  type t = A (* having a GADT seems mostly irrelevant to the problem at hand *)
end
let f1 (type a) (module M : S1 with type t = a) (x : a) = ()
let () = f1 (module M) A
3

Ah, maybe I was unclear in my question, my mistake. I recognize that S0 ⊂ S1. My question is if it’s possible to write a version of this pseudocode:

module type S0 = sig
  type t = A
end

module type S1 = sig
  include S0 with type t abstract
end

The reason I ask is because I have some (relatively) complex module types that include this pattern (which is why I was using a GADT :slight_smile:):

module type T =
  type 'a t
  type wrapped_t = Wrap : 'a t -> wrapped_t
sig

I could obviously rewrite the module with type wrapped_t abstract, but would prefer not to have two signatures which express the same thing.

4

No, it is not possible to erase this kind of information. The reverse direction works

module type S1 = sig
  type wrapped_t = A: 'a t -> wrapped_t
  include S0 with type t := wrapped_t
end
5

To be honest, I do not really understand what you want to try to do. If you wrap your GADT in an existential, you just get a type equivalent to this two valued one:

type t = String | Int

So why do you want to use a GADT if, at the end, you finally use a plain ordinary variant?