Sunday, June 12, 2005

understanding object calculi

So, Abadi and Cardelli came up with an object calculus.

b ::= x
| [ l = \varsigma (x) b ... ]
| a.l
| (a.l <= \varsigma (x) b)

When I was digesting this, at some point I wondered, "is the fourth production just sugar for the second?" And I played around with it and decided, "no, its not just sugar, because at the point of update, we don't know all of the implementations that our self might be currently carrying. So this is a fundamental operation; it is not macro-expressible in terms of the other forms in the language."

However, this led me to consider the other direction: "is the second production just sugar for the fourth?" This is obviously false; without the second production, we'd have no base case capable of defining a closed term, and we'd be screwed. BUT, there is a much simpler formuation, where you predefine a constant Useless which dies on any attempt to use any of its methods (and it has every method in our label set defined). Then, it seems to me that we could define the second production in terms of the fourth production and Useless. Why didn't they go down this route, which would appear to simplify things?

If you're not happy about having an object that is magic (in that it has every method "implemented", though the implementation seems to match exactly what Abadi and Cardelli's model would have done in such situations), then instead we could not use Useless, but instead simplify the second production to [l_1 ... l_n], and now this defines an object which has l_1 through l_n predefined with some default implementation (like returning self). Again, this seems like it would simplify the calculus, since there's now really only that fourth production in the grammar where all the power is lurking.

But maybe I'm crazy.

2 Comments:

Blogger pnkfelix said...

In your system with "Useless", or with some basis of labels, every type would always include every label and no method call or method update would ever fail. Abadi and Cardelli need to differentiate call and update from construction because one constructs a value and the others use it - one creates a lower bound on a type, the others create an upper bound.

Method update cannot be used for object construction because you can only update a method which exists, and you can't start with a "default" implementation of a method of arbitrary type. Object construction cannot replace method update in the case where an object has "selftype" - you may be updating an object with an arbitrary set of "extra" labels beyond those known statically at the udpate point.

Does this clear it up?

10:17 AM  
Blogger pnkfelix said...

You're right, I totally forgot about the role of the type system in all of this. If we want to be able to employ a static reasoning system, we need some way of getting an idea of what the intended (allowable) behaviors are.

So, did Abadi and Cardelli just present an object system with no type system, but design it in a way where they were planning for a type system to be introduced? Or did they introduce a type system, and you just aren't presenting it here? I got the impression from your writing that the type system is due to Jim and Palsberg

1:28 PM  

Post a Comment

<< Home