Keeping local types local?

[David Rajchenbach-Teller <David.Teller@ens-lyon.org>]

        Hi everyone,

 Recently, I've been thinking about a small technique which I would like
to use to design some libraries. Essentially, I'd like to define values
which can't escape a given scope. One way of doing so would be to use
monads but my idea is to use local modules and local types and take
advantage of the fact that values of that type cannot escape the scope
of the local module. Unfortunately, as it turns out, sometimes, values
with a local type can escape their scope -- and I'm looking for an idea
on how to plug the leak.

Let's try and make this clear with an example. In the following code, we
have two operations [set] and [get], which should only be called between
initialization and clean-up. To enforce this guarantee, we use a local
module (added by Camlp4), with a local type ['a t] and we make sure that
our two operations have a return type ['a t]. We also have some client
code (actually written by the user), which may use [get], [set] and
[return] (note: 

let f () =
  let result = 
    let module A =
	struct
	  type 'a t = Guard of 'a (*Used only to prevent scope escape.*)

                  (** Local primitives, usage guarded by [Guard] *)

	  let set v =
	    (*perform some side-effect*)
	    Guard ()

                  let get () =
                    (*perform some side-effect*)
                    Guard 42(*or some other value*)

                  let return x =
                    Guard x

                  (** Infrastructure *)

	  let result =
                    (*initialize some stuff*)
                     match
                      (*start of client code*)
                            (*client code doesn't know about [Guard]*)
                      (*end of client code*)
                     with Guard x -> 
                      (*do some clean-up*)
                      x

	end in A.result
  in result

Now, any use of [set] or [get] will yield a result of type ['a A.t]. By
definition of local modules, this type can't escape the scope of [A],
which means that we can't store references to either value in an outside
reference, we can't put it into a continuation and it can't cross module
boundaries. Which means that we have safely used our resources. Yeah.

Unfortunately that's not always true, as there is a way for the client
code to sneak a continuation which can call [set]:

(*start of client code*)
   return (fun () -> ignore (set 99))
(*end of client code*)

I can then write [f () ()] and avoid the whole resource-protection
infrastructure :( 

Now, as far as I can tell, the only way of leaking unsafe operations is
to return a continuation which perform one of our local operations,
trigger the continuation and somehow ignore the value of the result.

Does anyone have ideas regarding how to prevent this kind of leaks? I'm
willing to resort to Camlp4 and/or advanced type hackery but not to
write my own type system.

Thanks in advance,
 David

P.S.:
 In case you're interested, such a design pattern would permit
definition of fast checked local and polymorphic exceptions without
monads, and might be applicable to some cases of types-and-effects.




-- 
David Teller-Rajchenbach
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations.