From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA29579; Thu, 2 May 2002 09:47:14 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA29575 for ; Thu, 2 May 2002 09:47:14 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id g427lDD07591 for ; Thu, 2 May 2002 09:47:13 +0200 (MET DST) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA29571 for caml-list@inria.fr; Thu, 2 May 2002 09:47:13 +0200 (MET DST) Date: Thu, 2 May 2002 09:47:13 +0200 From: Francois Pottier To: caml-list@inria.fr Subject: Re: [Caml-list] Re: Encoding "abstract" signatures Message-ID: <20020502094713.D27687@pauillac.inria.fr> Reply-To: Francois.Pottier@inria.fr References: <3CCD55BD.6DB352F5@ps.uni-sb.de> <20020429172853.A6314@pauillac.inria.fr> <3CCD794B.142F65D@ps.uni-sb.de> <20020430090732.A16788@pauillac.inria.fr> <000701c1f032$a69072c0$e8abfea9@melbourne> <20020430171846.A28745@pauillac.inria.fr> <000801c1f112$d4c266e0$e8abfea9@melbourne> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 1.0i In-Reply-To: <000801c1f112$d4c266e0$e8abfea9@melbourne>; from AndreasRossberg@web.de on Wed, May 01, 2002 at 03:19:29PM +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Wed, May 01, 2002 at 03:19:29PM +0200, Andreas Rossberg wrote: > > This is just one reason. More generally, it's the need for a coherent > encoding in the higher-order setting we face. If we say that type > > functor(X : sig type t val x : t end) -> ... > > maps to something like > > forall t. t -> ... > > then consequently > > functor(Y : sig module type T end) -> functor(X : Y.T) -> ... > > must map to some type that yields the above as the result of some sequence > of applications. Oh, I see what you mean. It's a good point. But still I think I can encode the second functor as forall T. () -> T -> ... (where (), the empty structure type, corresponds to Y and T corresponds to X) which, when applied to an empty structure, yields forall T. T -> ... as expected (provided the ``forall'' quantifier doesn't get in the way of application, i.e. polymorphic instantiation and abstraction are transparent, as in ML). > Well, besides the aforementioned problems, you don't represent type > abstraction at all (which, I would argue, is a central feature) - the > functor in question would not differ from > > functor F (X : sig module type T end) (Y : X.T) = Y Indeed it wouldn't. But I fail to see the point; if Y's type is X.T, there is no difference between Y and (Y : X.T), is there? The two functors in question have the same type in O'Caml. -- François Pottier Francois.Pottier@inria.fr http://pauillac.inria.fr/~fpottier/ ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners