[Caml-list] Signature monomorphism in functors

[Caml-list] Signature monomorphism in functors

[Lauri Alanko]

I stumbled into a limitation in functors:


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. It also seems to stem
directly from implementation limitations instead of any theoretical
problems.

I'd be interested in hearing if anyone has stumbled into this problem
earlier, and if there are any known workarounds. Also, are there any
plans to remove this limitation from the language?


Lauri

Re: [Caml-list] Signature monomorphism in functors

[rossberg]

> 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

Re: [Caml-list] Signature monomorphism in functors

[rossberg]

I wrote:
>   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)

(And my excuses for accidentally mixing Caml with SML syntax. :) Please read
"val" as "let" where appropriate.)

/Andreas

Re: [Caml-list] Signature monomorphism in functors

[Lauri Alanko]

On Tue, Jan 18, 2011 at 11:02:31AM +0100, rossberg@mpi-sws.org wrote:
> > 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)

> 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.

True enough. The real problem is that a functor forces one to fix a
single signature into which the argument module is narrowed.

Still, I think this is legitimately as surprising as the fact that in
Hindley-Milner, beta reduction doesn't reflect well-typedness:

((fun x -> x) 42, (fun x -> x) true) : int * bool

but a seemingly legitimate abstraction

(fun f -> (f 42, f true)) (fun x -> x) is ill-typed.

I guess what I want is "bounded signature polymorphism" of some sort:

module F(A : sig module type S <: S1 module M : S end) 
  : S3 with module M = A.M = 
struct
  module M = A.M
end

module M3B : S3 with module M = M2 = 
  F(struct module type S = S2 module M = M2 end)

Alas, there are no signature bounds in ocaml and I cannot offhand
think of a way to encode them.

>   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)

That's a good example. In fact I have always felt a bit uneasy about
the possibility of including an argument module. Now I know why.

For what it's worth, I figured out that for my current purposes, it
suffices if I simply do, for each subsignature S2 of S1:

module type S4 = sig
  module MM : S2
  include S3 with type M.t = MM.t
end

module F2(M_ : S2) : S4 with module MM = M_ = struct
  module MM = M_
  include F(M_)
end

module M3B : S4 with module MM = M2 = F2(M2)

I would have liked to shadow M with MM, but having to access it with a
different name is not too big of a deal for me, thankfully.


Lauri

Re: [Caml-list] Signature monomorphism in functors

[Jacques Garrigue]

On 2011/01/18, at 11:00, Lauri Alanko wrote:

> I guess what I want is "bounded signature polymorphism" of some sort:
> 
> module F(A : sig module type S <: S1 module M : S end) 
>  : S3 with module M = A.M = 
> struct
>  module M = A.M
> end
> 
> module M3B : S3 with module M = M2 = 
>  F(struct module type S = S2 module M = M2 end)
> 
> Alas, there are no signature bounds in ocaml and I cannot offhand
> think of a way to encode them.

You can always encode it by using an abstract module type:

  module type S1'  = sig type t  module type X  module X : X end

This way you can put anything you wish in X.
But this is going to be pretty heavy to use...

Alternatively, if you don't need all the functionality of modules,
objects let you do exactly that. A function from objects to objects may
be polymorphic in the available methods.

Jacques Garrigue

Re: [Caml-list] Signature monomorphism in functors

[rossberg]

Lauri Alenko:
>> Without coercive subtyping semantics, what would be the meaning of:
>>
>>   module A = F (struct val x = 2 val y = 3 end)
>
> That's a good example. In fact I have always felt a bit uneasy about
> the possibility of including an argument module. Now I know why.

Well, to be fair, the whole point of your original example was that you
wanted to do just that, albeit by slightly different means. ;-)

/Andreas