A question on type/module equality

Learning
, ,
#1

Dear all,

I have a likely newbie question on the module system, assume this program:

module U : sig type t            end = struct type t = int      end
module S : sig type t = C of U.t end = struct type t = C of U.t end
module T = struct
  type s = S.t =
    | C of U.t
end

module API : sig
  module U : module type of U
  module S : module type of S

  module T : sig
    type s = S.t
    (* = C of U.t *)
  end

end = struct
  module U = U
  module S = S
  module T = T
end

Up to this point, everything goes OK, however, if I uncomment the C of U.t bit, then OCaml complains with

This variant or record definition does not match that of type S.t
The types for field C are not equal.

That’s fairly strange as ocamlc -i gives me the interface for the original version:

module U : sig type t end
module S : sig type t = C of U.t end
module T : sig type s = S.t = C of U.t end
module API :
  sig
    module U : sig type t end
    module S : sig type t = C of U.t end
    module T : sig type s = S.t end
  end

which in principle compiles fine if I add the type constraint. Thanks!

#2

This a problem of name catpure: U.t refers to two different types within the program.
More precisely, the problem starts at that line

module S : sig type t = C of U.t end = struct type t = C of U.t end

Here, the definition of S.t captures the concrete type U.t defined at line 1.
Contrarily when defining the submodule API.T

module T : sig
  type s = S.t = C of U.t
end

U.t refers to the submodule API.U defined at line 9. There is therefore a type error since S.t =C of U[line 1].t ≠ C of U[line 9].t.

That’s fairly strange as ocamlc -i gives me the interface for the original version:

Unfortunately, the interfaces printed by ocamlc -i are not always equal to the interface actually inferred by the compiler due to these problems of name capture. Using a version of the compiler patched to make these problems more explicit yields for ocamlc -i test.ml:

Warning 63: The printed interface differs from the inferred interface.
The inferred interface contained items which could not be printed
properly due to name collisions between identifiers.
File “test.ml”, line 9, characters 2-29:
Definition of module U/1
File “test.ml”, line 1, characters 0-67:
Definition of module U/2
Beware that this warning is purely informational and will not catch all
instances of erroneous printed interface.

module U : sig type t end
module S : sig type t = C of U.t end
module T : sig type s = S.t = C of U.t end
module API :
sig
module U : sig type t end
module S : sig type t = C of U/2.t end
module T : sig type s = S.t end
end

3 Likes
#3

Oh indeed I see it now, thanks @octachron; I was not sure how references to types where resolved when using module type of and now I see they are preserved, however the printing confused me indeed. I will have to add the proper equalities then.

#4

More generally; I often find myself wanting to “reuse” module types but wishing they would resolve type references using dynamic scoping.

#5

I don’t know in which context you want to use such a pattern, but maybe you can transform the outer modules S ans T into functors to capture the dependency with U.t. This example compile :

module U : sig type t end = struct type t = int end
module S (U : module type of U) : sig type t = C of U.t end = struct
  type t = C of U.t
end
module T (U : module type of U) = struct
  type s = S(U).t = C of U.t
end

module API : sig
  module U : module type of U
  module S : module type of S(U)

  module T : sig
    type s = S.t
     = C of U.t
  end

end = struct
  module U = U
  module S = S(U)
  module T = T(U)
end

I’ve never met the syntax type s = S.t = C of U.t before this thread, what is its rationale ? Why not simply write type s = S.t ?

#6

This syntax allows to re-export constructor or record field names. For instance,

module M = struct type t = A end
type t = M.t
let x = A

fails with

Error: Unbound constructor A

whereas

module M = struct type t = A end
type t = M.t = A
let x = A

works.

2 Likes
#7

Thanks for the hint, indeed I could use functors, but here I am in the context of trying ot make “a module overlay” over a large existing codebase so functorializing hundreths of modules is not an option ATM.

#8

Thanks for the explanations. Indeed, this is a useful feature.

#9

This is just a kind of eta-expansion.

let i = 1
let j = succ i

(* vs *)

let i = 1
let j_closed i = succ i
let j = j_closed i

You had a module expression (namely S) with a free variable (namely U), the trick is to bind the free variable in a functor and then apply it.

Is it in Coq code base ? Maybe you can consider to write (not a the moment) an automatic rewriting tool to expand all modules with free variables.

#10

Indeed that’s in the Coq codebase. I would like to redeclare signatures in order to better organize them, so if I have:

module A : sig type t end
module B : sig type t = A.t end

I would like to have a new API.A.t and redeclare API.B.t such that it refers to API.A.t and the equality is lost (as to ensure encapsulation). However it looks like either functors should be used or some custom tool (that I’m not willing to write :D)

#11

I’m not sure I understand your intention : do you want to hide the equality between API.A.t and API.B.t (and ensure encapsulation) or do you want to show it ? In the example of you first message the equality is known outside the API module.

BTW, you can achieve what you try to do in your first message without functors but you have to not use module type of and rewrite explicitly the signature of each modules, as in this example :

module API : sig
  module U : sig type t end
  module S : sig type t = C of U.t end
  module T : sig
    type s = S.t
    = C of U.t
  end

end = struct
  module U = U
  module S = S
  module T = T
end

In either case (functors + module type of or rewrite signatures) you’ll have a lot of code to write if you have hundreds of modules; or you have to face up the toolsmith problem : “I’d rather write programs to write programs than write programs” :stuck_out_tongue: .

#12

Indeed we want to hide the equality of A.t and API.A.t.

Thanks for the example, this is indeed the actual solution [file] we are using, but obviously induces a lot of maintenance pain as you point out.

#13

Ok, I better understand what you want. This is indeed the case A.t and API.A.t are not compatible types, as we can see in this example :

module A : sig 
  type t 
  val v : t
end = struct
  type t = A
  let v = A
end

module API : sig
  module A : module type of A
end = struct
  module A = A
end

A.v = API.A.v;;
Error: This expression has type API.A.t but an expression was expected of type
           A.t

I don’t see how you can do what you want without manually write this .mli file. For example, the Univ.Level module and the API.Univ.Level one don’t have the same signature. If the use of module type of worked, the modules would have the same signature.