Constraining a generic value to a module

Hi,

I’d like to attach a module to a generically to a record.

module type X_int = sig 
    val x : int 
end

module Three: X_int = struct let x = 3 end

module Test = struct
    let three = (module Three: X_int);
    type 'a rec1 = {
        x: int;
        y: 'a
    }
    let a = {x = 2; y = three}

end

the above code works however I’d like to restrict the generic parameter 'a to a specific module. Something like this

    type 'a rec1 = {
        x: int;
        y: (module 'a: X_int)
    }

but this doesn’t work. Is there a way to express such a thing?

Do you want something like

module type pack = sig type t val x:t end
type 'a rec2 = { x: int; y: (module pack with type t = 'a) }

?

Otherwise

type rec1 = { x: int; y: (module X_int) } 

is perfectly valid but there is no free type parameter in this record definition.

Hey,

thx for the answer. It’s certainly a possible solution to a subset of what I have in mind.
assume this module structure

module type pack = sig type t val x:t end
module type extended_pack = 
    sig
       include pack
       val someOperation: pack.t -> pack.t
    end

type 'a rec2 = { x: int; y: (module pack with type t = 'a) }

So i want to be able to put anything that conforms to packs interface which means also extended_packs

There is still no obstacles here: since extended_pack is a subtype of pack; any module implementing
extended_pack can be packed as a (module pack). It is also perfectly possible to restrict first-class modules themselves

let conv (type a) (module M: extended_pack with type t = a) = 
  (module M: pack with type t = a);;
2 Likes

As @octachron rightly tells, you can do this, as extended_pack is a structural subtype of pack. However, the structural subtyping relies on a subsumption rule, that forgets the extension of the extended_pack, roughly it upcasts it, e.g.,


type 'a pack = (module pack with type t = 'a)
type 'a extended_pack = (module pack with type t = 'a)
type 'a packed = {
   x : int;
   y : 'a pack;   (* forall 'a s.t. 'a implements pack *)
}

(* a higher rank identity, needs explicit type annotations *)
let forget : type t. t extended_pack -> t pack =
  fun (module M) -> (module M)

let do_stuff : type t. t packed -> t = fun {x; y = (module P)} ->
      let works = P.x in
      (* let doesn't_compile = P.someOperation P.x in *)
      works

(* let's play more *)
let admit = assert false
let p1 : int pack = admit
let p2 : int extended_pack = admit
let checks : bool = p1 = forget p2 (* with an explicit upcast *)
(* let fails : bool = p1 = p2  -- doesn't work without an explicit upcast *)
let packed = {x = 0; y = forget p2}
(* let fails : int extended_pack = packed.y -- no downcasting *)

In other words, once you put the extended pack into the pack slot, you can only access the base interface. If you need to preserve it, you need to rely on row polymorphism, i.e., use polymorphic records, aka objects.

2 Likes

@ivg wow. thx for the answer.

How would a solution look like using row polymorphism?

Polymorphic records are like modules, in a sense that they both represent tuples of values that are structurally typed (i.e., ducked typed), the main difference is that polymorphic records provide a mechanism to capture an extension in a row variable and assign it to a type variable or to an anonymous abstract type, e.g., in a type definition type 'a duck = 'a constraint 'a = <quacks : unit; ..> the type variable 'a ranges over a set of types that quacks and do whatever they want. There is an option to capture the row type in a private abstract type, see the Private row types: abstracting the unnamed paper by Jacques Garrigue for more thorough explanation.

Below is a re-implementation of an example above with objects instead of modules, enjoy :slight_smile:

module Row = struct
  class type pack = object
    method op1 : unit
  end

  class type ext_pack = object
    inherit pack
    method op2 : unit
  end

  type +'a packed = {
    x : int;
    y : 'a;
  } constraint 'a = #pack


  let admit = assert false

  let p1 : pack = admit
  let p2 : ext_pack = admit

  (* we still need an explicit upcast, though now it is built in *)
  let checks = p1 = (p2 :> pack)

  let packed1 = {x = 42; y = p1}

  (* we can put a bigger class into the y slot,
     and its type is not forgotten *)
  let packed2  = {x = 42; y = p2}

  (* no problem with calling it. *)
  let () = packed2.y#op2


  (* even bigger than ext_pack *)
  let p3 : #ext_pack = admit

  let packed3 = {x = 42; y = p3}

  let checks = p1 = (p3 :> pack)

  (* though we can put them in the same list, we need to forget the
     type, as lists are monomorphic *)
  let listable = [
    p1;
    (p2 :> pack);
    (p3 :> pack)
  ]

  (* the packs could also be put, since 'a is covariant *)
  let packs_listable = [
    packed1;
    (packed2 :> pack packed);
    (packed3 :> pack packed)
  ]
end
1 Like