[Caml-list] mutability analysis too strict?

[Caml-list] mutability analysis too strict?

[Ohad Rodeh]

List,
   I have a problem with hashtable mutability analysis. For example:

      let h = Hashtbl.create 10;;
      h : ('_a, '_b) Hashtbl.t

The objects and keys in the table are infered to be mutable. However,
in my case, they are immutable and I have to coerce them using Obj.magic
from
'_b to 'b.

Can this be fixed? why is the analysis so restrictive?

     Ohad.


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] mutability analysis too strict?

[Francois Pottier]

On Sun, Dec 09, 2001 at 05:43:41PM +0200, Ohad Rodeh wrote:
> 
>       let h = Hashtbl.create 10;;
>       h : ('_a, '_b) Hashtbl.t
> 
> The objects and keys in the table are infered to be mutable. However,
> in my case, they are immutable and I have to coerce them using Obj.magic
> from '_b to 'b.

You are slightly wrong here: the analysis infers the table itself (not the
keys or objects in it) to be mutable, which it indeed is. If the table was
given a polymorphic type, you would be able to store objects of a certain
type and to retrieve them at another type (by taking different instances of
'b), which would be unsound.

Furthermore, I'm surprised to hear that using Obj.magic helps; indeed, any
application of Obj.magic is itself deemed `dangerous' by O'Caml, leading
to the following behavior:

  # let h = Hashtbl.create 10;;  
  val h : ('_a, '_b) Hashtbl.t = <abstr>
  # let h = (Obj.magic h : ('a, 'b) Hashtbl.t);;
  val h : ('_a, '_b) Hashtbl.t = <abstr>

That is, Obj.magic doesn't help at all in this case.

Perhaps you could tell us what you are trying to achieve? Any polymorphic,
mutable structure is unsound and rightly rejected. A monomorphic, mutable
structure that contains polymorphic data is sound, but cannot be expressed
in ML's type system where universal quantification must be prenex.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] mutability analysis too strict?

[Mark Seaborn]

"Ohad Rodeh" <ORODEH@il.ibm.com> writes:

> Well, that's a strong argument ...
> 
> How do you propose building a repository of polymorphic values then?
> 
>      Ohad.

I assume you don't want to store polymorphic values (eg. polymorphic
functions) but want to store values of different (but monomorphic)
types.  One way is to wrap your values up in a variant type.  However,
that limits you to a fixed, finite number of types which must be
declared in the same place.  Here's some code which effectively lets
you create an open (extensible) variant type:


module type Stamp = sig
  type t
  val make : unit -> t
  val eq : t -> t -> bool
end

(* This is vulnerable to overflow, and will not garbage collect
   unused stamps.  However, the one advantage of this is that new
   stamps require no heap allocation. *)
module Stamp_Int : Stamp = struct
  type t = int
  let c = ref 0
  let make() = let v = !c in c := v+1; v
  let eq s1 s2 = s1 = s2
end

module Stamp_Cell : Stamp = struct
  type t = unit ref
  let make() = ref()
  let eq s1 s2 = s1 == s2
  (* An interesting difference between SML and OCaml is that
     in OCaml, `=' will recursive into references, whereas in
     SML, `=' stops at references and compares their locations. *)
end

module Stamp = Stamp_Cell


(* Should obey these axioms:
     unpack b (pack b x) = Some x
     unpack b1 (pack b2 x) = None    provided b1 != b2
     unpack b null = None
   (ie. for the last one, the brand for null is closely-held)
   and lastly:
     make_brand() != make_brand()
   NB. The equality used here is behavioural equality (which
   is undecidable) rather than OCaml's `=' or `=='.
*)
module type Dyn = sig
  type 'a brand
  type t
  val make_brand : unit -> 'a brand
  val pack : 'a brand -> 'a -> t
  val unpack : 'a brand -> t -> 'a option
  val null : t
end

(* The aim is that this should be type sound.  The reason this should be
   sound is that it is not possible to create polymorphic brands,
   since the same restriction that applies to polymorphic references
   applies here, and brands, like references, are generative, so that
   eta-converting will change the semantics and not break
   soundness. *)
