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 RAA29097; Tue, 30 Apr 2002 17:18:48 +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 RAA29093 for ; Tue, 30 Apr 2002 17:18:47 +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 g3UFIk515278 for ; Tue, 30 Apr 2002 17:18:46 +0200 (MET DST) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA29089 for caml-list@inria.fr; Tue, 30 Apr 2002 17:18:46 +0200 (MET DST) Date: Tue, 30 Apr 2002 17:18:46 +0200 From: Francois Pottier To: caml-list@inria.fr Subject: [Caml-list] Re: Encoding "abstract" signatures Message-ID: <20020430171846.A28745@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> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 1.0i In-Reply-To: <000701c1f032$a69072c0$e8abfea9@melbourne>; from AndreasRossberg@web.de on Tue, Apr 30, 2002 at 12:34:26PM +0200 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Andreas, On Tue, Apr 30, 2002 at 12:34:26PM +0200, Andreas Rossberg wrote: > > How do you express > > functor F (X : sig module type T end) (Y : X.T) = (Y : X.T) > > without parameterizing over the set of existentially quantified variables > somehow? I had in mind something like (again assuming non-applicative > functors, because they are much simpler): > > LAMBDA k. Lambda S:(k->*). Lambda ts:k. lambda Y:S(ts). > pack Y as exists ts:k.S(ts) You make the functor F polymorphic in the number of type components defined by the signature S. As far as I understand, this is made necessary by the desire to hide these types in the functor's result (i.e. the pack operation). It seems to me that it is simpler to suppress the pack operation, i.e. to return Y instead of (pack Y as ...). Then, instead of quantifying separately over S and ts, you only need to quantify over S(ts), that is, T, as follows: val F : forall T. T -> T I must say I don't know exactly what is lost with this simplification; is there a loss of abstraction? The answer isn't obvious to me. But it seems to offer a simple understanding of the above O'Caml specification. -- 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