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 LAA31987; Thu, 2 May 2002 11:30:53 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id LAA31982 for ; Thu, 2 May 2002 11:30:51 +0200 (MET DST) Received: from indyio.rz.uni-sb.de (indyio.rz.uni-sb.de [134.96.7.3]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g429UoX01287; Thu, 2 May 2002 11:30:50 +0200 (MET DST) Received: from mars.rz.uni-sb.de (IDENT:FRMJmyrbo3te79kLtLFVElzYs1I46L1k@mars.rz.uni-sb.de [134.96.7.4]) by indyio.rz.uni-sb.de (8.9.3/8.9.3) with ESMTP id LAA3578916; Thu, 2 May 2002 11:30:50 +0200 (CEST) Received: from uni-sb.de (uni-sb.de [134.96.7.230]) by mars.rz.uni-sb.de (8.8.8/8.8.4/8.8.2) with ESMTP id LAA104134126; Thu, 2 May 2002 11:30:50 +0200 (CEST) Received: from cs.uni-sb.de (cs.uni-sb.de [134.96.252.31]) by uni-sb.de (8.12.2/2002030600) with ESMTP id g429Und28015; Thu, 2 May 2002 11:30:49 +0200 (CEST) Received: from mail.cs.uni-sb.de (IDENT:IB+3fkEjfYE9GICg2ClSUvp6FefVEv8q@mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.12.1/2002030600) with ESMTP id g429UmW04481; Thu, 2 May 2002 11:30:49 +0200 (CEST) Received: from ps.uni-sb.de (grizzly.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.12.3/2002040900) with ESMTP id g429Ul605058; Thu, 2 May 2002 11:30:47 +0200 (CEST) X-Authentication-Warning: email: Host grizzly.ps.uni-sb.de [134.96.186.68] claimed to be ps.uni-sb.de Received: from ps.uni-sb.de (zoidberg.ps.uni-sb.de [134.96.186.121]) by ps.uni-sb.de (8.11.6/8.11.0) with ESMTP id g429Umh22595; Thu, 2 May 2002 11:30:48 +0200 Message-ID: <3CD107B5.E300E47E@ps.uni-sb.de> Date: Thu, 02 May 2002 11:32:37 +0200 From: Andreas Rossberg Organization: =?iso-8859-1?Q?Universit=E4t?= des Saarlandes X-Mailer: Mozilla 4.78 [en] (X11; U; Linux 2.4.9-21 i686) X-Accept-Language: de, en MIME-Version: 1.0 To: Francois.Pottier@inria.fr CC: caml-list@inria.fr Subject: Re: [Caml-list] Re: Encoding "abstract" signatures 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> <20020502094713.D27687@pauillac.inria.fr> Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk Hi François, Francois Pottier 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). OK, consider applying module type T = sig type t type u val x : t * u end Then, in the encoding, application should yield the result type forall t,u. t * u -> ... So you cannot simply `reuse' T's quantifier. Also note that in general the quantifier(s) in question might be buried deep inside the RHS of the arrow, even in contravariant position. (Moreover, it is not obvious to me whether we could use implicit type application, because polymorphism is first-class (a field or argument of functor type would be polymorphic)). > > 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. Ah, yes, you are right, I forgot about that. Actually, I see that as an unfortunate limitation of OCaml's module typing: it has to forget some sharing because it lacks proper singleton types (and thus loses principality). Ideally, the type of the above variant of F should be functor(X : sig module type T end) -> functor(Y : X.T) -> that Y where I write "that Y" for the singleton type inhabited by Y only (a subtype of X.T). That functor is essentially the polymorphic identity functor, while the other variation was a polymorphic eta-expansion of the abstraction operator. But in fact, what that means is that in OCaml both functors must be represented by a type with an existential quantifier. Otherwise you would not witness any difference between module expressions M and F (struct module type T = ABSTRACT_SIG_OF_M end) (M) -- Andreas Rossberg, rossberg@ps.uni-sb.de "Computer games don't affect kids; I mean if Pac Man affected us as kids, we would all be running around in darkened rooms, munching magic pills, and listening to repetitive electronic music." - Kristian Wilson, Nintendo Inc. ------------------- 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