Typed Syndicate
1 Overview
2 Types
Int
Bool
String
Byte  String
Symbol
U
★/  t
Discard
Bind
Facet  Name
Role
Stop
Field
Shares
Reacts
On  Start
On  Stop
Asserted
Retracted
Actor
Actor  With  Role
Sends
Realize
Branch
Effs
Tuple
Unit
Assertion  Set
→fn
proc
Computation
Value
Endpoints
Roles
Spawns
3 User Defined Types
define-type-alias
define-constructor
define-constructor*
assertion-struct
message-struct
4 Actor Forms
run-ground-dataspace
spawn
dataspace
start-facet
stop
on
on-start
on-stop
assert
know
send!
realize!
field
ref
set!
begin/  dataflow
during
during/  spawn
define/  query-value
define/  query-set
define/  query-hash
define/  dataflow
5 Expressions
ann
if
cond
else
when
unless
let
let*
lambda
λ
Λ
inst
define
define-tuple
match-define
begin
block
match
tuple
select
unit
error
+
-
*
<
>
<=
>=
=
even?
odd?
add1
sub1
max
min
zero?
positive?
negative?
current-inexact-milleseconds?
string=?
bytes->string/  utf-8
string->bytes/  utf-8
gensym
symbol->string
string->symbol
not
/
and
or
equal?
displayln
printf
~a
for/  fold
for/  list
for/  set
for/  sum
for
for/  first
6 Require & Provide
struct-out
6.1 Requiring From Outside Typed Syndicate
require/  typed
require-struct
7 Builtin Data Structures
observe
Observe
inbound
Inbound
outbound
Outbound
message
Message
7.1 Lists
List
empty
empty?
cons
cons?
first
second
rest
member?
reverse
partition
map
argmax
argmin
remove
length
list
7.2 Sets
Set
set
set-union
set-intersect
set-subtract
set-first
set-empty?
set-count
set-add
set-remove
set-member?
list->set
set->list
7.3 Hashes
Hash
hash
hash-set
hash-ref
hash-ref/  failure
hash-empty?
hash-has-key?
hash-count
hash-update
hash-update/  failure
hash-remove
hash-map
hash-keys
hash-values
hash-union
hash-union/  combine
hash-keys-subset?
7.4 Sequences
Sequence
empty-sequence
sequence->list
sequence-length
sequence-ref
sequence-tail
sequence-append
sequence-map
sequence-andmap
sequence-ormap
sequence-fold
sequence-count
sequence-filter
sequence-add-between
in-list
in-hash-keys
in-hash-values
in-range
in-set
7.5 Maybe
None
none
some
Some
Maybe
7.6 Either
left
Left
right
Right
Either
partition/  either
8 Behavioral Checking
8.12

Typed Syndicate🔗

 (require typed/syndicate/roles) package: syndicate-classic

1 Overview🔗

2 Types🔗

syntax

Int

syntax

Bool

syntax

String

syntax

ByteString

syntax

Symbol

Base types.

syntax

(U type ...)

The type representing the union of type ....

syntax

An alias for (U).

syntax

★/t

The type representing any possible assertion, and, in an AssertionSet, the possibility for an infinite set of assertions.

syntax

Discard

The type of _ patterns.

syntax

(Bind type)

The type of $ patterns.

syntax

FacetName

The type associated with identifiers bound by start-facet.

syntax

(Role (x) type ...)

The type of a facet named x and endpoints described by type ....

syntax

(Stop X type ...)

The type of a stop action.

syntax

(Field type)

The type of a field containing values of type.

syntax

(Shares type)

The type of an assert endpoint.

syntax

(Reacts EventDesc type ...)

 
EventDesc = OnStart
  | OnStart
  | (Asserted event-type)
  | (Retracted event-type)
The type of a on endpoint that reacts to events described by EventDesc with the behavior given by type ....

syntax

OnStart

syntax

OnStop

syntax

(Asserted type)

syntax

(Retracted type)

See Reacts.

syntax

(Actor type)

The type of an actor that operates in a dataspace with a certain communication type.

syntax

(ActorWithRole comm-type behavior-type)

An Actor type with the additional behavior-type describing the actor’s behavior in terms of a Role.

syntax

(Sends type)

The type of a send! action.

syntax

(Realize type)

The type of a realize! action.

syntax

(Branch type ...)

syntax

(Effs type ...)

Types that may arise in descriptions in Role types due to branching and sequencing.

syntax

(Tuple type ...)

The type of tuple expressions.

syntax

Unit

An alias for (Tuple).

syntax

(AssertionSet type)

The type for a set of assertions of a certain type. Note that these are not interoperable with the general purpose set data structures.

syntax

( (X ...) type)

Universal quantification over types.

syntax

( type ... (Computation (Value result-type)
                         (Endpoints ep-type ...)
                         (Roles role-type ...)
                         (Spawns spawn-type ...)))
The type of a function with parameters type ... that returns result-type. The type includes the effects of any actions performed by the function:
  • Endpoints: includes any endpoint installation effects, such as from assert and on.

  • Roles: includes any script action effects, such as from start-facet, stop, and send!.

  • Spawns: includes descriptions of any spawn actions.

syntax

(→fn type-in ... type-out)

Shorthand for a type with no effects.

syntax

(proc maybe-quantifiers type-in ... maybe-arrow type-out
      maybe-endpoints
      maybe-roles
      maybe-spawns)
 
maybe-quantifiers = 
  | #:forall (X ...)
     
maybe-arrow = 
  | 
  | ->
     
maybe-endpoints = 
  | #:endpoints (e ...)
     
maybe-roles = 
  | #:roles (r ...)
     
maybe-spawns = 
  | #:spawns (s ...)
A more convenient notation for writing (potentially polymorphic) function types with effects. Shorthand for ( (X ...) ( type-in ... (Computation (Value type-out) (Endpoints e ...) (Roles r ...) (Spawns s ...)))).

syntax

(Computation type ...)

syntax

(Value type)

syntax

(Endpoints type)

syntax

(Roles type)

syntax

(Spawns type)

See .

3 User Defined Types🔗

syntax

(define-type-alias id type)

(define-type-alias (ty-cons-id arg-id ...) type)
Define id to be the same as type, or create a type constructor (ty-cons-id ty ...) whose meaning is type with references to arg-id ... replaced by ty ....

syntax

(define-constructor (ctor-id slot-id ...)
      maybe-type-ctor
      maybe-alias ...)
 
maybe-type-ctor = 
  | #:type-constructor type-ctor-id
     
maybe-alias = 
  | #:with alias alias-body
Defines a container analagous to a prefab struct. Includes accessor functions for each slot-id. (But not, presently, a predicate function).

When a type-ctor-id is provided, the type of such structures is (type-ctor-id type ...), where each type describes the value of the corresponding slot. When not provided, the type constructor is named by appending "/t" to ctor-id.

Each alias and alias-body creates an instance of define-type-alias.

syntax

(define-constructor* (ctor-id : type-ctor-id slot-id ...)
      maybe-alias ...)
An abbreviated form of define-constructor.

syntax

(assertion-struct ctor-id : type-ctor-id (slot-id ...))

An abbreviated form of define-constructor.

syntax

(message-struct ctor-id : type-ctor-id (slot-id ...))

An abbreviated form of define-constructor.

4 Actor Forms🔗

syntax

(run-ground-dataspace type expr ...)

Starts a ground, i.e. main, dataspace of the program, with the given communication type and initial actors spawned by expr ....

syntax

(spawn maybe-type s)

 
maybe-type = 
  | type
Spawns an actor with behavior given by s. The type gives the communication type of the enclosing dataspace. When absent, type is supplied by the nearest lexically enclosing spawn or dataspace form, if any exist.

syntax

(dataspace type expr ...)

Spawns a dataspace with communication type type as a child of the dataspace enclosing the executing actor. The script expr ... spawns the initial actors of the new dataspace.

syntax

(start-facet id maybe-spec expr ...+)

 
maybe-spec = 
  | #:implements type
  | #:includes-behavior type
Start a facet with name id and endpoints installed through the evaluation of expr ....

syntax

(stop id expr ...)

Terminate the facet id with continuation script expr .... Any facets started by the continuation script survive the termination of facet id.

syntax

(on event-description body ...+)

 
event-description = start
  | stop
  | (message pattern)
  | (asserted pattern)
  | (retracted pattern)
     
pattern = _
  | ($ id type)
  | ($ id)
  | $id
  | $id:type
  | (ctor pattern ...)
  | expr
Creates an event handler endpoint that responds to the event specified by event-description. Executes the body ... for each matching event, with any pattern variables bound to their matched value.

Patterns have the following meanings:
  • _ matches anything.

  • ($ id type) matches any value and binds it to id with assumed type type.

  • ($ id) is like ($ id type), but attempts to use the current communication type to fill in the type of potential matches. May raise an error if no suitable communication type is in scope.

  • (? pred pattern) matches values where (pred val) is not #f and that match pattern.

  • $id:type is shorthand for ($ id type).

  • $id is shorthand for ($ id).

  • (ctor pat ...) matches values built by applying the constructor ctor to values matching pat .... ctor is usually a struct name.

  • expr patterns match values that are equal? to expr.

syntax

(on-start expr ...+)

Shorthand for (on start expr ...).

syntax

(on-stop expr ...+)

Shorthand for (on stop expr ...).

syntax

(assert expr)

Creates an assertion endpoint with the value of expr.

syntax

(know expr)

Creates an internal assertion endpoint with the value of expr.

syntax

(send! expr)

Broadcast a dataspace message with the value of expr.

syntax

(realize! expr)

Broadcast an actor-internal message with the value of expr.

syntax

(field [id maybe-type expr] ...)

 
maybe-type = 
  | type
  | : type
Defines fields of type type with names id and initial values expr. If type is not provided, the type of the initial expression is used as the type of the field.

syntax

(ref id)

Reference the field named id.

syntax

(set! id expr)

Update the value the field named id.

syntax

(begin/dataflow expr ...+)

Evaluate and perform the script expr ..., and then again each time a field referenced by the script updates.

syntax

(during pattern expr ...+)

Engage in behavior for the duration of a matching assertion. The syntax of pattern is the same as described by on.

syntax

(during/spawn pattern expr ...+)

Like during, but spawns an actor for the behavior expr ....

syntax

(define/query-value name absent-expr pattern expr
                    maybe-on-add
                    maybe-on-remove)
 
maybe-on-add = 
  | #:on-add on-add-expr
     
maybe-on-remove = 
  | #:on-remove on-remove-expr
Equivalent to the untyped untyped:define/query-value. The on-add-expr and on-remove-expr, when given, execute after name has been updated.

syntax

(define/query-set name pattern expr
                  maybe-on-add
                  maybe-on-remove)
 
maybe-on-add = 
  | #:on-add on-add-expr
     
maybe-on-remove = 
  | #:on-remove on-remove-expr
Equivalent to the untyped untyped:define/query-set.

syntax

(define/query-hash name pattern key-expr value-expr
                   maybe-on-add
                   maybe-on-remove)
 
maybe-on-add = 
  | #:on-add on-add-expr
     
maybe-on-remove = 
  | #:on-remove on-remove-expr
Equivalent to the untyped untyped:define/query-hash.

syntax

(define/dataflow name maybe-type expr)

 
maybe-type = 
  | type
Define a field named name, whose value is reevaluated to the result of expr each time any referenced field changes. When type is not supplied, the field has the type of the given expr.

5 Expressions🔗

syntax

(ann expr : type)

(ann expr type)
Ensure that expr has the given type.

syntax

(if test-expr then-expr else-expr)

The same as Racket’s racket:if.

syntax

(cond [test-expr body-expr ...+] ...+)

value

else : Bool = #t

Like Racket’s racket:cond.

syntax

(when test-expr expr)

Like Racket’s racket:when, but results in #f when test-expr is #f.

syntax

(unless test-expr expr)

Like Racket’s racket:unless, but results in #f when test-expr is #f.

syntax

(let ([id expr] ...) body ...+)

The same as Racket’s racket:let.

syntax

(let* ([id expr] ...) body ...+)

The same as Racket’s racket:let*.

syntax

(lambda ([x opt-: type] ...) expr ...+)

 
opt-: = 
  | :
Constructsa an anonymous function.

syntax

λ

Synonym for lambda.

syntax

(Λ (X ...) expr)

Parametric abstraction over type variables X ....

syntax

(inst expr type ...)

Instantiates the type variables X ... with type ..., where expr has type ( (X ...) t).

syntax

(define id : type expr)

(define id expr)
(define (id [arg-id opt-: arg-type] ... opt-res-ty) expr ...+)
(define ( (X ...) (id [arg-id opt-: arg-type] ... opt-res-ty)) expr ...+)
 
opt-: = 
  | :
     
opt-res-ty = 
  | arr res-type
     
arr = 
  | ->
Define a constant or a (potentially polymorphic) function. Note that the function name id is not bound in the body.

syntax

(define-tuple (id ...) expr)

Define id ... to each of the slots of the tuple produced by expr.

syntax

(match-define pattern expr)

Define the binders of pattern to the matching values of expr.

syntax

(begin expr ...+)

Sequencing form whose value and type is that of the final expr.

syntax

(block expr ...+)

Like begin, but also introduces a definition context for its body.

syntax

(match expr [pattern body-expr ...+] ...+)

Like Racket’s racket:match but with the pattern syntax described by on.

syntax

(tuple expr ...)

Constructs a tuple of arbitrary arity.

syntax

(select i expr)

Extract the ith element of a tuple.

value

unit : Unit = (tuple)

syntax

(error format-expr arg-expr ...)

Raises an exception using format-expr as a format string together with arg-expr ....

value

+ : (→fn Int Int Int)

value

- : (→fn Int Int Int)

value

* : (→fn Int Int Int)

value

< : (→fn Int Int Bool)

value

> : (→fn Int Int Bool)

value

<= : (→fn Int Int Bool)

value

>= : (→fn Int Int Bool)

value

= : (→fn Int Int Bool)

value

even? : (→fn Int Bool)

value

odd? : (→fn Int Bool)

value

add1 : (→fn Int Int)

value

sub1 : (→fn Int Int)

value

max : (→fn Int Int Int)

value

min : (→fn Int Int Int)

value

zero? : (→fn Int Bool)

value

positive? : (→fn Int Bool)

value

negative? : (→fn Int Bool)

value

current-inexact-milleseconds? : (→fn Int)

value

string=? : (→fn String String Bool)

value

bytes->string/utf-8 : (→fn ByteString String)

value

string->bytes/utf-8 : (→fn String ByteString)

value

gensym : (→fn Symbol Symbol)

value

symbol->string : (→fn Symbol String)

value

string->symbol : (→fn String Symbol)

value

not : (→fn Bool Bool)

syntax

(/ e1 e2)

syntax

(and e ...)

syntax

(or e ...)

syntax

(equal? e1 e2)

syntax

(displayln e)

syntax

(printf fmt-expr val-expr ...)

syntax

(~a e ...)

Primitive operations imported from Racket.

syntax

(for/fold ([acc-id maybe-:ty acc-expr] ...+)
          (for-clause ...)
  body-expr ...+)
 
maybe-:ty = 
  | : acc-type
     
for-clause = [id seq-expr]
  | [id : type seq-expr]
  | [(k-id v-id) hash-expr]
  | #:when test-expr
  | #:unless test-expr
  | #:break test-expr
Similar to Racket’s racket:for/fold.

When more than one acc-id is used, the body of the loop must evaluate to a tuple with one value for each accumulator, with the final tuple also being the result of the entire expression.

Each seq-expr should be of type Sequence, though expressions of type List and Set are automatically converted.

syntax

(for/list (for-clause ...) body ...+)

syntax

(for/set (for-clause ...) body ...+)

syntax

(for/sum (for-clause ...) body ...+)

syntax

(for (for-clause ...) body ...+)

syntax

(for/first (for-clause ...) body ...+)

Like their Racket counterparts. See for/fold for the description of for-clause.

Unlike racket:for/first, for/first returns a Maybe value to indicate success/failure.

6 Require & Provide🔗

syntax

(struct-out ctor-id)

6.1 Requiring From Outside Typed Syndicate🔗

syntax

(require/typed lib clause ...)

 
clause = [id : type]
  | opaque
     
opaque = [#:opaque type-name]
  | [#:opaque type-name #:arity op arity-nat]
     
opaque = =
  | >
  | >=
Import and assign types to bindings from outside Typed Syndicate.

Note that unlike Typed Racket, Typed Syndicate does not attach contracts to imported bindings.

An #:opaque declaration defines a type type-name (or, in the #:arity case, a type constructor) that may be used to describe imports but otherwise has no other operations.

syntax

(require-struct ctor-id #:as ty-ctor-id #:from lib maybe-omit-accs)

 
maybe-omit-accs = 
  | #:omit-accs
Import a Racket struct named ctor-id and create a type constructor ty-ctor-id for its instances.

Unless #:omit-accs is specified, defines the accessor functions for the struct.

7 Builtin Data Structures🔗

struct

(struct observe (claim))

  claim : any?

syntax

(Observe type)

Constructs an assertion of interest.

struct

(struct inbound (assertion))

  assertion : any?

syntax

(Inbound type)

Constructor for an assertion inbound from an outer dataspace.

struct

(struct outbound (assertion))

  assertion : any?

syntax

(Outbound type)

Constructor for an assertion outbound to an outer dataspace.

struct

(struct message (body))

  body : any?

syntax

(Message type)

Constructor for a broadcast message.

7.1 Lists🔗

syntax

(List type)

The type for cons lists whose elements are of type type.

value

empty : (List )

value

empty? : ( (X) (→fn (List X) Bool))

value

cons : ( (X) (→fn X (List X) (List X)))

value

cons? : ( (X) (→fn X (List X) Bool))

value

first : ( (X) (→fn (List X) X))

value

second : ( (X) (→fn (List X) X))

value

rest : ( (X) (→fn (List X) (List X)))

value

member? : ( (X) (→fn X (List X) Bool))

value

reverse : ( (X) (→fn (List X) (List X)))

value

partition : ( (X) (→fn (List X) (→fn X Bool) (List X)))

value

map : ( (X Y) (→fn (→fn X Y) (List X) (List Y)))

value

argmax : ( (X) (→fn (→fn X Int) (List X) X))

value

argmin : ( (X) (→fn (→fn X Int) (List X) X))

value

remove : ( (X) (→fn X (List X) (List X)))

value

length : ( (X) (→fn (List X) Int))

syntax

(list e ...)

Like their Racket counterparts.

7.2 Sets🔗

syntax

(Set type)

The type for sets whose elements are of type type.

syntax

(set e ...)

syntax

(set-union st ...+)

syntax

(set-intersect st ...+)

syntax

(set-subtract st ...+)

value

set-first : ( (X) (→fn (Set X) X))

value

set-empty? : ( (X) (→fn (Set X) Bool))

value

set-count : ( (X) (→fn (Set X) Int))

value

set-add : ( (X) (→fn (Set X) X (Set X)))

value

set-remove : ( (X) (→fn (Set X) X (Set X)))

value

set-member? : ( (X) (→fn (Set X) X Bool))

value

list->set : ( (X) (→fn (List X) (Set X)))

value

set->list : ( (X) (→fn (Set X) (List X)))

Like their Racket counterparts.

7.3 Hashes🔗

syntax

(Hash key-type value-type)

The type for key/value hash tables.

syntax

(hash key val ... ...)

value

hash-set : ( (K V) (→fn (Hash K V) K V (Hash K V)))

value

hash-ref : ( (K V) (→fn (Hash K V) K V))

value

hash-ref/failure : ( (K V) (→fn (Hash K V) K V V))

value

hash-empty? : ( (K V) (→fn (Hash K V) Bool))

value

hash-has-key? : ( (K V) (→fn (Hash K V) K Bool))

value

hash-count : ( (K V) (→fn (Hash K V) Int))

value

hash-update : ( (K V) (→fn (Hash K V) K (→fn V V) (Hash K V)))

value

hash-update/failure

 : ( (K V) (→fn (Hash K V) K (→fn V V) V (Hash K V)))

value

hash-remove : ( (K V) (→fn (Hash K V) K (Hash K V)))

value

hash-map : ( (K V R) (→fn (Hash K V) (→fn K V R) (List R)))

value

hash-keys : ( (K V) (→fn (Hash K V) (List K)))

value

hash-values : ( (K V) (→fn (Hash K V) (List V)))

value

hash-union

 : ( (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))

value

hash-union/combine

 : ( (K V) (→fn (Hash K V) (Hash K V) (→fn V V V) (Hash K V)))

value

hash-keys-subset?

 : ( (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) Bool))
Like their Racket counterparts. The /failure and /combine suffixes are in place of keyword arguments, which Typed Syndicate does not presently support.

7.4 Sequences🔗

syntax

(Sequence type)

The type for a sequence of type values.

value

empty-sequence : (Sequence )

value

sequence->list : ( (X) (→fn (Sequence X) (List X)))

value

sequence-length : ( (X) (→fn (Sequence X) Int))

value

sequence-ref : ( (X) (→fn (Sequence X) Int Int))

value

sequence-tail : ( (X) (→fn (Sequence X) Int (Sequence X)))

value

sequence-append

 : ( (X) (→fn (Sequence X) (Sequence X) (Sequence X)))

value

sequence-map

 : ( (A B) (→fn (→fn A B) (Sequence A) (Sequence B)))

value

sequence-andmap : ( (X) (→fn (→fn X Bool) (Sequence X) Bool))

value

sequence-ormap : ( (X) (→fn (→fn X Bool) (Sequence X) Bool))

value

sequence-fold : ( (A B) (→fn (→fn A B A) (Sequence B) A))

value

sequence-count : ( (X) (→fn (→fn X Bool) (Sequence X) Int))

value

sequence-filter

 : ( (X) (→fn (→fn X Bool) (Sequence X) (Sequence X)))

value

sequence-add-between : ( (X) (→fn (Sequence X) X (Sequence X)))

value

in-list : ( (X) (→fn (List X) (Sequence X)))

value

in-hash-keys : ( (K V) (→fn (Hash K V) (Sequence K)))

value

in-hash-values : ( (K V) (→fn (Hash K V) (Sequence V)))

value

in-range : (→fn Int (Sequence Int))

value

in-set : ( (X) (→fn (Set X) (Sequence X)))

Like their Racket counterparts.

7.5 Maybe🔗

syntax

None

value

none : None

struct

(struct some (v))

  v : any?

syntax

(Some type)

syntax

(Maybe type)

(Maybe type) is an alias for (U None (Some type)).

7.6 Either🔗

struct

(struct left (v))

  v : any?

syntax

(Left type)

struct

(struct right (v))

  v : any?

syntax

(Right type)

syntax

(Either left-type right-type)

(Either left-type right-type) is an alias for (U (Left left-type) (Right right-type)).

value

partition/either

 : ( (X Y Z) (→fn (List X) (→fn X (Either Y Z)) (Tuple (List Y) (List Z))))
Partition a list based on a function that returns an Either value.

8 Behavioral Checking🔗