The problem
If you have an affine type system, then objects and closures that return (from a method in the case of an object and from a function call in the case of the closure) an owned field cause major problems.
Object Example:
class Blarg
{
private owned<int> x = 0;
public owned<int> GetX()
{
return x;
}
}
let b = new Blarg()
let x = b.GetX()
let x’ = b.GetX()
You can get around this problem by breaking encapsulation. If the private fields are public and you grab them directly you can get the lifetime analyzer to ensure single ownership of a field. However, it would be nice if we could keep encapsulation and also breaking encapsulation isn’t really an option for closures.
The Proposed Solution
Dependent types, row polymorphism, affine types, and macros. Using an affine type system you can modify the type of the object (or closure) that you’re dealing wth after calling a method on it. I think the basic idea in literature is called session types. So if you knew which field you were giving away statically, then you could pass back a new object type that didn’t have the owned field present. Of course you’ll have to redeclare the object in a new variable because it will have a new type, but that’s where the macros come in handy. Basically, just redeclare the object in a new (hidden) scope with the same name and hide all the evidence that it’s going on.
Manually creating a bunch of different objects to handle any possible owned field being given away seems tedious, so I’m suggesting that you use row polymorphism to track the different possible objects. Typically you use row polymorphism to preserve fields that aren’t required by some method, but I’m also suggesting you tweak it some such that you kill off the owned field in the returned object/closure type. This should take care of any situation where it’s statically knowable which field is being given away.
However, maybe you don’t know statically which field is going to be given away. So you throw in dependent types and force all methods to be total to ensure that all programs must be statically analyzable.
Analysis of the proposed solution (plus some musing)
It feels like it would be really difficult to pull off. And if you pull it off I’m not sure that programming in that style would be productive or result in more comprehensible code. It seems like this method would preserve encapsulation and closures. And I also think it’s interesting that encapsulation and closures seem to fight against an affine type system. It’s also interesting that closures immediately start working like you would want them to if you allow copying any field that they return (or maybe it shouldn’t be *that* interesting because closures come from lambda calculus and beta reduction is just textual replacement).
Encapsulation and closures seem to live in a different world than affine types and it looks like getting them back in is a bit odious. I wonder if there isn’t an analogous idea that we can embed in an affine typed system such that we get all of the benefits of encapsulation and closures without needed to do backflips to handle returning owned fields.
[] - Okay, let’s convince ourselves that affine type systems by themselves are probably not going to be improved such that you can statically track the lifetime of an owned field in order to invalidate programs that give the field away twice.
class Blarg
{
private owned<int> x = 0;
private owned<int> y = 0;
public owned<int> GetUnknown( int z )
{
if ( blah_blah_halting_problem( z ) )
{
return x;
}
else
{
return y;
}
}
}
let dynamicInt = TrueRandomNumber()
let b = new Blarg()
let x = b.GetUnknown( dynamicInt )
let x’ = b.GetUnknown( dynamicInt + 1 )
Okay, I’m pretty sure there isn’t a static analysis technique in existence that will be able to determine whether or not single ownership of Blarg’s inner fields is being respected. No lifetime analysis technique should be powerful enough to defeat the halting problem. You’ll need something stronger like a non-turing complete language with dependent types.
No comments:
Post a Comment