Is there a technical good reason functor application should be generative?
Yes: sometimes it's what you want. Suppose the result signature of a functor has some abstract type t which, under the hood, is represented by some stateful thing like a reference, or keys into a lookup table, or something like that. The implementor of such a functor might reasonably hope that clients won't be able to get t's from some other instantiation of the functor which -- although its type component is equal -- has a different reference or a different lookup table on the inside.
Here's a simple example illustrating the problem:
module type TABLE =
sig
type t
val x : t
val get : t -> int
val inc : t -> unit
end
module I = struct let x = 5 end
module AppTable(X : sig val x : int end) : TABLE =
struct
type t = int ref
let x = ref X.x
let get y = !y
let inc y = incr y
end
Now suppose we say
module M = Table(I);;
module N = Table(I);;
Now certainly we both agree that M.t and N.t are equal types, namely both int ref, but they have different invariants, since they are inhabited by different int ref values! But i can do all sorts of nefarious things like N.get M.x and M.inc N.x, and in a more involved setting like the lookup table keys i alluded to, in some cases this violation of abstraction might result in a run-time error.
As far as i can tell, there is no way to obtain implementor-side guarantees like this from O'Caml's applicative functors. Interestingly, you can always make the two types actually different by sealing the two modules, e.g.:
module M : TABLE = AppTable(I);;
module N : TABLE = AppTable(I);;
but this pushes the resolution to the client-side -- i.e. the client of the module has to realize the extra sealing is necessary to ensure the proper invariants are maintained. If you can find a way to enforce this guarantee on the implementor's side in O'Caml, i'd love to see it!
no subject
Yes: sometimes it's what you want. Suppose the result signature of a functor has some abstract type t which, under the hood, is represented by some stateful thing like a reference, or keys into a lookup table, or something like that. The implementor of such a functor might reasonably hope that clients won't be able to get t's from some other instantiation of the functor which -- although its type component is equal -- has a different reference or a different lookup table on the inside.
Here's a simple example illustrating the problem:
Now suppose we say
Now certainly we both agree that M.t and N.t are equal types, namely both int ref, but they have different invariants, since they are inhabited by different int ref values! But i can do all sorts of nefarious things like
N.get M.x
andM.inc N.x
, and in a more involved setting like the lookup table keys i alluded to, in some cases this violation of abstraction might result in a run-time error.As far as i can tell, there is no way to obtain implementor-side guarantees like this from O'Caml's applicative functors. Interestingly, you can always make the two types actually different by sealing the two modules, e.g.:
but this pushes the resolution to the client-side -- i.e. the client of the module has to realize the extra sealing is necessary to ensure the proper invariants are maintained. If you can find a way to enforce this guarantee on the implementor's side in O'Caml, i'd love to see it!