Module type containing subtype

Learning
1

Is it possible to define a module type that contains a subtype of some known “super” type (sorry for the mouthful).

Here’s a quick example of what I mean:

type super = [ `A | `B | `C ]

module type S = sig
  type sub (** Want to constrain this to be [< super] *) 
end

module M : S = struct
  type sub = [ `A | `B ]
end

module N : S = struct
  type sub = [ `A ]
end

This will compile, but { M | N }.sub will be abstract. I was thinking this might be possible with constraints, i.e.

module type S = sig
  type 'a sub = [< super ] as 'a
end

module M : S = struct
  type 'a sub = [< `A | `B ] as 'a
end

module N : S = struct
  type 'a sub = [< `A ] as 'a
end

But this doesn’t work (I assume) since we can’t know 'a for arbitrary instances of (module S).

Is there a way to achieve this kind of subtyping that I’m missing?

1 Like
2

You can use a private row type in the signature S:

type super = [ `A | ` B ]
module type S = sig type t = private [< super ] end
module M : S= struct
  type t = [ `A ]
end
3 Likes
3

Thanks @octachron, this is exactly what I was looking for. Is there any way to convince the compiler that for some module M : S that M.t is a polymorphic variant? I.e. is it possible to do something like

module Make (M : S) = struct
  let f : super -> unit = function
    | #M.t -> print_endline "got M.t"
    | _ -> print_endline "got super"
end

This might include too much to be known at compile time, so not sure if it’s actually possible.

4

The pattern #M.t refers to the definition of the type t which is not a simple polymorphic variant definition. However, you can expose the pattern matching in M itself with:

type super = [ `A | ` B ]
module type S = sig
  type t = private [< super ]
  val case: t:(t -> 'a) -> other:(super -> 'a) -> t ->  'a
end
module M: S = struct
  type t = [  `A ]
  let case ~t ~other x = match (x: t :>super) with
  | #t as x -> t x
  | x -> other x
end
let test = M.case
  ~t:(function 
       | `A -> Format.printf "got A" 
       | `B -> Format.printf "Impossible" )
  ~other:(function
      | _ -> Format.printf "Other")
5 Likes
5

Awesome, thanks again. That’s similar to a method I had thought of

module type S = sig
  ...
  val narrow : super -> sub option
end

let f : int -> super = ...

module Make (M : S) = struct
  let g : int -> sub option = fun i -> i |> f |> M.narrow  
end