Generative Functors

Learning
1

The explanation in Section 8.21 Generative Functors of the OCaml Manual gives the impression that using () or struct end as functor argument make a functor generative. The code below makes me suspect that any functor argument that is not a named module makes a functor generative. What are the details here?

module X (E: sig type x end): sig 
  type t 
  val t: t 
end = struct 
  type t = int 
  let t = 0 
end

module X1 = X (struct type x = int end)
module X2 = X (struct type x = int end)

module E = struct
  type x = int
end

module X1' = X (E)
module X2' = X (E)
  • Types X1.t and X2.t are incompatible – X is generative
  • Types X1'.t anf X2'.t are compatible – X is not generative
2

I think the right thing to say is that, first, generativity is a property of the functor itself, not of any particular application of that functor; in particular, your functor X is applicative since it doesn’t have any () parameter.

Second, what’s happening in your X1 and X2 is that the parameters are two different modules (even though they happen to have the same implementation), so that the resulting modules contain different types. EDIT: You can see the same behavior if you bind module P1 = struct type x = int end and module P2 = struct type x = int end and then apply X to P1 and P2.

However, I’m no module expert, so take this with a grain of salt until one comes along.

2 Likes
3

The semantic of functor in OCaml is applicative : a functor applied to the same path always returns compatible abstract types. But if you apply to anonymous structure, it will return incompatible abstract types. This is distinct to the semantic of functors in SML where functors are always generative (X1'.t and X2'.t will be incompatible in SML).

This extension is just a kind of syntactic sugar to have generative functors in OCaml when applied to the same path.

module type S = sig type t val x : t end

module F (M : sig end) : S = struct
  type t = int
  let x = 1
end

module F_gen (M : sig end) () : S = F (M)

module E = struct end;;
module E : sig  end

module X1 = F (E);;
module X1 : sig type t = F(E).t val x : t end

module X2 = F (E);;
module X2 : sig type t = X1.t val x : t end

module X1' = F_gen (E) ();;
module X1' : S

module X2' = F_gen (E) ();;
module X2' : S

here X1.t and X2.t are compatible, but X1'.t and X2'.t are not.

You can read this Xavier Leroy’s paper (section 1 and 2) to understand the motivation behind applicative semantic.

5 Likes