ext_101586 ([identity profile] wjl.livejournal.com) wrote in [personal profile] chrisamaphone 2009-11-19 07:21 am (UTC)

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!

Post a comment in response:

This account has disabled anonymous posting.
If you don't have an account you can create one now.
HTML doesn't work in the subject.
More info about formatting