From mboxrd@z Thu Jan  1 00:00:00 1970
Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104])
	by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p0ICAhBW017951
	for <caml-list@sympa-roc.inria.fr>; Tue, 18 Jan 2011 13:10:43 +0100
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AhYBAKoRNU2A1gkBhWdsb2JhbACWQI4tAQEBCgsKGAUfwjSFUAQ
X-IronPort-AV: E=Sophos;i="4.60,339,1291590000"; 
   d="scan'208";a="73398513"
Received: from courier.cs.helsinki.fi (HELO mail.cs.helsinki.fi) ([128.214.9.1])
  by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 18 Jan 2011 13:10:37 +0100
Received: from melkinpaasi.cs.helsinki.fi (melkinpaasi.cs.helsinki.fi [128.214.9.14])
  (AUTH: PLAIN cs-relay, TLS: TLSv1/SSLv3,256bits,AES256-SHA)
  by mail.cs.helsinki.fi with esmtp; Tue, 18 Jan 2011 14:10:36 +0200
  id 00093F11.4D35833C.000066DF
Received: by melkinpaasi.cs.helsinki.fi (Postfix, from userid 37211)
	id 86F898241F; Tue, 18 Jan 2011 14:10:36 +0200 (EET)
Date: Tue, 18 Jan 2011 14:10:36 +0200
From: Lauri Alanko <la@iki.fi>
To: caml-list@inria.fr
Message-ID: <20110118121036.GK323@melkinpaasi.cs.helsinki.fi>
References: <20110118020018.GI323@melkinpaasi.cs.helsinki.fi>
 <7f9a42a3cac8ea539f9f48432cd8a5af.squirrel@mail.mpi-sws.org>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
In-Reply-To: <7f9a42a3cac8ea539f9f48432cd8a5af.squirrel@mail.mpi-sws.org>
User-Agent: Mutt/1.5.20 (2009-06-14)
Subject: Re: [Caml-list] Signature monomorphism in functors

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