RE: [Caml-list] Type safe affectation ?

RE: [Caml-list] Type safe affectation ?

[Gregory Morrisett]

>The problem is that holes at the type level are a difficult feature to
>offer: they require linear types in the compiler. As an 
>optimization, it is a rather high-level one, and maybe not so 
>easy to know when it will apply.

Perhaps, but it's easy for a compiler to offer support
for "tail-allocation" (i.e., a tail-call except for a
constructor application) which is what you need for
a tail-recursive append or map.  Perry Cheng implemented it in
the TIL compiler in about a week if memory serves and
it was a tremendous improvement in performance without
any magic.  

Yasuhiko Minamide wrote a paper on how to model this
well (I think it appeared in ICFP).  The approach used
in our Typed Assembly Language paper is yet another
approach based on a simple subtyping trick with initialization
flags.  It didn't require linear types at all and 
instead of implicit subtyping, you could accomplish
the same thing with an explicit (type-safe) up-cast.

So, all in all, it's quite possible to have the compiler
implement this optimization for the common case of
tail-allocation, and if you think it's more generally
applicable, then you could move to something like TAL's
initialization flags (though I would prefer the former
option.)  

-Greg

-------------------
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

Re: [Caml-list] Type safe affectation ?

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 2637 bytes --]

Gregory Morrisett wrote:
>>The problem is that holes at the type level are a difficult feature to
>>offer: they require linear types in the compiler. As an 
>>optimization, it is a rather high-level one, and maybe not so 
>>easy to know when it will apply.
> 
> 
> Perhaps, but it's easy for a compiler to offer support
> for "tail-allocation" (i.e., a tail-call except for a
> constructor application) which is what you need for
> a tail-recursive append or map.  Perry Cheng implemented it in
> the TIL compiler in about a week if memory serves and
> it was a tremendous improvement in performance without
> any magic.  
> 
> Yasuhiko Minamide wrote a paper on how to model this
> well (I think it appeared in ICFP).  The approach used
> in our Typed Assembly Language paper is yet another
> approach based on a simple subtyping trick with initialization
> flags.  It didn't require linear types at all and 
> instead of implicit subtyping, you could accomplish
> the same thing with an explicit (type-safe) up-cast.
> 
> So, all in all, it's quite possible to have the compiler
> implement this optimization for the common case of
> tail-allocation, and if you think it's more generally
> applicable, then you could move to something like TAL's
> initialization flags (though I would prefer the former
> option.)  

Does this also solve the construction of structure with loop ? (the 
other case were affectation is needed ? I say that because it is a 
similar problem and can be seen as a failuer of the compiler to type 
some expressions like this (the compiler says :

This kind of expression is not allowed as right-hand side of `let rec'
for add_Greater and add_Less

module Var = struct
   type t = var
   let compare = (-)
end

module MapVar = Map.Make(Var)

type env = value MapVar.t

and value =
   | Def of closure
   | Less of closure
   | Greater of closure

and closure = typ * env

let add_Greater v t e =
   let rec va = Greater(t, e')
   and e' = MapVar.add v va e in
   e'

let add_Less v t e =
   let rec va = Greater(t, e')
   and e' = MapVar.add v va e in
   e'

The same fonction is easy to write with affectation ... so it should be 
possible to compile it ?


-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------

[-- Attachment #2: Type: application/pgp-signature, Size: 252 bytes --]

RE: [Caml-list] Type safe affectation ?

[Gregory Morrisett]

> > Perhaps, but it's easy for a compiler to offer support
> > for "tail-allocation"  

> Does this also solve the construction of structure with loop ? (the 
> other case were affectation is needed ? 

No, not really.  The TAL approach would handle this.  
But then so would using an option ref.  I'd hate to
see the external language changed with that kind of
ugliness.

-Greg

-------------------
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

Re: [Caml-list] Type safe affectation ?

[Jacques Garrigue]

From: Brian Hurt <brian.hurt@qlogic.com>
> On Sun, 15 Jun 2003 brogoff@speakeasy.net wrote:
> > On Sat, 14 Jun 2003, Xavier Leroy wrote:
> > > 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.

There are safe ways to do that: when you build such a structure with a
hole, first define a mutable type sharing the same representation with
your intended immutable type, and cast to it after you're fisnished.
Since ocaml doesn't do any fancy representation optimizations, this
will work, and if it changes all C libraries are broken anyway.

For instance, you can write for a list:

type 'a mut_list = {hd: 'a; mutable tl: 'a list}
external inj : 'a mut_list -> 'a list = "%identity"

Limitation: for sum types, this only works for the first parameterized
constructor (the tag has to be 0). For records there is no problem.

Also, you must be very careful about not letting a mut_list value leak
out (respect the linearity), otherwise inferred information such as
variance will be incorrect, and you can break the type system.

By the way, the above limitation is yet one more reason I think it
would be really cool to allow records inside sum-type definitions.

> 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.

The problem is that holes at the type level are a difficult feature to
offer: they require linear types in the compiler. As an optimization,
it is a rather high-level one, and maybe not so easy to know when it
will apply.
 
> Or maybe I'm overstating ExtLib's effect- and there has always been a lot 
> of Obj.magic going around.

I certainly hope this is not the case. Obj.magic is EVIL.
It is only acceptable in this case because we want to optimize some
well-known structure, and we can check the correctness for sure.
At the user level, it is certainly preferable to use a mutable
structure to start with.

> > 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.

This one is just a typing problem. Nothing magic here, and it should
actually be possible to infer correctly the variance of an abstract
type, independently of its representation. But this is high-level and
potentially dangerous stuff, so don't hold your breath for this.

> 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.

Here the problem is variance. Currently ocaml does not allow the
above, because 'a array is not covariant.

Cheers,

        Jacques

-------------------
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

Re: [Caml-list] Type safe affectation ?

[Brian Hurt]

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

Re: [Caml-list] Type safe affectation ?

[brogoff]

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

Re: [Caml-list] Type safe affectation ?

[Xavier Leroy]

> 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

[Caml-list] Type safe affectation ?

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1220 bytes --]


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 !

Why not allow a typesafe way to mute immutable data (sum, products, 
immutable records and so on) ?

---

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 ?


-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------

[-- Attachment #2: Type: application/pgp-signature, Size: 252 bytes --]