FW: Why should a forward&backward compatible change make a new type?

From: Mike Spreitzer (spreitze@parc.xerox.com)
Date: Mon, Aug 30 1999


From: "Mike Spreitzer" <spreitze@parc.xerox.com>
To: "Andy Begel (E-mail)" <abegel@cs.berkeley.edu>
Cc: "IETF HTTP-NG discussion list (E-mail)" <ietf-http-ng@w3.org>, "John Lamping (E-mail)" <lamping@parc.xerox.com>
Date: Mon, 30 Aug 1999 15:12:31 PDT
Message-ID: <004201bef334$c16b3470$1776020d@phobos.parc.xerox.com>
Subject: FW: Why should a forward&backward compatible change make a new type?


FYI, an interesting conversation has sprung up with John Lamping as a
result of my Dealer on our flexible typing work.  Attached are the two
main messages.

Mike


attached mail follows:


From: "Mike Spreitzer" <spreitze@parc.xerox.com>
To: "John Lamping" <lamping@parc.xerox.com>
Cc: "Andy Begel" <abegel@cs.berkeley.edu>, "Doug Terry" <terry@parc.xerox.com>, "Richard Burton" <burton@parc.xerox.com>, "PARC HTTP-NG" <http-ng-parc@parc.xerox.com>
Subject: Why should a forward&backward compatible change make a new type?
Date: Fri, 9 Jul 1999 14:06:08 -0700
Message-ID: <000201beca4e$dd36f9a0$27d1000d@deimos.parc.xerox.com>

You asked this question at my Dealer this week, and I didn't have a
short,
sharp answer ready.  In this note I'll try to state, with reasonable
clarity, three reasons why not.

Specifically, the question refers to the example in which we start with
a
type

O1 = { m: {a:A} -> {x:X} }

and create an extension

O2 = { m: {a:A, b:optional:B} -> {x:X, y:optional:Y} }

The question is: why is the type {a:A, b:optional:B} not considered
equal
to the type {a:A}?  Following are three answers.

(1) It lets us tell a realistic story about field name collisions.  The
extensible record type {a:A} admits values that have a "b" field with a
non-"B" value.  I have considered formally banishing such a possibility,
by
saying that fields are identified not by simple names like "b" but by
some
kind of global unique identifier that is always associated with exactly
one
type.  The idea is that every time you write a new subtype that adds
fields, those fields have identifiers that are unique to the new
subtype.
For example, when Mark Andreeson extended HTTP/0.9's GET parameters with
a
set of format preferences (supposing he did), he might have written the
new
GET's parameter type like this:

{ch.cern.gamma/tbl/http/0.9/url: String,
 edu.u-illinois.uc/~andreeson/accept: optional: Preferences}

Even if someone else wanted to create a different extension with an
"accept" parameter, the full ID of his field would be different.  There
are
many different ways one can imagine creating the GUIDs for fields and
managing their eternal association with exactly one type --- many of
which
are not entirely reliable (e.g., users just write these things down, and
have to be sure the change them whenever they change any detail
reachable
from a GUID).  Having a formal basis that admits the possibility of
field
name collisions seems more appropriate for a world in which mistakes can
happen --- even though they're not supposed to occur in the normal case.

(2) If extension doesn't make new types, then the types don't tell us
much
about what's going on.  There are a number of ways in which types can be
used as meta-data.  In just one current example, Jini's lookup service
is
based on types.  If extended iterfaces didn't have new types, a Jini
directory won't tell you which services are extended and which aren't.
In
general, there's a well established trend in software engineering to use
types to convey information.  We *could* invent another "facet" of data
(aside from "types") and use it to convey extension information; putting
that information in the types struck me as going a more familiar route.

(3) Where extension and subtyping differ is at procedure types ---
that's
not something that can be changed even if we took different positions on
the above issues.  Recognizing that, you offered another framing of your
question as something like "is the point of extension that you use it
when
you *want* invocations to fail?".  I hestitate to agree, because coupled
with coarse types it lets you pass extended objects through third
parties
(and variables in programs) that won't be doing any invocations.

Mike Spreitzer <spreitze@parc.xerox.com>
http://parcweb.parc/spreitze/ (Xerox internal)
http://www.parc.xerox.com/spreitze/ (external)
+1-650-812-4833



attached mail follows:


From: "Mike Spreitzer" <spreitze@parc.xerox.com>
To: "'John Lamping'" <lamping@parc.xerox.com>
Cc: <abegel@cs.berkeley.edu>, <terry@parc.xerox.com>, <http-ng-parc@parc.xerox.com>
Subject: RE: Why should a forward&backward compatible change make a new type?
Date: Sat, 24 Jul 1999 01:26:48 -0700
Message-ID: <001501bed5ae$46180e40$27d1000d@deimos.parc.xerox.com>

Let me summarize where I think this discussion stands, and attempt to
move it forward a tiny bit.

You're proposing an alternate way of supporting evolution that doesn't
require as much innovation in the type system.  Specifically, your
proposal has: structural typing, extensible record types with two
"mode" dimensions per field ("optional/not" and
"ignorable/not/dontCare"), record values where each field is marked
"ignorable" or not, and a belief that we can formally banish field
name collision problems.  Your proposal does not have a new
"extension" type relation, nor does it have coarse types.  Instead, it
makes do with subtyping, by the novel expedient of having client and
server use different types to describe the server.  Specifically, when
taking an evolutionary step, the server creates and uses to describe
itself a subtype of its former type, while the client creates and uses
a supertype of the type it formerly used to describe its expectations
of the server.  Your system has the charm that it has clients and
servers describing themselves more precisely than the system I
proposed.

Here's a concrete (although unmotivated) example.  Both sides start
with a server type

       T = {a:A} -> {x:X}

(let me use a shorthand where a field is optional only if explicitly
marked so, and constrains the "ignorable" bit in the datum only if and
how explicitly marked).

The client has type

    T -> Foo

for some unimportant type Foo.  To take a backward and forward
compatible step, the new server adopts type

    S = {a:A, b:opt:B} -> {x:X, y:ign:Y}

while the client adopts type

      U -> Foo

where

	U = {a:A, b:ign:B} -> {x:X, y:opt:Y}

Part of the key is the subtyping relation among record types, whose
key features are: (1) fields not mentioned in the record type must be
marked "ignorable" in the record value, and (2) adding an optional
field to a record type is purely an expansion (because of feature 1)
of the set of acceptable values --- there is no contraction because of
a formal banishment of field naming collisions.

(You suggest banishing field name collisions by making the record
typing rule say that a type mismatch at an optional field does not
prevent the record value from having the considered record type.  I
don't favor that, as it seems rather sloppy; I'd rather take the
approach of letting field names be GUIDs.  There may be problems with
that approach too --- what's The One True field type for a given field
name in the presence of subtyping that restricts that field's type?
More thought is warranted on this issue.)

The upshot of your record typing rules are that

    {a:A, c:ign:C} <: {a:A} <: {a:A, b:opt:B}

(where "<:" means "is a subtype of").  For the example above, this
means that:

       S <: T <: U

and

	(U -> Foo) <: (T -> Foo)

So new servers can be used wherever old servers were expected, and new
clients can be used wherever old clients were expected.

Now let's work an example with less than complete forward/backward
compatability.  Let's add web-style per-request proxying:

	PI = {to: T}
	R = {a:A, pi:opt:PI} -> {x:X}

That is, a new server, having type R, is willing to entertain a
request (via the optional "pi" field) to act as a proxy.  It's also
willing to not be a proxy.  OTOH, a new client expects the following
type of servers:

	V = {a:A, pi:opt&~ign:PI} -> {x:X}

That is, the client reserves the right to supply or not supply a "pi"
field, but if it is supplied, it will be marked "non-ignorable".  Now,
while R, like S, is a subtype of T, V is not a supertype of T.  That's
because

      {a:A, pi:opt&~ign:PI}

is not a subtype of

   {a:A}

(rather, it's a supertype).

Thus, while a new server can be used by an old client, an old server
cannot be used by a new client (for all possible requests from new
clients).  Which is in fact an accurate reflection of what
combinations work (for all possible requests).  However, this starts
to make me nervous, as it runs up against the third reason I gave for
the design I proposed: the ability to pass an extended server around
through static places that won't make an invocation that would
discover the mismatch.

Seeking an example that illustrates the problem, consider what happens
when the client asks the proxy to talk to an extended server (e.g.,
extended as in the S/U example above)?  The client expects the proxy
to have type W:

     W = {a:A, pi:opt&~ign:PJ} -> {x:X, y:opt:Y}

for some PJ that we'll try to discern.  You might expect to write

    PJ = {to:U},

but we'll see that won't work.  Supposing the actual proxy has type R,
we need R to be a subtype of W (so the newest client can use the
proxy).  For that to be so, we need

   {a:A, pi:opt&~ign:PJ} <: {a:A, pi:opt:PI}.

To get that, we need PJ <: PI (maybe the field name collision issue
resolution interferes here, need to be careful about that).  Now, PJ
will have the form {to:Q}, for some origin server type Q.  To get PJ
<: PI, we need Q <: T.  Q=U doesn't work, because U isn't a subtype of
T.  A solution for Q <: T is Q=S.  And if you think about it, that's
not unreasonable: it means the newest client expects the proxy to be
willing to be told to forward the request to an S.  Hmm, no bad
example here.  But it does illustrate how tricky it is to reason about
this stuff.  OTOH, maybe it's reasoning that would have to be done
with my proposed system too (just without as much "compiler" support).
At the end of our meeting a couple weeks ago, you and Bill were
suggesting a way to ease the reasoning burden, but I haven't yet
understood what you were trying to suggest.  Can either of you
clarify?

Thanks,
Mike