Re: [Caml-list] Signature monomorphism in functors

[rossberg@mpi-sws.org]

> module type S1 = sig
>   type t
> end
>
> module type S2 = sig
>   include S1
>   val v : t
> end
>
> module type S3 = sig
>   module M : S1
> end
>
> module M2 : S2 = struct
>   type t = int
>   let v = 42
> end
>
> module M3A : S3 with module M = M2 = struct
>   module M = M2
> end
>
> module F(M_ : S1) : S3 with module M = M_ = struct
>   module M = M_
> end
>
> module M3B : S3 with module M = M2 = F(M2)
>
>
> Here, M3A compiles ok, but when I try to do the same thing through a
> functor, I get an error upon the definition of M3B:
>
> Error: Signature mismatch:
>        Modules do not match:
>          sig module M : sig type t = M2.t end end
>        is not included in
>          sig module M : sig type t = M2.t val v : t end end
>        Modules do not match:
>          sig type t = M2.t end
>        is not included in
>          sig type t = M2.t val v : t end
>        The field `v' is required but not provided
>
> I can kind of understand the problem: modules are implemented as
> records, and signature coercions are translated to record
> relayouts. The functor code expects the layout for S1, so the argument
> M2 : S2 gets coerced into S1 and thus the extra fields in S2 are
> hidden and cannot be exposed in the result of the functor.
>
> In my particular situation, this isn't a horrible problem, and I can
> live with F(M2) : S3 with type M.t = M2.t, since the module M2 with
> its extra fields is visible directly and doesn't need to be accessed
> through F(M2). But still, this seems like a very unintuitive
> limitation: abstracting a module member into a functor suddenly
> changed the expressivity of the program.

I disagree with this assessment: you can abstract the module just fine, as
long as you do it at the signature you were using it at, namely S2, not S1.
I don't think it should be surprising that you narrow the type of an
expression when you narrow the types of its free variables.

> It also seems to stem
> directly from implementation limitations instead of any theoretical
> problems.

I wouldn't say so. Coercive subtyping is not just an implementation detail,
it is an essential part of the language design and semantics, and visible in
other places. It might not be the only possible design, but it's not clear
what the alternatives would be, either. Consider for example:

  module F (X : sig val x : int end) =
  struct
    val y = 1
    include X
    val z = x + y
  end

Without coercive subtyping semantics, what would be the meaning of:

  module A = F (struct val x = 2 val y = 3 end)

Would it even be legal? If not, why not? And then consider the case where y
isn't a value but a type.

/Andreas