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 PAA22776; Sat, 14 Jun 2003 15:35:25 +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 PAA22561 for ; Sat, 14 Jun 2003 15:35:24 +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 h5EDZNH28635; Sat, 14 Jun 2003 15:35:23 +0200 (MET DST) Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA22724; Sat, 14 Jun 2003 15:35:23 +0200 (MET DST) Date: Sat, 14 Jun 2003 15:35:23 +0200 From: Xavier Leroy To: Christophe Raffalli Cc: caml-list@inria.fr Subject: Re: [Caml-list] Type safe affectation ? Message-ID: <20030614153523.A21942@pauillac.inria.fr> References: <003601c33177$324ecc40$0201a8c0@dylan> <3EE98610.6090001@ozemail.com.au> <3EE9A15D.7080403@univ-savoie.fr> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 1.0i In-Reply-To: <3EE9A15D.7080403@univ-savoie.fr>; from Christophe.Raffalli@univ-savoie.fr on Fri, Jun 13, 2003 at 12:03:09PM +0200 X-Spam: no; 0.00; caml-list:01 funtion:01 type-safe:01 immutable:01 immutability:01 constants:01 infer:01 inference:01 compiler:01 ocaml:01 mutable:01 feasible:01 match:02 in-place:02 arbitrary:02 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > Using the Obj module you can do affectation of cons cell of a list (or > any onther data type), which is usefull for instance to write a tail > recursive Map funtion ... (see a previous thread) > But this is not typesafe ! Like all uses of module Obj, you can make this type-safe via proper type constraints: let set_cdr (l: 'a list) (x: 'a list) = match l with [] -> invalid_arg "set_cdr" | _::_ -> Obj.set_field (Obj.repr l) 1 (Obj.repr x) > Why not allow a typesafe way to mute immutable data (sum, products, > immutable records and so on) ? Because that would make this data mutable :-) Immutability isn't there just to annoy the programmer: it's a major improvement for software reliability and quality. Proving the correctness of functions that manipulate lists or trees is feasible if the data is immutable, but becomes essentially impossible if arbitrary in-place modifications are allowed anywhere in the program. Even if you're not interested in proofs of programs, I'm ready to bet that there aren't 1 programmer in 100 who can write *fully correct* code that manipulate mutable balanced trees, for instance. (I think I can't.) Also, keep in mind that the compiler can optimize based on immutability assumptions. For instance, the OCaml compiler performs propagation of structured constants and code motion for accesses inside data structures that are immutable. You might very well break something by using the set_cdr function above. > By the way, another step would be to infer for each function if it mutes > its arguments instead of annoting record with "mutable" indication. > > This is better because the same data may be considered as mutable by > some functions (for instance when you construct the data) but then be > used only by immutable functions and this way the type inference can > help you insure that you do not mute the data anymore. > > But this is research topic ? This sounds reminiscent of effect systems. - 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