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 UAA16457; Sun, 15 Jun 2003 20:53:24 +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 UAA16475 for ; Sun, 15 Jun 2003 20:53:22 +0200 (MET DST) Received: from mail.speakeasy.net (mail9.speakeasy.net [216.254.0.209]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id h5FIrLH14030 for ; Sun, 15 Jun 2003 20:53:21 +0200 (MET DST) Received: (qmail 13097 invoked from network); 15 Jun 2003 18:53:19 -0000 Received: from unknown (HELO grace.speakeasy.org) ([216.254.0.2]) (envelope-sender ) by mail9.speakeasy.net (qmail-ldap-1.03) with DES-CBC3-SHA encrypted SMTP for ; 15 Jun 2003 18:53:19 -0000 Date: Sun, 15 Jun 2003 11:53:19 -0700 (PDT) From: brogoff@speakeasy.net To: Xavier Leroy cc: Christophe Raffalli , "caml-list@inria.fr" Subject: Re: [Caml-list] Type safe affectation ? In-Reply-To: <20030614153523.A21942@pauillac.inria.fr> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Spam: no; 0.00; brogoff:01 caml-list:01 immutable:01 recursion:01 immutability:01 constants:01 extlib:01 pierre:01 weis:01 infer:01 inference:01 covariant:01 val:01 arrays:01 compiler:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Sat, 14 Jun 2003, Xavier Leroy wrote: > > Why not allow a typesafe way to mute immutable data (sum, products, > > immutable records and so on) ? > > Because that would make this data mutable :-) Agreed. However, as has been discussed on the list before, the specific example of list mutations where the mutation corresponds to filling "holes" or "one hole contexts" and allow more tail recursion optimizations is an important one that quite a few people would like to see addressed. > 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.) It's interesting that the theory for two (or n) hole contexts isn't worked out yet, or wasn't at the time Minamide wrote his paper. > 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. Is it the case that those functions which use it in a disciplined way, basically rewriting those functions transformable from "ML + Minamide style holes" to "ML + setcdr" are going to break something? I believe ExtLib is doing this, and probably a few others wrote such libaries after the previous round on this topic. It might make sense to provide immutable views of records which have privately mutable fields. This was discussed on the list too (by you and Pierre Weis I believe), so I guess the right people are thinking about it. > > 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. On a related note, I'd like a way to make an immutable representation of the built in array by not exporting the mutators, *and then* making the type parameter covariant, say a signature like the following module type FUNCTIONAL_ARRAY = sig type (+'a) t val init : int -> (int -> 'a) -> 'a t val get : 'a t -> int -> 'a val length : 'a t -> int val map : ('a -> 'b) -> 'a t -> 'b t end The only safe ways to do this using array are to hide array in a class definition or a function closure. It seems that I should be able to just write type 'a t = 'a array and have the type system figure out if it's OK. Arrays are efficient, and there are quite a few cases in my coding where they are not mutable. -- Brian ------------------- 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