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?
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);;
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.
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
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