Version française
Home     About     Download     Resources     Contact us    
Browse thread
Keeping local types local?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: oleg@o...
Subject: Keeping local types local?

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.