[Caml-list] Dynamic types, casts, and rights amplification

[Caml-list] Dynamic types, casts, and rights amplification

[Mark Seaborn]

Here's a nice use of OCaml's casts to provide what can be viewed as an
open dynamic type (except that variant tags -- called brands here --
are created at run time).

  (* 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 `=='.
  *)
  (* I was going to have:
     make_brand : 'a -> 'a brand
     where the argument is an example value which is ignored.
     But this isn't really necessary, and it could be awkward. *)
  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

  module Dyn : 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

using this module:

  module type Stamp = sig
    type t
    val make : unit -> t
    val eq : t -> t -> bool
  end
  
  module Stamp : Stamp = struct
    type t = unit ref
    let make() = ref()
    let eq s1 s2 = s1 == s2
  end

and here's a utility built with the Dyn module:

  (* Should obey these axioms:
       unpack (pack x) = x
       unpack (pack2 b s x) = x
       amplify b (pack x) = None
       amplify b (pack2 b s x) = Some s
       amplify b1 (pack2 b2 s x) = None    provided b1 != b2
     Note that
       pack x = pack2 b s x
     where b is closely-held, ie. not available to anyone.
     The last axiom is simply the generativity of make_brand:
       make_brand() != make_brand()
     NB. The equality used here is behavioural equality (which
     is undecidable) rather than OCaml's `=' or `=='.
  *)
  module type RightsAmp = sig
    type 'a t
    type 'a brand
    val make_brand : unit -> 'a brand
    val pack2 : 'b brand -> 'b -> 'a -> 'a t
    val pack : 'a -> 'a t
    val unpack : 'a t -> 'a
    val amplify : 'b brand -> 'a t -> 'b option
  end
  
  module RightsAmp : RightsAmp = struct
    type 'a brand = 'a Dyn.brand
    type 'a t = 'a * Dyn.t
    let make_brand = Dyn.make_brand
    let pack2 brand secret value = (value, Dyn.pack brand secret)
    let pack value = (value, Dyn.null)
    let unpack (value, _) = value
    let amplify brand (_, x) = Dyn.unpack brand x
  end


I believe it's type sound, because it's not possible to create
polymorphic brands by the same restriction that prevents reference
values from being used polymorphically (the fact that this worked was
rather neat, I thought).  However, if OCaml changed its tagged data
representation, casting could probably no longer be used this way (is
that likely to happen?).  I think it should be possible to
alternatively implement this with brands as weak hash tables, and
Dyn.t as a unique stamp acting as a hash table key (though OCaml
doesn't provide weak hash tables, I think).

I found this particularly useful for getting around OCaml's
restrictions on circular dependencies between modules (in particular,
not being able to use a module parametrically in a cycle of
mutually-recursive types).

I used it to wrap up closures and allow the creator of closures to
recognise those closures it created and unpack hidden data from them
(or fall back to the default case for closures created by others) --
this is where the RightsAmp module comes in.  It would have been
convenient if this layer of wrapping was not needed and closures could
be branded directly -- I imagine that the representation of closures
is fairly flexible, and this could be a more lightweight solution.
Brands would act a little like classes, except that the identity of a
class would act like a capability and need not be revealed.

I wonder, has anyone done this before?  And if so, what phrases did
they use?  (I have seen `brand' associated with rights amplification,
so I used that term.)

What is the chance of this going into the OCaml distribution?
ie. Would you want to commit yourself to providing this interface in
OCaml in the future?

-- 
         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] Dynamic types, casts, and rights amplification

[Francois Pottier]

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


Mark,

> Here's a nice use of OCaml's casts to provide what can be viewed as an
> open dynamic type (except that variant tags -- called brands here --
> are created at run time).

There are ways of implementing such a dynamic type without using unsafe
type casts (i.e. Obj.magic). I have attached a file containing two sample
implementations.

The first one generates exceptions dynamically and uses them as tags. The
fact that they are exceptions is irrelevant; what matters is the ability to
generate new tags at runtime. Unfortunately, this piece of code isn't accepted
by O'Caml, because it doesn't recognize the type variable 'a in the exception
declaration as bound by the preceding type annotation.

The second one uses references as temporary buffers for data exchange. The
idea was posted a while ago on this mailing list, but I couldn't find the
exact reference. Instead of being tagged, a value is encoded within a function
whose effect is to write the value into a reference.

The second implementation is interesting, because it makes it easy to see why
one shouldn't create polymorphic brands: brands *are* references in this
approach.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/

[-- Attachment #2: dyn.ml --]
[-- Type: text/plain, Size: 796 bytes --]

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

module Dyn : Dyn = struct
  type 'a brand = ('a -> exn) * (exn -> 'a option)
  type t = exn
  let make_brand : unit -> 'a brand = function () ->
    let module X = struct
      exception E of 'a
      let pack x = E x
      let unpack = function
	| E x -> Some x
	| _ -> None
    end in
    X.pack, X.unpack
  let pack = fst
  let unpack = snd
  exception Null
  let null = Null
end

module Dyn : Dyn = struct
  type 'a brand = ('a option) ref
  type t = unit -> unit
  let make_brand () =
    ref None
  let pack b x () =
    b := Some x
  let unpack b f =
    b := None;
    f();
    !b
  let null () =
    ()
end

Re: [Caml-list] Dynamic types, casts, and rights amplification

[Markus Mottl]

On Wed, 11 Jul 2001, Francois Pottier wrote:
> The first one generates exceptions dynamically and uses them as
> tags. The fact that they are exceptions is irrelevant; what matters
> is the ability to generate new tags at runtime. Unfortunately, this
> piece of code isn't accepted by O'Caml, because it doesn't recognize
> the type variable 'a in the exception declaration as bound by the
> preceding type annotation.

I also mentioned this limitation only a few days ago ("polymorphic"
exceptions - they are not really polymorphic, of course, but make use
of type variables bound elsewhere).  Unfortunately, I didn't get any
response so far whether there are inherent difficulties in implementing
an extension. It wouldn't require any syntax change at all, won't break
old code, but clearly gives more expressiveness to the developer. Any
comments?

Regards,
Markus Mottl

-- 
Markus Mottl                                             markus@oefai.at
Austrian Research Institute
for Artificial Intelligence                  http://www.oefai.at/~markus
-------------------
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