Return is not quite introduction
Chip Morningstar <
chip@...>
2013-05-07 23:32:42 GMT
This may fall into the category of stating something obvious that everybody
else but me already knew, but:
I had a thought as I was rereading The Ode To The Granovetter Diagram in the
course of preparing a presentation I'm going to be giving.
In the capability paradigm, the standard list of ways one object can end up
with a reference to another object is typically articulated as 1) by
parenthood, 2) by endowment/construction, and 3) by introduction. I think
MarkM's thesis also ads 4) by initial conditions. We typically diagram this
stuff using unidirectional message patterns, and so we model the usual
programming language call-return pattern in the continuation passing style,
where the return is explicitly handled as a second message sent to an addressee
who was passed as a parameter in the first message that corresponds to the
call.
Our standard rhetoric about the logic of introduction starts with Alice holding
references to Bob and Carol and passing the Carol reference to Bob in a
message, with the representation that this can only happen if 1) Alice has a
reference to Bob, 2) Alice has a reference to Carol, and 3) Alice chooses to
send the message.
A call-return sequence allows the callee to introduce the caller to somebody,
but the constraints don't quite align with the three rules just articulated, in
that the callee does not (typically) acquire a reference to the caller merely
as a consequence of being called. Nevertheless, the callee *does* acquire the
means to pass a message to the caller via the return path. In other words, an
object can send a message to another object without a reference to the
recipient. Hmmm.
This doesn't really introduce any new semantic wrinkles, in the sense that we
can model call-return in a more complicated way, by passing a reference to a
single-use forwarder object rather than a reference to the caller itself (and
if we were doing this in true continuation passing style we'd need to do
something like this anyway to capture the context at the return point from
which computation is to resume). Nevertheless, this seems like a lot of
cumbersome mechanism that rather gums up the cleanliness of the explanation.
It makes me wonder if return should be treated as a special case in the
standard explanation, much as we treat connectivity by endowment/construction
as a special case (and I think it *is* such a special case, motivated by a
desire for clarity, since connectivity by construction can be modeled as
parenthood followed by introduction).
Chip
RSS Feed