This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Re: [Caml-list] mutability analysis too strict?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2001-12-10 (11:19) From: Mark Seaborn Subject: Re: [Caml-list] mutability analysis too strict?

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

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