(* GC properties:
   If you discard a dyn value, its hidden value will be GC'd.
   But if you discard a brand, the hidden values in the dyn types won't. *)
module Dyn_Cast : Dyn = struct
  (* Don't care about this type; it is cast to and from,
     the equivalent of C's void*. *)
  type any = int
  type 'a brand = Stamp.t
  type t = Stamp.t * any
  let make_brand() = Stamp.make()
  let pack brand value = (brand, Obj.magic value)
  let unpack brand1 (brand2, value) =
    if Stamp.eq brand1 brand2 then Some (Obj.magic value) else None
  let null = pack (make_brand()) ()
end

(* Implementation using `energetic secrets'.  Does not require unsafe
   constructs like Obj.magic, but will not work as expected if
   temporal encapsulation is violated, eg. by concurrency.  OCaml
   doesn't have re-enterable continuations to violate this with,
   though if it did I'm not sure if you'd be able to capture a
   continuation inside the unpacking operation. *)
module Dyn_ES : Dyn = struct
  type 'a brand = 'a option ref
  (* Passing an action saves having to create two closures *)
  type action = Fill | Clear
  type t = action -> unit
  let make_brand() = ref None
  let pack brand value = function
    | Fill -> brand := Some value
    | Clear -> brand := None
  (* Invariant applies before these are called:  all brands are empty. *)
  let unpack brand f =
    f Fill;
    let r = !brand in
      f Clear; r
  (* This packed value modifies no brand when invoked *)
  let null _ = ()
end

module Dyn = Dyn_Cast

-- 
         Mark Seaborn
   - mseaborn@bigfoot.com - http://www.srcf.ucam.org/~mrs35/ -

        ``Cambridge?  Didn't that used to be a polytechnic?''
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] mutability analysis too strict?

[Francois Pottier]

On Mon, Dec 10, 2001 at 12:13:19PM +0200, Ohad Rodeh wrote:
> 
> How do you propose building a repository of polymorphic values then?

Unless I'm mistaken, the short answer is, you can't. As pointed out by
Rémi, your proposed interface:

  module type Repos = sig
    val put : 'a -> 'b -> unit
    val get : 'a -> 'b
  end

is inherently unsafe. One solution is to use several repositories
(i.e. several hash tables). You can wrap them up into a single module if you
wish, but the client will then need to tell which repository (i.e. which hash
table) he wishes to access:

  module type Repositories = sig
    type ('a, 'b) repository
    val put : ('a, 'b) repository -> 'a -> 'b -> unit
    val get : ('a, 'b) repository -> 'a -> 'b
  end

Not very useful, though, since this merely paraphrases the interface for hash
tables.

Another solution is to create a single repository where keys and/or objects
belong to a suitably defined `universal' (also known as `dynamic') type. That
is, the repository would be a hash table of type [(univ, univ) Hashtbl.t],
where the abstract type [univ] supports the following operations:

  type univ
  type 'a tag

  val new_tag: unit -> 'a tag
  val in: 'a tag -> 'a -> univ
  val out: 'a tag -> univ -> 'a

A value of arbitrary type can be turned into a [univ] value by attaching it
with an explicit tag, using [in]. It can later be retrieved by matching it
against the same tag, using [out]. ([out] may fail dynamically if the tags do
not match.) [out] is type-safe because it requires a tag; it would be unsound
for [out] to have type unit -> 'a (same problem as for [get] above).

One possible implementation for [univ], where a tag is implemented as a
reference cell, was posted to the list a while ago, but I can't find it at the
moment. Another possible implementation implements tags using exception names.
(In this variant, the type [tag] disappears, and [new_tag] is a functor which
produces specialized versions of [in] and [out].) These solutions are rather
tricky to implement; furthermore, they are inefficient and unsafe, because
[out] involves a run-time check. You are probably better off using several
hash tables.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] mutability analysis too strict?

[Basile STARYNKEVITCH]

>>>>> "Ohad" == Ohad Rodeh <ORODEH@il.ibm.com> writes:

[...]

    Ohad> How do you propose building a repository of polymorphic
    Ohad> values then?

Either use the Hashtbl.Make functor or else make your own polymorphic
hash tables.

See also the thread I started with
http://caml.inria.fr/archives/199704/msg00014.html on the mailing
list.

-- 

Basile STARYNKEVITCH         http://starynkevitch.net/Basile/ 
email: basile<at>starynkevitch<dot>net 
alias: basile<at>tunes<dot>org 
8, rue de la Faïencerie, 92340 Bourg La Reine, France
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] mutability analysis too strict?

[Ohad Rodeh]

> Sent by:     owner-caml-list@pauillac.inria.fr

> To: caml-list@inria.fr
> cc:
> Subject:     Re: [Caml-list] mutability analysis too strict?



> "Ohad Rodeh" <ORODEH@il.ibm.com> writes:

> > First of all, sorry my mail was sent twice, this was due to mail
delivery
> > problems
> > from my site.
> >
> > Perhaps I was not specific enough about what I wanted to acheive. What
I
> > need
> > is a repository that has the following interface:
> >
> > module type Repos = sig
> >   val put : 'a -> 'b -> unit
> >   val get : 'a -> 'b
> > end
> >
> > An  implementation that looks like this:
> >
> > module S : Repos = struct
> >    let h = Hashtbl.create 10
> >    let put key data = Hashtbl.add h key data
> >    let get key = Hashtbl.find h key
> > end
> >
> > Does not work. Compilation error:
> >
> > Signature mismatch:
> > Modules do not match:
> >   sig
> >     val h : ('_a, '_b) Hashtbl.t
> >     val put : '_a -> '_b -> unit
> >     val get : '_a -> '_b
> >   end
> > is not included in
> >   Repos
> > Values do not match:
> >   val put : '_a -> '_b -> unit
> > is not included in
> >   val put : 'a -> 'b -> unit
> >
> > I tried also using the Map and Set modules, but they don't really allow
> > building
> > a repository of immutable values either. Is there any deep reason for
this
> > behavior? Could you expound on this line:
> >
> > > A monomorphic, mutable
> > > structure that contains polymorphic data is sound, but cannot be
> > expressed
> > > in ML's type system where universal quantification must be prenex.
> >
> > Ohad.



Remi VANICAT <vanicat@labri.u-bordeaux.fr>@pauillac.inria.fr on 10/12/2001
11:28:42

> it's dangerous. Imagine you can do :
>
> put 2 "xd"
>
> what will be the type of :
>
> get 2
>
> how the type inference algorithm can know that it is a string ? it
> can't because you can do something like :
>
> if x < y then put 2 "xd"
> else put 2 5
>
> and then, the type of get 2 wil be string or int depending on the fact
> that x was less than y or not.



Well, that's a strong argument ...

How do you propose building a repository of polymorphic values then?

     Ohad.


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] mutability analysis too strict?

[Remi VANICAT]

"Ohad Rodeh" <ORODEH@il.ibm.com> writes:

> First of all, sorry my mail was sent twice, this was due to mail delivery
> problems
> from my site.
> 
> Perhaps I was not specific enough about what I wanted to acheive. What I
> need
> is a repository that has the following interface:
> 
> module type Repos = sig
>   val put : 'a -> 'b -> unit
>   val get : 'a -> 'b
> end
> 
> An  implementation that looks like this:
> 
> module S : Repos = struct
>    let h = Hashtbl.create 10
>    let put key data = Hashtbl.add h key data
>    let get key = Hashtbl.find h key
> end
> 
> Does not work. Compilation error:
> 
> Signature mismatch:
> Modules do not match:
>   sig
>     val h : ('_a, '_b) Hashtbl.t
>     val put : '_a -> '_b -> unit
>     val get : '_a -> '_b
>   end
> is not included in
>   Repos
> Values do not match:
>   val put : '_a -> '_b -> unit
> is not included in
>   val put : 'a -> 'b -> unit
> 
> I tried also using the Map and Set modules, but they don't really allow
> building
> a repository of immutable values either. Is there any deep reason for this
> behavior? Could you expound on this line:
> 
> > A monomorphic, mutable
> > structure that contains polymorphic data is sound, but cannot be
> expressed
> > in ML's type system where universal quantification must be prenex.
> 
> Ohad.

