Re: Keeping local types local?

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

Thanks for the answer.

My hope is that, since OCaml does already perform some scope escape
analysis, this analysis could be hijacked into something more
restrictive with the help of some simple rewriting/staged compilation.

Now, I realise that monads (I'm unfamiliar with parametrised monads,
although I have the intuition that they are what I call "indexed
families of monads" in my own work -- I'll be sure to read your paper)
are a solution to the problem, possibly the only solution. My issue with
this is that monads are a quite un-ocamlish solution, which requires
rewriting every single line of code, largely losing the ability to
compose functions and affecting performances too much for my taste, not
to mention the problem of monad transformers.

So I'm looking for another way out. As far as both your examples and my
experiments seem to indicate, the only way of escaping scope is to
return a continuation which calls one of the protected functions and
ignores the result. So there is a relatively simple way of preventing
escapes, which can probably be done syntactically: forbidding
continuations. Now, that's a harsh measure so perhaps we can alleviate
it. Assuming we allow rewriting, we can possibly replace every single
function definition inside the scope with something a tad more drastic
-- I don't know what yet, but there may be a way.

Now, I have the feeling that this may require also modifying the
language, to introduce something which, to my intuition, looks like
implicit parameters. I'm not sure how deep such a modification should
run (perhaps Camlp4 is sufficient) but I have the feeling that such a
modification would also prove quite useful for adding type-classes to
OCaml, so if the depth is limited, it may be a good idea to achieve both
changes with one stroke.

What do you think?

Cheers,
 David

P.S.: I'll be sure to read your paper -- we seem to have many common
preoccupations of late.
P.P.S.: Sandboxing? Interesting idea. I was planning to get a few
students to implement dynamic  evaluation in OCaml but I hadn't thought
of using that for the purpose of sandboxing.

On Tue, 2008-09-16 at 03:12 -0700, oleg@okmij.org wrote:
> David Rajchenbach-Teller wrote:
> 
> > 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.
> 
> I don't think there is much hope. Without monads (or, better,
> parameterized monads) and without the effect type system, there is
> nothing to prevent the `escape'. The type system of OCaml is
> powerless: it can prevent the value 'v' of some type to be used
> outside the local module that declares that local type. However,
> nothing prevents us from forming a closure
> 	fun () -> consumer v; ()
> and using that closure anywhere we see fit. The closure has the
> `effect' of consuming the value, regardless of any bracketing
> boundaries. And yet its type is unit->unit. The problem with ML in
> general is precisely that the type of the function says absolutely
> nothing about the function's effects. It gets worse: there is a
> similar way to consume the value 'v' of a `local' type
> inappropriately: via an assignment. The consumer code may include the
> following:
> 
> 	let thunk = ref (fun () -> ())
> 
> 	let process () =
> 	     !thunk ();
> 	     thunk := fun () -> ignore (set v);
> 	     ...
> 
> The next invocation of the the process function of the consumer will
> execute set v, probably outside of the transaction
> boundaries. One should also worry about returning thunks via
> exceptions... 
> 
> Section 4.3 of
> 	http://okmij.org/ftp/Computation/resource-aware-prog/region-io.pdf
> as well as the accompanying code shows several attempts to break out
> of the region boundaries. As far as the Region-IO paper is concerned,
> all attempts failed. Because we do use monads, rank-2 polymorphism and
> because the type of the monad specifically reflects its effects. For
> fancier guarantees, one needs parameterized monads (which aren't
> actually monads), see Section 6 of the paper.
> 
> Rank-2 polymorphism is available in OCaml too. In fact, MetaOCaml uses
> this technique to prevent `escaping' of free variables, to make sure
> that only closed code could be run. Mutations and exceptions still
> pose the problem however.
> 
> Perhaps the best approach in OCaml now is sand-boxing. Although
> it is not advertised much, OCaml system is quite `reflective'. One can
> trivially adapt the main compiler driver so to compile a source code
> file in a `reduced' environment -- the environment that does not have
> the ref type, for example. By controlling the available operations and
> available types, we can restrict the effects; we should also define an
> appropriate variant (Int, Bool, pair, array -- but not a closure) and
> insist the return value be of that variant type. The return value
> must be serializable, and we should only permit assignments of
> serializable values. That may be sufficient for safety.
> 
> 
-- 
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.