Re: [Caml-list] Signature monomorphism in functors

[Lauri Alanko <la@iki.fi>]

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