Re: [Caml-list] Type safe affectation ?

[Brian Hurt <brian.hurt@qlogic.com>]

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