Re: [Caml-list] Type safe affectation ?

[brogoff@speakeasy.net]

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