it's dangerous. Imagine you can do :

put 2 "xd"

what will be the type of :

get 2

how the type inference algorithm can know that it is a string ? it
can't because you can do something like :

if x < y then put 2 "xd"
else put 2 5

and then, the type of get 2 wil be string or int depending on the fact
that x was less than y or not.


-- 
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

Re: [Caml-list] mutability analysis too strict?

[Ohad Rodeh]

First of all, sorry my mail was sent twice, this was due to mail delivery
problems
from my site.

Perhaps I was not specific enough about what I wanted to acheive. What I
need
is a repository that has the following interface:

module type Repos = sig
  val put : 'a -> 'b -> unit
  val get : 'a -> 'b
end

An  implementation that looks like this:

module S : Repos = struct
   let h = Hashtbl.create 10
   let put key data = Hashtbl.add h key data
   let get key = Hashtbl.find h key
end

Does not work. Compilation error:

Signature mismatch:
Modules do not match:
  sig
    val h : ('_a, '_b) Hashtbl.t
    val put : '_a -> '_b -> unit
    val get : '_a -> '_b
  end
is not included in
  Repos
Values do not match:
  val put : '_a -> '_b -> unit
is not included in
  val put : 'a -> 'b -> unit

I tried also using the Map and Set modules, but they don't really allow
building
a repository of immutable values either. Is there any deep reason for this
behavior? Could you expound on this line:

> A monomorphic, mutable
> structure that contains polymorphic data is sound, but cannot be
expressed
> in ML's type system where universal quantification must be prenex.

Ohad.



Francois Pottier <francois.pottier@inria.fr>@pauillac.inria.fr on
10/12/2001 10:13:31

Please respond to Francois.Pottier@inria.fr

Sent by:  owner-caml-list@pauillac.inria.fr


To:   Ohad Rodeh/Haifa/IBM@IBMIL
cc:   caml-list@inria.fr
Subject:  Re: [Caml-list] mutability analysis too strict?




On Sun, Dec 09, 2001 at 05:43:41PM +0200, Ohad Rodeh wrote:
>
>       let h = Hashtbl.create 10;;
>       h : ('_a, '_b) Hashtbl.t
>
> The objects and keys in the table are infered to be mutable. However,
> in my case, they are immutable and I have to coerce them using Obj.magic
> from '_b to 'b.

You are slightly wrong here: the analysis infers the table itself (not the
keys or objects in it) to be mutable, which it indeed is. If the table was
given a polymorphic type, you would be able to store objects of a certain
type and to retrieve them at another type (by taking different instances of
'b), which would be unsound.

Furthermore, I'm surprised to hear that using Obj.magic helps; indeed, any
application of Obj.magic is itself deemed `dangerous' by O'Caml, leading
to the following behavior:

  # let h = Hashtbl.create 10;;
  val h : ('_a, '_b) Hashtbl.t = <abstr>
  # let h = (Obj.magic h : ('a, 'b) Hashtbl.t);;
  val h : ('_a, '_b) Hashtbl.t = <abstr>

That is, Obj.magic doesn't help at all in this case.

Perhaps you could tell us what you are trying to achieve? Any polymorphic,
mutable structure is unsound and rightly rejected. A monomorphic, mutable
structure that contains polymorphic data is sound, but cannot be expressed
in ML's type system where universal quantification must be prenex.

--
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/
-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ:
http://caml.inria.fr/FAQ/
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/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

[Caml-list] Mutability analysis too strict?

[Ohad Rodeh]

List,
   I have a problem with the mutability analysis for hash-tables.
For example:
     let h = Hashtbl.create 10 ;;
creates:
     h : ('_a, '_b) Hashtbl.t
instead of:
     h ('a, 'b) Hashtbl.t

My specific hashtable contains immutable objects that can be added
and removed to the table.  The default analysis is too strict, forcing me
to use Obj.magic for coercion ('_b -> 'b). This is safe in this case,
because I know
the objects are immutable. However, in the general case, I don't see
why it is neccessary.

 Anyone cares to explain?

     Ohad.


-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr