Remove the concept of a shared objects

[nomeata]

previously, objects might have had a class identity that is not valid
across different actors, so we distinguished between shared and
non-shared objects. With is removed (#145), we no longer that
distinction; an object is a subtype of Shared if and only if all
fields are (same as for tuples, as one would expect).

This removes a bunch of code. It might be that Andreas could have
implemented this faster on his own than reviewing this PR, but I wanted
to sieze the opportunity to learn more about the type chekcker etc.

It is one of the clean-ups menionted in #81 (there are more left though).

It fixes #103.

[crusso]

@andreas, @nomeata Wasn't there another reason for this distinction though? A mutable class could be seen as immutable thus sharable via subtyping. If we serialize at the dynamic type, not the static type, we'll wind up serializing mutable state. Have we committed to serializing at static type?

[nomeata]

An object is just a record of closures. There are no mutable classes, just mutable fields.

An object with a public mutable field ought to be non-sharable (and I think this PR does not check that, thanks!).

An object with private mutable field, well, that field isn’t really part of the object. It is merely in the closure of the functions in the public fields. And then the question is just if these functions are sharable.

[nomeata]

An object with a public mutable field ought to be non-sharable (and I think this PR does not check that, thanks!).

Actually, objects with mutable fields are correctly recognized as non-shared. All is well.

[rossberg]

Yes, this is problematic, because it would imply

{var x : Nat} <: Shared

which doesn't make sense. It looks like your change currently rejects that, but that breaks transitivity of subtyping, so is not viable -- and I can still do

(new {var x : Nat} : {}) : Shared

Things will become more fishy with generics:

shared func send<T <: Shared>(x : T) = ...;

type R = {var x : Nat};
func f(r : R) = g<R>(r);

This would type-check, but what would it send?

[crusso]

What he said.

A halfway house might be to disallow forgetting of mutable fields via subtyping, but that's a bit gross...,

[nomeata]

Ouch, ok. So I guess objects are more than just tuples with named fields after all :-(

OTOH, if I drop a non-sharable field from an object, the remaining object is sharable. This is not specific to mutable fields:

{foo : Nat -> Nat} <: {} <: Shared

We’d have the same problem if larger tuples were subtypes of smaller ones (which ought to be a relatively benign feature, ought it not?)

Maybe the problem is that we try hard ot use subtyping to characterize sharable types, when the proposition “is sharable” simply is not a downward closed set in the partial order of subtypes?

[rossberg]

Correct, this applies to all non-sharable types of fields.

Maybe the problem is that we try hard ot use subtyping to characterize sharable types, when the proposition “is sharable” simply is not a downward closed set in the partial order of subtypes?

I don't think it makes a difference. If you were to use something else, say, type class constraints, you'd still have the same kind of problem as long as subtyping exists at all:

func f<T with Shared T>(x : T) = ...;

f<{}>({var x : Nat});

Though here, perhaps, you could argue that a coercive interpretation of subtyping would explain this away.

[nomeata]

I don’t see the problem with your example. Clearly f<{}> expects an empty object, so it can ignore additional fields.

I don't think it makes a difference.

It seems it does make a difference: If we don’t expect that “can be shared“ is a downset, then we no longer expect

“{var x : Nat} <: {}” and “{} sharable“ implies {var x: Nat} sharable

and the problem goes away.

Is “is sharable” an upward-closed predicate? I.e. for every t1 <: t2 , if t1 is sharable, then t2 is sharable? It seems so. And there is a good reason: If t1 is sharable, then there (morally) is a function send : t1 -> () that sends it. And, by subtyping, the same function is also able to send x : t2.

So maybe all problems go away as soon as soon as make Sharable a subtype (not supertype) of all sharable things? At least the subtyping relationship would be transitive again (I think).

[rossberg]

Under subtyping, T includes all values whose most specific type is a subtype of T, so "T is sharable", no matter how expressed, always extends to all subtype values. Unless you use a coercive interpretation of subtyping, which might get tricky in higher-order cases.

[nomeata]

Hmm, I see what you are saying: The value new { var x = 1 } is an element of the type {}.

So “t is sharable” makes no sense as a predicate on object types (because every object type contains sharable and non-sharable values), until we carve out the subset of values that are sharable. And that is exactly the purpose of the sharable attribute on objects. Too bad. But I learned something.

[rossberg]

I agree this is unfortunate. I wish there was a nicer solution, but I can't think of one.