Is it possible to constrain a functor module parameter in this case?

Learning
,
1

Consider the following code:

module type A = sig
  type 'a repr
  val f : string -> 'a repr
end

module type B = functor (X:A) -> sig
  type 'a repr
  val g : _ X.repr -> 'a repr
end

(* Example doesn't care what 'a repr really are. *)
module Example(XA:A)(XB:B) = struct
  open XA
  open XB(XA)
  let expr () = g (f "foo")
end

where modules A and B describe representations and B depends on A. As you can see, Example is an actual expression using those representations but it’s independent on what the actual representations really are (this is inspired by tagless-final optimizations article: http://okmij.org/ftp/tagless-final/course/optimizations.html). For example, A could be expressions and B could be statements.

Now, if I try to write interpreters for A and B for, say, printing the expression in Example:

module AInstance = struct
  type 'a repr = string
  let f s = Printf.sprintf "AInstance.f(%s)" s
end

(* Here, 'a A.repr must be a string for this module to make sense.
 * Is there a way to constrain it? *)
module BInstance(X:A) = struct 
  type 'a repr = string
  let g s = Printf.sprintf "BInstance.g(%s)" s
end

let ()  =
  let module M = Example(AInstance)(BInstance) in
  print_endline (M.expr ())

the compiler complains about a signature mismatch:

File "b.ml", line 31, characters 36-45:
31 |   let module M = Example(AInstance)(BInstance) in
                                         ^^^^^^^^^
Error: Signature mismatch:
       Modules do not match:
         functor (X : A) ->
           sig type 'a repr = string val g : string -> string end
       is not included in
         B
       At position functor (X) -> <here>
       Modules do not match:
         sig type 'a repr = string val g : string -> string end
       is not included in
         sig type 'a repr val g : 'b X.repr -> 'a repr end
       At position functor (X) -> <here>
       Values do not match:
         val g : string -> string
       is not included in
         val g : 'a X.repr -> string
       File "b.ml", line 8, characters 2-29: Expected declaration
       File "b.ml", line 27, characters 6-7: Actual declaration

Is there a way to constrain or hint that BInstance actually implements B? Thanks.

2

The problem is that the type of BInstance is genuinely not B because it does not accept all modules of type A as argument.

You need to refine the type of example by expressing the fact that your second functor is allowed to only work on module types with type constructor repr equal to A.repr.

A first step may need to write the corresponding type by hand:

module Example(XA:A)(XB: functor (X: A with type 'a repr = 'a XA.repr) ->
  sig
    type 'a repr
    val g : _ XA.repr -> 'a repr
  end) = struct ... end

since the module type of XB is a bit long, you can use a separate functor to compute it:

module Btype(XA:A) = struct
  module type t =
    functor (X: A with type 'a repr = 'a XA.repr) ->
    sig
      type 'a repr
      val g : _ XA.repr -> 'a repr
    end
end
`
module Example(XA:A)(XB: Btype(XA).t) = struct ... end
1 Like
3

You could also do something like



module type A = sig
  type 'a repr
  val f : string -> 'a repr
end

module type B = sig
  module X : A
  type 'a repr
  val g : _ X.repr -> 'a repr
end

(* if you use "= XA" instead of ":= XA" you need to add "module X = AInstance" in the definition of BInstance *)
module Example(XA:A)(XB:B with module X := XA) = struct
  open XA
  open XB
  let expr () = g (f "foo")
end


module AInstance = struct
  type 'a repr = string
  let f s = Printf.sprintf "AInstance.f(%s)" s
end

module BInstance = struct
  type 'a repr = string
  let g s = Printf.sprintf "BInstance.g(%s)" s
end

let ()  =
  let module M = Example(AInstance)(BInstance) in
  print_endline (M.expr ())
1 Like