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 NAA18932; Tue, 2 Jul 2002 13:42:30 +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 NAA18927 for ; Tue, 2 Jul 2002 13:42:29 +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 g62BgRP06544; Tue, 2 Jul 2002 13:42:27 +0200 (MET DST) Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA18815; Tue, 2 Jul 2002 13:42:26 +0200 (MET DST) Date: Tue, 2 Jul 2002 13:42:26 +0200 From: Xavier Leroy To: Michael Vanier Cc: pierre.weis@inria.fr, caml-list@inria.fr Subject: Re: [Caml-list] simple typing question Message-ID: <20020702134226.A18305@pauillac.inria.fr> References: <200207020914.LAA16152@pauillac.inria.fr> <200207020949.g629nQ606959@orchestra.cs.caltech.edu> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 1.0i In-Reply-To: <200207020949.g629nQ606959@orchestra.cs.caltech.edu>; from mvanier@cs.caltech.edu on Tue, Jul 02, 2002 at 02:49:26AM -0700 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > I *almost* understand. I understand the need for restrictions with > polymorphic references. The stated rule is that for > > let name = expr1 ... > > The type of expr1 is generalized when expr1 is a function, an identifier > or a constant. Otherwise the identifier name is not polymorphic (type > variables are not generalized). > > And later it's stated that when expr1 is "map (function x -> x)" it's an > application, so it isn't generalized. However, it's an application that > evaluates to a function, so it seems like it would meet the stated > criteria. No, it doesn't. There is a major difference between a literal function "fun x -> ..." and an expression that evaluates to a function. The latter can create and hide polymorphic references, as shown below. > Also, I'm not sure why such a restrictive rule is needed. If > expr1 doesn't manipulate references, why can't it be generalized? Because very similar expressions do manipulate references. In particular, consider that a (polymorphic) function can "hide" a (polymorphic) reference. For instance: # let make_toggle () = let r = ref [] in fun x -> let old = !r in r := x; old val make_toggle : unit -> 'a -> 'a list = The result of make_toggle() is a function with type _a list -> _a list that returns the argument that it received the last time it was called. # let f = make_toggle();; val f : '_a list -> '_a list = # f [1;2;3];; - : int list = [] # f [4;5;6];; - : int list = [1; 2; 3] Now, consider what happens if we were to generalize '_a in the type of f: # let f = make_toggle();; val f : 'a list -> 'a list = # f [1;2;3];; - : int list = [] # f ["hello"; "world"];; - : string list = [1; 2; 3] <--- crash! (wrong value for the type) The gist of this example is that "make_toggle()" looks a lot like "List.map (fun x -> x)" : both are function applications that return a function from '_a list to '_a list. Yet, one is safe to generalize and not the other. No reasonably simple type system can distinguish both examples. Many have been proposed -- this was a hot research topic in the 1980-1993 time frame, and I even did my PhD on this very topic -- but none was found to be really usable in practice. The value restriction on polymorphism (i.e. what Caml implements) is far from perfect, but is the "least bad" of the known solutions. - Xavier Leroy ------------------- 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