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 VAA17252; Sun, 15 Jun 2003 21:30:37 +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 VAA17350 for ; Sun, 15 Jun 2003 21:30:35 +0200 (MET DST) Received: from epexch01.qlogic.org ([63.170.40.3]) by concorde.inria.fr (8.11.1/8.11.1) with ESMTP id h5FJUYH16970; Sun, 15 Jun 2003 21:30:34 +0200 (MET DST) Received: from epmailtmp.qlogic.org ([10.20.33.254]) by epexch01.qlogic.org with Microsoft SMTPSVC(5.0.2195.5329); Sun, 15 Jun 2003 14:31:29 -0500 Received: from [10.20.33.146] ([10.20.33.146]) by epmailtmp.qlogic.org with Microsoft SMTPSVC(5.0.2195.4905); Sun, 15 Jun 2003 14:31:29 -0500 Date: Sun, 15 Jun 2003 14:49:57 -0500 (CDT) From: Brian Hurt X-X-Sender: Reply-To: Brian Hurt To: cc: Xavier Leroy , Christophe Raffalli , "caml-list@inria.fr" Subject: Re: [Caml-list] Type safe affectation ? In-Reply-To: Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-OriginalArrivalTime: 15 Jun 2003 19:31:29.0379 (UTC) FILETIME=[B8101330:01C33374] X-Spam: no; 0.00; qlogic:01 caml-list:01 brogoff:01 immutable:01 recursion:01 overflowing:01 inlining:01 coroutines:01 immutability:01 constants:01 extlib:01 enum:01 covariant:01 val:01 type-:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Sun, 15 Jun 2003 brogoff@speakeasy.net wrote: > 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. I, personally, would perfer to see the optimizer do this. Any code that *correctly* uses holes is just as correct specified in a (non-tail-) recursive manner. List.append should be written like: let rec append a b = match a with [] -> b | h :: t -> h :: (append t b) Everything else is just optimization (and not overflowing the stack on large lists). Which, if it *can* (reasonably) be done by the compiler, *should* be done by the compilier. > > 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. Hmm. If the same result simply gets used in two or more places, then extending the optimization is obvious. If two different functions are called to fill the two different holes, I don't see how you can run both functions "at once", without either rampant inlining or coroutines. > > > 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. If there is one thing I'm regretting with ExtLib, is that we've seemed to make using Obj.magic "cool", or at least "common and usefull". Were holes added to the standard Ocaml compiler, I'd be re-rewritting ExtList to take those optimizations *out*. There's other stuff in ExtLib which is usefull even without the new List code- Enum, for example. So the project will survive regardless. Or maybe I'm overstating ExtLib's effect- and there has always been a lot of Obj.magic going around. > 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. All you have to do in this code is just not allow a mutation to occur in your code. As I understand things, to everyone outside of the module 'a t is an abstract type- the only way to mutate it is to pass it to a function in the module that mutates it. The only other problem is that you currently have to give up a.(i) addressing style. I wish operator defining would be extended to allow array references. 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