How to cause functor types to "inherit" their elements' polymorphic variant subtyping relations

Learning
1

The following is a minimal example of the shape of what’s proven to be a very stubborn problem for me. Thanks in advance to everyone that takes the time to read this and maybe help get me unstuck. :slight_smile: A link to the full code shown here is at the end.

Presume you have some number of polymorphic variant types, with natural subtyping relationships, e.g.

type a = [ `A of int ]
type b = [ a | `B of int ]

Those relations flow through nicely to things like List.t and other types that are defined with type parameters either explicitly marked as covariant or inferred as such, e.g.

let pair (a : a) (b : b) = ([a] :> b list) @ [b]  (* works fine *)

However, I have some data structures that need some helper functions suitable to the types they are to contain. The most natural and typesafe way to set this up seemed to be to define each data structure as a functor, and have the contained type and helper functions provided by an argument:

module type Config = sig type t end

module type Box = sig
  module C : Config
  type t = { regions : C.t list }
  val empty : t
  val add : C.t -> t -> t
  val get : t -> C.t list
end

module Box (C: Config) : Box with type C.t = C.t = struct
  module C = C
  type t = { regions : C.t list }
  let empty = { regions = [] }
  let add r box = { regions = r :: box.regions }
  let get box = box.regions
end

module ABox = Box(struct type t = a end)
module BBox = Box(struct type t = b end)

(Of course the actual functor argument type is much more than just the member type; just presume the real-world analogue of Box uses a bunch of functions provided by Config.)

This approach has been working just fine for me for months. However, I now need to be able to treat the more constrained instances of these data structures as if they were more general (just as pair above did in coercing a list :> b list). Alas:

(* Error: Type ABox.t is not a subtype of BBox.t *)
let join (abox : ABox.t) = BBox.get (abox :> BBox.t)

FWIW, feedback I’ve gotten in irc mostly gives me the impression that I’m fairly misguided either in my use of modules and functors or in my expectations w.r.t. OCaml’s type system (specifically, the degree to which polymorphic variant subtyping relations can or should affect subtyping relations of higher-order types). Accomplishing this sort of thing is generally pretty straightforward in other languages (granted, perhaps due to various unsoundness there); any suggestions as to how to accomplish what I’ve described here (or maybe confirmation that I am actually misguided) would be greatly appreciated.

1 Like
2

In your example ABox.t is not a subtype of BBox.t because, despite they have the same name, ABox.regions and BBox.regions are not the same record field. If you just define your functor result type with type t = C.t list, then the coercion will work. What you need to say is that the type t resulting from your functor application is the application of a covariant parametric type +'a f. For instance:

type +'a f = {regions : 'a list}

module type Box = sig
  module C : Config
  type t = C.t f
  val empty : t
  val add : C.t -> t -> t
  val get : t -> C.t list
end

module Box (C: Config) : Box with module C = C = struct
  module C = C
  type t = C.t f
  let empty = { regions = [] }
  let add r box = { regions = r :: box.regions }
  let get box = box.regions
end

module ABox = Box (struct type t = a end)
module BBox = Box (struct type t = b end)

(* now the coercion works *)
let join (abox : ABox.t) = BBox.get (abox :> BBox.t);;
val join : ABox.t -> b list = <fun>
1 Like
3

Thank you.

I tried doing this, e.g. via

  type +'a bt = { regions : 'a list }
  type t = C.t bt

…but always entirely within Box. I never thought to define the functor’s essential type outside of the functor!

I wonder if there are any materials aside from the usual books and such that talk about good OCaml design, data modeling techniques, etc? I should be able to arrive at this solution independently, but honestly not sure I ever would have. I feel like I have some big gaps in my design intuition given the tools available in OCaml, and prior experience elsewhere seems like more of a hindrance than help.

I’m off to apply this to real code. Thanks again!

2 Likes
4

I’m not aware of such materials, but I can explain where was your error in such a way you could find the solution in the future for similar case.

The problem with your solution was not particular to subtyping, but was due to incompatible and distinct types. When you define variants (not polymorphic ones) and records in modules, the modules behave as namespaces. Hence these two types are distinct:

module A = struct type t = {r : int} end
module B = struct type t = {r : int} end

Here, A.t and B.t are two distinct types:

let v = A.{r = 1};;
val v : A.t = {A.r = 1}

v.B.r;;
Error: The field B.r belongs to the record type B.t
       but a field was expected belonging to the record type A.t

This is what append with your two types ABox.t and BBox.t. If we put your covariant polymorphic type inside the module we have something like:

module ABox = struct
  type +'a f = {records : 'a list}
  type t = a f
end

module BBox = struct
  type +'a f = {records : 'a list}
  type t = b f
end

Here, for the same reason than above, ABox.f and BBox.f are distinct and incompatible parametric types. So ABox.t can’t be a subtype of BBox.t. However, ABox.t is a subtype of b ABox.f

let (v : ABox.t) = ABox.{records = [`A 1]};;
val v : ABox.t = {ABox.records = [`A 1]}

(v :> b ABox.f);;
- : b ABox.f = {ABox.records = [`A 1]}

but v is not a member of a BBox.f:

(v : a BBox.f);;
Error: This expression has type ABox.t = a ABox.f
       but an expression was expected of type a BBox.f

Basically, with your functor what you said is:

  • for every config module C, there is a covariant parametric type f such that…

but, what you wanted to say is:

  • there is a covariant parametric type f such that for every config module C…

In the first case (your solution) f depends on your configuration module and is not necessarily the same for two distinct configuration modules. In the second case (the right solution), f is independent of the configuration module (the functor parameter) and, as so, it preserves the subtyping relation.

This is the same situation with the proposition everybody loves somebody: do we mean that there is someone that everybody loves, or that each one loves a distinct and specific person?

I do not know if everybody loves somebody but, as Jack and Elwood Blues said: everybody needs somebody to love. And I hope that now you can see the light :smiley:

3 Likes
5

Outstanding explanation; thank you again. :smiley: