Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Kill Shared type #560

Merged
merged 6 commits into from
Jul 15, 2019
Merged
Show file tree
Hide file tree
Changes from 4 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion design/Syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -113,7 +113,7 @@ Productions marked * probably deferred to later versions.
<exp> expression
let <pat> = <exp> immutable
var <id> (: <typ>)? = <exp> mutable
(new|object|actor|shared) <id>? =? { <exp-field>;* } object
(new|object|actor) <id>? =? { <exp-field>;* } object
shared? func <id>? <typ-params>? <pat> (: <typ>)? =? <exp> function
type <id> <typ-params>? = <typ> type
actor? class <id> <typ-params>? <pat> (: <typ>)? =? <exp> class
Expand Down
15 changes: 7 additions & 8 deletions guide/as-slides.md
Original file line number Diff line number Diff line change
Expand Up @@ -108,9 +108,9 @@ structural record types, JS-like, fields can be mutable

* `{var x : Int; color : Color}`

* `shared {x : Int; color: Color}`
* `{x : Int; color: Color}`

shared (think serializable) objects have immutable fields of sharable types.
objects with immutable fields of sharable types are sharable.

### Actor types

Expand Down Expand Up @@ -188,7 +188,7 @@ AS distinguishes sharable types:

- all primitive types are sharable (scalars + text)
- any `shared` function type is sharable
- any `shared` object type is sharable
- an object type is sharable if it's fields are sharable and immutable
- any `actor` type is sharable
- `[T]` and `?T` are sharable if `T` is sharable.
- `(T1,...,Tn)` is sharable if `T1`,..., `Tn` all sharable.
Expand All @@ -197,8 +197,7 @@ AS distinguishes sharable types:

### ... Sharability

* `shared` functions must have sharable arguments and return `()` or async `T`, where `T` sharable
* `shared` object must have sharable fields
* `shared` functions must have sharable arguments and return `()` or async `T`, where `T` sharable
* actor fields must re `shared` functions

(actors \& shared functions serialized by *reference*, other types serialzed by *value*)
Expand All @@ -224,12 +223,12 @@ AS distinguishes sharable types:
* Unary & binary, arithmetic & logical operators
- `- x`, `not b`, `a + b`, `a & b` ...

### (Shared) Objects
### (Sharable) Objects

* `shared` (think serializable) objects have immutable fields of sharable type:
* sharable (think serializable) objects have immutable fields of sharable type:

```
shared { x = 0; color = Colors.Red }
{ x = 0; color = Colors.Red }
```

* full `object`s can be mutable, stateful
Expand Down
4 changes: 2 additions & 2 deletions guide/chat.as
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ type Post = shared Text -> ();
actor Server = {
private var clients : List<Client> = null;

private shared broadcast(message : Text) {
private shared func broadcast(message : Text) {
var next = clients;
loop {
switch next {
Expand All @@ -18,7 +18,7 @@ actor Server = {
};
};

subscribe(client : Client) : async Post {
func subscribe(client : Client) : async Post {
let cs = new {head = client; var tail = clients};
clients := ?cs;
return broadcast;
Expand Down
78 changes: 34 additions & 44 deletions guide/guide.md
Original file line number Diff line number Diff line change
Expand Up @@ -328,7 +328,7 @@ Type expressions are used to specify the types of arguments, constraints (a.k.a
```
<typ> ::= type expressions
<id> <typ-args>? constructor
(shared|actor)? { <typ-field>;* } object
actor? { <typ-field>;* } object
[ var? <typ> ] array
Null null type
? <typ> option
Expand Down Expand Up @@ -436,16 +436,12 @@ representation is applied.

## Object types

`(shared|actor)? { <typ-field>;* }` specifies an object type by listing its zero or more named *type fields*.
`actor? { <typ-field>;* }` specifies an object type by listing its zero or more named *type fields*.

Within an object type, the names of fields must be distinct.

Object types that differ only in the ordering of the fields are equivalent.

The optional qualifier `shared` constrains the object's field to have *sharable* type.

Messages (see below) always requires arguments of *sharable* (think *serializable*) type.

The optional qualifier `actor` constrains the object's fields to be *shared* functions (i.e. messages).


Expand Down Expand Up @@ -496,10 +492,6 @@ No value has type `None`.

As an empty type, `None` can be used to specify the impossible return value of an infinite loop or unconditional trap.

## Shared type

Type `Shared` is the super-type of all types that can be transmitted between actors (i.e. sent or received) as the arguments or return values of `shared` functions.


## Parenthesised type

Expand Down Expand Up @@ -569,16 +561,15 @@ type parameter.

## Well-formed types

A type `T` is well-formed only if (recursively) its constituent types are well-formed,and:
A type `T` is well-formed only if (recursively) its constituent types are well-formed, and:

* if `T` is `async U` then `U <: Shared`, and
* if `T` is `shared < ... > V -> W` then `...` is empty, `U <: Shared` and
`W == ()` or `W == async W`, and
* if `T` is `async U` then `U` is shared, and
* if `T` is `shared < ... > V -> W` then `...` is empty, `U` is shared and
`W == ()` or `W == async W'`, and
* if `T` is `C<T0, ..., TN>` where:
* a declaration `type C<X0 <: U0, Xn <: Un> = ...` is in scope, and
* `Ti <: Ui[ T0/X0, ..., Tn/Xn ]`, for each `0 <= i <= n`.
* if `T` is `actor { ... }` then all fields in `...` are immutable and have `shared` function type.
* if `T` is `shared { ... }` then all fields in `...` are immutable and have a type that subtypes `Shared`.

## Subtyping

Expand Down Expand Up @@ -631,16 +622,19 @@ Two types `T`, `U` are related by subtyping, written `T <: U`, whenever, one of

* For some type `V`, `T <: V` and `V <: U` (*transitivity*).

* `U` is type `Shared` and `T` is equivalent to:
* a `shared` function type, or
* a `shared` object type, or
* a `actor` object type, or
* a scalar primitive type, or
* the type `Text`, or
* an immutable array type `[V]` with `V <: Shared`, or
* the type `Null`, or
* an option type `? V` with `V <: Shared`, or
* a tuple type `(T0, ..., Tn)` where, for each `0 <= i <= n`, `Ti <: Shared`.
## Sharability

A type `T` is *shared* if it is
* a `shared` function type, or
* an object type where all fields are non-`var` and have shared type, or
* an `actor` object type, or
* a scalar primitive type, or
* the type `Text`, or
* an immutable array type `[V]` where `V` is shared, or
* the type `Null`, or
* an option type `? V` where `V` is shared, or
* a tuple type `(T0, ..., Tn)` where, for each `0 <= i <= n`, `Ti` is shared.


# Literals

Expand Down Expand Up @@ -980,7 +974,7 @@ Otherwise, `r2` is false and the result is `()`.

The for expression `for ( <pat> in <exp1> ) <exp2>` has type `()` provided:

* `<exp1>` has type `(object|shared) { Next : () -> ?T; }`;
* `<exp1>` has type `{ next : () -> ?T; }`;
* pattern `<pat>` has type `U`; and,
* expression `<exp2>` has type `()` (in the environment extended with `<pat>`'s bindings).

Expand All @@ -990,19 +984,18 @@ The `for`-expression is syntactic sugar for
for ( <pat> in <exp1> ) <exp2> :=
{
let x = <exp1>;
label l
loop {
switch (x.Next()) {
label l loop {
switch (x.next()) {
case (? <pat>) <exp2>;
case (null) break l;
};
};
};
}
}
}
```

where `x` is fresh identifier.

In particular, the `for` loops will trap if evaluation of `<exp1>` traps; as soon as some value of `x.Next()` traps or the value of `x.Next()` does not match pattern `<pat>`.
In particular, the `for` loops will trap if evaluation of `<exp1>` traps; as soon as some value of `x.next()` traps or the value of `x.next()` does not match pattern `<pat>`.


_TBR: do we want this semantics? We could, instead, skip values that don't match `<pat>`?_
Expand Down Expand Up @@ -1066,7 +1059,7 @@ TBR async traps?
The async expression `async <exp>` has type `async T` provided:

* `<exp>` has type `T`;
* `T <: Shared`.
* `T` is shared.

Any control-flow label in scope for `async <exp>` is not in scope for `<exp>` (that `<exp>` may declare its own, local, labels.

Expand All @@ -1082,8 +1075,8 @@ Evaluation of `async <exp>` queues a message to evaluate `<exp>` in the nearest
The `await` expression `await <exp>` has type `T` provided:

* `<exp>` has type `async T`,
* `T <: Shared`.
* the `await` is explicitly enclosed by an `async`-expression or its nearest enclosing function is `shared`.
* `T` is shared,
* the `await` is explicitly enclosed by an `async`-expression.

`await <exp>` evaluates `<exp>` to a result `r`. If `r` is `trap`, evaluation returns `trap`. Otherwise `r1` is a promise. If the promise is complete with value `v`, then `await <exp>` evaluates to value `v`. If the `promise` is incomplete, that is, its evaluation is still pending, `await <exp>` suspends evaluation of the neared enclosing `async` or `shared`-function, adding the suspension to the wait-queue of the `promise`. Execution of the suspension is resumed once the promise is completed (if ever).

Expand Down Expand Up @@ -1193,7 +1186,7 @@ matching `<pat1>`, if it succeeds, or the result of matching `<pat2>`, if the fi
<exp> expression
let <pat> = <exp> immutable
var <id> (: <typ>)? = <exp> mutable
(new|object|actor|shared) <id>? =? { <exp-field>;* } object
(new|object|actor) <id>? =? { <exp-field>;* } object
shared? func <id>? <typ-params>? <pat> (: <typ>)? =? <exp> function
type <id> <typ-params>? = <typ> type
obj_sort? class <id> <typ-params>? <pat> =? { <exp-field>;* }` class
Expand Down Expand Up @@ -1257,9 +1250,9 @@ In scope of the declaration `type C < X0<:T0>, ..., Xn <: Tn > = U`, any well-

## Object Declaration

Declaration `(new|object|actor|shared) <id>? =? { <exp-field>;* }` declares an object with optional identifier `<id>` and zero or more fields `<exp_field>;*`.
Declaration `(new|object|actor) <id>? =? { <exp-field>;* }` declares an object with optional identifier `<id>` and zero or more fields `<exp_field>;*`.

The qualifier `new|object|actor|shared` specifies the *sort* of the object's type (`new` is equivalent to `object`). The sort imposes restrictions on the types of the non-private object fields and the sharability of the object itself.
The qualifier `new|object|actor` specifies the *sort* of the object's type (`new` is equivalent to `object`). The sort imposes restrictions on the types of the non-private object fields.

Let `T = sort { [var0] id0 : T0, ... , [varn] idn : T0 }` denote the type of the object.
Let `<dec>;*` be the sequence of declarations in `<exp_field>;*`.
Expand All @@ -1276,11 +1269,8 @@ Note that requirement 1. imposes further constraints on the fields type of `T`.
In particular:

* if the sort is `actor` then all non-private fields must be non-`var` (immutable) `shared` functions (the public interface of an actor can only provide asynchronous messaging via shared functions).
* if the sort is `shared` then all non-private field must be non-`var` (immutable) and of a type that is sharable (`T(idi) <: Shared`). Shared objects can be sent
as arguments to `shared` functions or returned as the result of a `shared`
function (wrapped in a promise).

Evaluation of `(new|object|actor|shared) <id>? =? { <exp-field>;* }` proceeds by
Evaluation of `(new|object|actor) <id>? =? { <exp-field>;* }` proceeds by
evaluating the declarations in `<dec>;*`. If the evaluation of `<dec>;*` traps, so does the object declaration.
Otherwise, `<dec>;*` produces a set of bindings for identifiers in `Id`.
let `v0`, ..., `vn` be the values or locations bound to identifiers `<id0>`, ..., `<idn>`.
Expand Down Expand Up @@ -1322,7 +1312,7 @@ where:
* `<typ-field>;*` is the set of non-`private` field types inferred from `<exp_field;*>`.
* `<id_this>?` is the optional `this` parameter of the object instance.

_TBR can we delete `new'?_
_TBR can we delete `new`?_

## Expression Fields

Expand Down
2 changes: 1 addition & 1 deletion samples/app/server.as
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ actor class Server() = {
nextId += 1;
let cs = new {head = c; var tail = clients};
clients := ?cs;
return (shared {
return (new {
post = shared func(message : Text) {
if (not c.revoked) broadcast(c.id, message);
};
Expand Down
4 changes: 1 addition & 3 deletions samples/app/types.as
Original file line number Diff line number Diff line change
@@ -1,6 +1,4 @@
type Subscription = shared {
type Subscription = {
post : shared Text -> (); // revokable by Server
cancel : shared () -> ();
};


13 changes: 10 additions & 3 deletions src/as_def/arrange.ml
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ let rec exp e = match e.it with
| FuncE (x, s, tp, p, t, e') ->
"FuncE" $$ [
Atom (Type.string_of_typ e.note.note_typ);
Atom (Arrange_type.sharing s.it);
func_sort s;
Atom x] @
List.map typ_bind tp @ [
pat p;
Expand Down Expand Up @@ -97,7 +97,14 @@ and case c = "case" $$ [pat c.it.pat; exp c.it.exp]

and pat_field pf = pf.it.id.it $$ [pat pf.it.pat]

and obj_sort s = Arrange_type.obj_sort s.it
and obj_sort s = match s.it with
| Type.Object -> Atom "Object"
| Type.Actor -> Atom "Actor"
| Type.Module -> Atom "Module"

and func_sort s = match s.it with
| Type.Local -> Atom "Local"
| Type.Shared -> Atom "Shared"

and mut m = match m.it with
| Const -> Atom "Const"
Expand Down Expand Up @@ -133,7 +140,7 @@ and typ t = match t.it with
| OptT t -> "OptT" $$ [typ t]
| VariantT cts -> "VariantT" $$ List.map typ_tag cts
| TupT ts -> "TupT" $$ List.map typ ts
| FuncT (s, tbs, at, rt) -> "FuncT" $$ [Atom (Arrange_type.sharing s.it)] @ List.map typ_bind tbs @ [ typ at; typ rt]
| FuncT (s, tbs, at, rt) -> "FuncT" $$ [func_sort s] @ List.map typ_bind tbs @ [ typ at; typ rt]
| AsyncT t -> "AsyncT" $$ [typ t]
| ParT t -> "ParT" $$ [typ t]

Expand Down
6 changes: 3 additions & 3 deletions src/as_def/syntax.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ type typ_id = (string, Type.con option) Source.annotated_phrase

(* Types *)

type sharing = Type.sharing Source.phrase
type obj_sort = Type.obj_sort Source.phrase
type func_sort = Type.func_sort Source.phrase

type mut = mut' Source.phrase
and mut' = Const | Var
Expand All @@ -39,7 +39,7 @@ and typ' =
| OptT of typ (* option *)
| VariantT of typ_tag list (* variant *)
| TupT of typ list (* tuple *)
| FuncT of sharing * typ_bind list * typ * typ (* function *)
| FuncT of func_sort * typ_bind list * typ * typ (* function *)
| AsyncT of typ (* future *)
| ParT of typ (* parentheses, used to control function arity only *)

Expand Down Expand Up @@ -126,7 +126,7 @@ and exp' =
| AssignE of exp * exp (* assignment *)
| ArrayE of mut * exp list (* array *)
| IdxE of exp * exp (* array indexing *)
| FuncE of string * sharing * typ_bind list * pat * typ option * exp (* function *)
| FuncE of string * func_sort * typ_bind list * pat * typ option * exp (* function *)
| CallE of exp * typ list * exp (* function call *)
| BlockE of dec list (* block (with type after avoidance)*)
| NotE of exp (* negation *)
Expand Down
Loading