Don't use syndicate's action-collecting module-begin

Implicitly starting a dataspace with top-level actions is a hole for
the type system, which needs to know the type of possible assertions.

Instead, provide `run-ground-dataspace` for kicking off the program.

racket/syndicate/examples/actor/chat-client-tcp2.rkt

@@ -13,4 +13,6 @@
        (define stdin-evt (read-bytes-line-evt (current-input-port) 'any))
        (stop-when (message (inbound (external-event stdin-evt (list (? eof-object? _))))))
        (on (message (inbound (external-event stdin-evt (list (? bytes? $line)))))
-           (send! (tcp-out id line))))
+           (send! (tcp-out id line))
+           ;; chat-tcp2 uses the line-reader, so need line separators.
+           (send! (tcp-out id #"\n"))))

racket/typed/drivers/tcp.rkt

@@ -0,0 +1,117 @@
+#lang typed/syndicate/roles
+
+(provide activate!
+         tcp-connection
+         tcp-accepted
+         tcp-out
+         tcp-in
+         tcp-in-line
+         tcp-address
+         tcp-listener
+         seal
+         advertise
+         Tcp2LineReaderFactory
+         Tcp2Driver)
+
+(require-struct tcp-connection
+                #:as TcpConnection
+                #:from syndicate/drivers/tcp2)
+
+(require-struct tcp-accepted
+                #:as TcpAccepted
+                #:from syndicate/drivers/tcp2)
+
+(require-struct tcp-out
+                #:as TcpOut
+                #:from syndicate/drivers/tcp2)
+
+(require-struct tcp-in
+                #:as TcpIn
+                #:from syndicate/drivers/tcp2)
+
+(require-struct tcp-in-line
+                #:as TcpInLine
+                #:from syndicate/drivers/tcp2)
+
+(require-struct tcp-address
+                #:as TcpAddress
+                #:from syndicate/drivers/tcp2)
+
+(require-struct tcp-listener
+                #:as TcpListener
+                #:from syndicate/drivers/tcp2)
+
+(require-struct tcp-channel
+                #:as TcpChannel
+                #:from syndicate/drivers/tcp)
+
+(require-struct tcp-handle
+                #:as TcpHandle
+                #:from syndicate/drivers/tcp)
+
+(require-struct seal
+                #:as Seal
+                #:from syndicate/lang)
+
+(require-struct advertise
+                #:as Advertise
+                #:from syndicate/protocol/advertise)
+
+;; assertions and messages sent & received by the 'tcp2-listen-driver
+(define-type-alias Tcp2ListenDriver
+  (U (Observe (Observe (TcpConnection ★/t (TcpListener ★/t))))
+     (Observe (TcpConnection ★/t (TcpListener Int)))
+     (Observe (TcpConnection ★/t (TcpListener Int)))
+     (Advertise (Observe (TcpChannel ★/t (TcpListener (TcpHandle (Seal ★/t)) ★/t))))
+     (Observe (Advertise (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ★/t)))
+     (TcpAccepted ★/t)
+     (Advertise (TcpChannel (TcpHandle (Seal ★/t)) (TcpAddress String Int) ★/t))
+     (Observe (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ★/t))
+     (Message (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ByteString))
+     (Message (TcpIn (Seal ★/t) ByteString))
+     (Observe (TcpOut (Seal ★/t) ★/t))
+     (Message (TcpOut (Seal ★/t) ByteString))
+     (Message (TcpChannel (TcpHandle (Seal ★/t)) (TcpAddress String Int) ByteString))))
+
+;; assertions and messages sent & received by the 'tcp2-connect-driver
+(define-type-alias Tcp2ConnectDriver
+  (U (Observe (TcpConnection ★/t (TcpAddress ★/t ★/t)))
+     (TcpConnection Symbol (TcpAddress String Int))
+     (Observe (Advertise (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ★/t)))
+     (TcpAccepted ★/t)
+     (Advertise (TcpChannel (TcpHandle (Seal ★/t)) (TcpAddress String Int) ★/t))
+     (Observe (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ★/t))
+     (Message (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ByteString))
+     (Message (TcpIn ★/t ByteString))
+     (Observe (TcpOut ★/t ★/t))
+     (Message (TcpOut ★/t ByteString))
+     (Message (TcpChannel (TcpHandle (Seal ★/t)) (TcpAddress String Int) ByteString))))
+
+;; assertions and messages sent & received by the 'tcp2-line-reader-factory
+(define-type-alias Tcp2LineReaderFactory
+  (U (Observe (Observe (TcpInLine ★/t ★/t)))
+     (Observe (TcpInLine ★/t ★/t))
+     (Observe (TcpIn ★/t ★/t))
+     (Message (TcpIn ★/t ByteString))
+     (Message (TcpInLine ★/t ByteString))))
+
+(define-type-alias Tcp2Driver
+  (U Tcp2ListenDriver
+     Tcp2ConnectDriver
+     Tcp2LineReaderFactory))
+
+(require/typed syndicate/drivers/tcp2)
+(require/typed (submod syndicate/drivers/tcp2 syndicate-main)
+               [activate! : (→ (Computation (Value (U))
+                                            (Endpoints)
+                                            (Roles)
+                                            (Spawns (Actor Tcp2Driver))))])
+
+;; TODO
+;;
+;; The tcp2 driver also "activates" the tcp driver, so in order to be sound the typed driver ought to
+;; indicate through the types that whatever assertions and messages that driver does can also happen.
+;;
+;; The require/activate model doesn't lend itself to the current workings of the type system very
+;; easily. Perhaps a require/activate/typed would be in order, where the provided type describes the
+;; dataspace type of the actors that get spawned.

racket/typed/example.rkt

@@ -0,0 +1,27 @@
+#lang typed/syndicate
+
+(define-type-alias ds-type
+   (U (Observe (Tuple String ★)) (Tuple String Int)))
+
+(dataspace ds-type
+
+           (spawn ds-type
+                  (facet _
+                         (fields [the-thing Int 0])
+                         (assert (tuple "the thing" (ref the-thing)))
+                         (on (asserted (tuple "set thing" (bind new-v Int)))
+                             (set! the-thing new-v))))
+
+           (spawn ds-type
+                  (let [k (λ [10 (begin)]
+                            [(bind x Int)
+                             (facet _ (fields)
+                                    (assert (tuple "set thing" (+ x 1))))])]
+                    (facet _ (fields)
+                           (on (asserted (tuple "the thing" (bind x Int)))
+                               (k x)))))
+
+           (spawn ds-type
+                  (facet _ (fields)
+                         (on (asserted (tuple "the thing" (bind t Int)))
+                             (displayln t)))))

racket/typed/examples/bank-account.rkt

@@ -0,0 +1,62 @@
+#lang typed/syndicate
+
+(define-constructor (account balance)
+  #:type-constructor AccountT
+  #:with Account (AccountT Int)
+  #:with AccountRequest (AccountT ★))
+
+(define-constructor (deposit amount)
+  #:type-constructor DepositT
+  #:with Deposit (DepositT Int)
+  #:with DepositRequest (DepositT ★))
+
+(define-type-alias ds-type
+  (U Account
+     (Observe AccountRequest)
+     (Observe (Observe AccountRequest))
+     Deposit
+     (Observe DepositRequest)
+     (Observe (Observe DepositRequest))))
+
+(dataspace ds-type
+
+           (spawn ds-type
+                  (facet _
+                         (fields [balance Int 0])
+                         (assert (account (ref balance)))
+                         (on (asserted (deposit (bind amount Int)))
+                             (set! balance (+ (ref balance) amount)))))
+
+           (spawn ds-type
+                  (facet _
+                         (fields)
+                         (on (asserted (account (bind amount Int)))
+                             (displayln amount))))
+
+           (spawn ds-type
+                  (facet _
+                         (fields)
+                         (on (asserted (observe (deposit discard)))
+                               (facet _
+                                      (fields)
+                                      (assert (deposit 100))
+                                      (assert (deposit -30)))))))
+
+#|
+;; Hello-worldish "bank account" example.
+
+(struct account (balance) #:prefab)
+(struct deposit (amount) #:prefab)
+
+(spawn (field [balance 0])
+       (assert (account (balance)))
+       (on (message (deposit $amount))
+           (balance (+ (balance) amount))))
+
+(spawn (on (asserted (account $balance))
+           (printf "Balance changed to ~a\n" balance)))
+
+(spawn* (until (asserted (observe (deposit _))))
+        (send! (deposit +100))
+        (send! (deposit -30)))
+|#

racket/typed/examples/core/bank-account.rkt

@@ -0,0 +1,63 @@
+#lang typed/syndicate/core
+
+(define-constructor (account balance)
+  #:type-constructor AccountT
+  #:with Account (AccountT Int))
+
+(define-constructor (transaction id amount)
+  #:type-constructor TransactionT
+  #:with Transaction (TransactionT Int Int))
+
+(define-type-alias τc
+  (U Account
+     Transaction
+     (Observe (AccountT ★/t))
+     (Observe (TransactionT ★/t ★/t))))
+
+(define account-manager
+  (actor τc
+    (lambda ([e : (Event τc)]
+             [b : Int])
+      (let ([new-balance
+             (for/fold [balance b]
+                       [txn (project [(transaction discard (bind v Int)) (patch-added e)] v)]
+               (+ balance txn))])
+        (transition new-balance
+                    (list (patch (make-assertion-set (account new-balance))
+                                 (make-assertion-set (account ★)))))))
+    0
+    (make-assertion-set (account 0)
+                        (observe (transaction ★ ★)))))
+
+(define (make-transaction [id : Int] [amount : Int] → (Actor Transaction))
+  (actor Transaction
+   (lambda ([e : (Event (U))]
+            [s : ★/t])
+     idle)
+   #f
+   (make-assertion-set (transaction id amount))))
+
+(define client
+  (actor τc
+    (lambda ([e : (Event τc)]
+             [s : ★/t])
+      (quit (list (make-transaction 0 100)
+                  (make-transaction 1 -70))))
+    #f
+    (make-assertion-set (observe (account ★)))))
+
+(define observer
+  (actor τc
+    (lambda ([e : (Event τc)]
+             [s : ★/t])
+      (project [(account (bind value Int)) (patch-added e)]
+        (displayln value))
+      idle)
+    #f
+    (make-assertion-set (observe (account ★)))))
+
+(dataspace τc
+  (list
+   account-manager
+   observer
+   client))

racket/typed/examples/core/book-club.rkt

@@ -0,0 +1,223 @@
+#lang typed/syndicate/core
+
+(define-constructor (in-stock title quantity)
+  #:type-constructor InStock)
+
+(define-constructor (order title client id)
+  #:type-constructor Order)
+
+(define-constructor (club-member name)
+  #:type-constructor ClubMember)
+
+(define-constructor (book-interest title name answer)
+  #:type-constructor BookInterest)
+
+(define-constructor (book-of-the-month title)
+  #:type-constructor BookOfTheMonth)
+
+(define-type-alias τc
+  (U (ClubMember String)
+     (Observe (ClubMember ★/t))
+     (BookInterest String String Bool)
+     (Observe (BookInterest String ★/t ★/t))
+     (Observe (Observe (BookInterest ★/t ★/t ★/t)))
+     (InStock String Int)
+     (Observe (InStock String ★/t))
+     (Observe (Observe (InStock ★/t ★/t)))
+     (BookOfTheMonth String)
+     (Observe (BookOfTheMonth ★/t))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Leader
+
+(define-type-alias LeaderState
+  (Tuple String (List String) (Set String) String (Set String) (Set String)))
+
+(define (leader-state-current-title [ls : LeaderState] -> String)
+  (select 0 ls))
+
+(define (leader-state-interests [ls : LeaderState] -> (List String))
+  (select 1 ls))
+
+(define (leader-state-members [ls : LeaderState] -> (Set String))
+  (select 2 ls))
+
+(define (leader-state-conv [ls : LeaderState] -> String)
+  (select 3 ls))
+
+(define (leader-state-yays [ls : LeaderState] -> (Set String))
+  (select 4 ls))
+
+(define (leader-state-nays [ls : LeaderState] -> (Set String))
+  (select 5 ls))
+
+(define (leader-state [current-title : String]
+                      [interests : (List String)]
+                      [members : (Set String)]
+                      [conv : String]
+                      [yays : (Set String)]
+                      [nays : (Set String)]
+                      -> LeaderState)
+  (tuple current-title interests members conv yays nays))
+
+(define (update-members [members : (Set String)]
+                        [added : (AssertionSet τc)]
+                        [retracted : (AssertionSet τc)]
+                        -> (Set String))
+  (let ([as (project [(club-member (bind name String)) added] name)]
+        [rs (project [(club-member (bind name String)) retracted] name)])
+    (set-subtract (set-union members (list->set as)) (list->set rs))))
+
+(define (next-book [books : (List String)]
+                   [members : (Set String)]
+                   -> (Instruction LeaderState τc τc))
+  (if (empty? books)
+      (begin (displayln "leader fails to find a suitable book")
+             (quit))
+      (let ([next (first books)]
+            [remaining (rest books)])
+        (transition (leader-state next remaining members "quote" (set) (set))
+                    (list (patch-seq (unsub (in-stock ★ ★))
+                                     (unsub (book-interest ★ ★ ★))
+                                     (sub (in-stock next ★))))))))
+
+(define (leader-learns [quantity : Int]
+                       [title : String]
+                       -> (Tuple))
+  (displayln "leader learns that there are")
+  (displayln quantity)
+  (displayln "copies of")
+  (displayln title)
+  (tuple))
+
+(define (respond-to-quotes [added : (AssertionSet τc)]
+                           [title : String]
+                           [interests : (List String)]
+                           [members : (Set String)]
+                           [changed? Bool]
+                           -> (Instruction LeaderState τc τc))
+  (let ([answers (project [(in-stock title (bind n Int)) added] n)])
+    (if (empty? answers)
+        (if changed?
+            (transition (leader-state title interests members "quote" (set) (set)) (list))
+            idle)
+        (let ([quantity (first answers)])
+          (leader-learns quantity title)
+          (if (<= quantity (set-count members))
+              (begin (displayln "there aren't enough copies to go around")
+                     (next-book interests members))
+              (transition (leader-state title interests members "poll" (set) (set))
+                          (list (sub (book-interest title ★ ★)))))))))
+
+(define (respond-to-interests [added : (AssertionSet τc)]
+                              [title : String]
+                              [books : (List String)]
+                              [members : (Set String)]
+                              [yays : (Set String)]
+                              [nays : (Set String)]
+                              -> (Instruction LeaderState τc τc))
+  (let ([yups (set-union yays (list->set (project [(book-interest title (bind name String) #t) added]
+                                                  name)))]
+        [nups (set-union nays (list->set (project [(book-interest title (bind name String) #f) added]
+                                                  name)))])
+    (if (>= (set-count yups) (/ (set-count members) 2))
+        (begin (displayln "leader finds enough affirmation for") (displayln title)
+               (transition (leader-state title books members "complete" yays nays)
+                           (list (patch-seq (assert (book-of-the-month title))
+                                            (unsub (book-interest ★ ★ ★))))))
+        (if (> (set-count nups) (/ (set-count members) 2))
+            (begin (displayln "leader finds enough negative nancys for") (displayln title)
+                   (next-book books members))
+            (transition (leader-state title books members "poll" yups nups) (list))))))
+
+(define (leader-behavior [e : (Event τc)]
+                         [s : LeaderState]
+                         -> (Instruction LeaderState τc τc))
+  (let* ([added (patch-added e)]
+         [retracted (patch-removed e)]
+         [title (leader-state-current-title s)]
+         [books (leader-state-interests s)]
+         [members (leader-state-members s)]
+         [state (leader-state-conv s)]
+         [yays (leader-state-yays s)]
+         [nays (leader-state-nays s)]
+         [new-members (update-members members added retracted)]
+         [changed? (not (equal? new-members members))])
+    (if changed?
+        (begin (displayln "leader knows about") (displayln new-members) #f)
+        #f)
+    (if (equal? state "quote")
+        (respond-to-quotes added title books new-members changed?)
+        (if (equal? state "poll")
+            (respond-to-interests added title books new-members yays nays)
+            idle))))
+
+(define (make-leader [interests : (List String)] -> (Actor τc))
+  (let ([first-book (first interests)]
+        [books (rest interests)])
+    (actor τc
+      leader-behavior
+      (leader-state first-book books (set) "quote" (set) (set))
+      (make-assertion-set (observe (in-stock first-book ★))
+                          (observe (club-member ★))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Seller
+
+(define-type-alias Inventory (List (Tuple String Int)))
+
+(define (lookup/default [title : String]
+                        [inv : Inventory]
+                        [default : Int]
+                        -> Int)
+  (for/fold [answer default]
+            [item inv]
+    (if (equal? title (select 0 item))
+        (select 1 item)
+        answer)))
+
+(define (answer-inquiries [e : (AssertionSet τc)]
+                          [inventory : Inventory]
+                          -> (Patch (InStock String Int) (U)))
+  (patch-seq*
+   (project [(observe (in-stock (bind title String) discard)) e]
+     (assert (in-stock title (lookup/default title inventory 0))))))
+
+(define (make-book-seller [initial-inventory : Inventory] -> (Actor τc))
+  (actor τc
+    (lambda ([e : (Event τc)]
+             [inv : Inventory])
+      (transition inv (list (answer-inquiries (patch-added e) inv))))
+    initial-inventory
+    (make-assertion-set (observe (observe (in-stock ★ ★))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Members
+
+(define (make-club-member [name : String] [preferences : (List String)] -> (Actor τc))
+  (actor τc
+   (lambda ([e : (Event τc)]
+            [s : ★/t])
+     (let ([answers
+            (project [(observe (book-interest (bind title String) discard discard)) (patch-added e)]
+              (patch (make-assertion-set (book-interest title name (member? title preferences)))
+                     (make-assertion-set)))])
+       (transition s answers)))
+   #f
+   (make-assertion-set (club-member name)
+                       (observe (observe (book-interest ★ ★ ★))))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Main
+
+(dataspace τc
+  (list
+   (make-book-seller (list (tuple "The Wind in the Willows" 5)
+                          (tuple "Catch 22" 2)
+                          (tuple "Candide" 3)))
+   (make-leader (list "The Wind in the Willows"
+                      "Catch 22"
+                      "Candide"
+                      "Encyclopaedia Brittannica"))
+   (make-club-member "tony" (list "Candide"))
+   (make-club-member "sam" (list "Encyclopaedia Brittannica" "Candide"))))

racket/typed/examples/core/box-and-client.rkt

@@ -0,0 +1,45 @@
+#lang typed/syndicate/core
+
+(define-constructor (set-box new-value)
+  #:type-constructor SetBoxT
+  #:with SetBox (SetBoxT Int))
+
+(define-constructor (box-state value)
+  #:type-constructor BoxStateT
+  #:with BoxState (BoxStateT Int))
+
+(define-type-alias τ-c
+  (U BoxState
+     (Observe (BoxStateT ★/t))
+     SetBox
+     (Observe (SetBoxT ★/t))))
+
+(dataspace τ-c
+  (list
+  (actor τ-c
+         (lambda ([e : (Event τ-c)]
+                  [current-value : Int])
+           (let ([sets (project [(set-box (bind v Int)) (patch-added e)] v)])
+             (if (empty? sets)
+                 idle
+                 (let ([new-value (first sets)])
+                   (displayln new-value)
+                   (transition new-value (list (patch (make-assertion-set (box-state new-value))
+                                                      (make-assertion-set (box-state current-value)))))))))
+         0
+         (make-assertion-set (box-state 0)
+                             (observe (set-box ★))))
+
+  (actor τ-c
+         (lambda ([e : (Event τ-c)]
+                  [s : (Tuple)])
+           (let ([updates (project [(box-state (bind v Int)) (patch-added e)] v)])
+             (if (empty? updates)
+                 idle
+                 (let ([new-value (first updates)])
+                   (if (> new-value 9)
+                       (quit)
+                       (transition s (list (patch (make-assertion-set (set-box (+ new-value 1)))
+                                                  (make-assertion-set (set-box ★))))))))))
+         (tuple)
+         (make-assertion-set (observe (box-state ★))))))

racket/typed/examples/roles/bank-account.rkt

@@ -0,0 +1,57 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; 0
+;; 70
+;; #f
+
+(define-constructor (account balance)
+  #:type-constructor AccountT
+  #:with Account (AccountT Int)
+  #:with AccountRequest (AccountT ★/t))
+
+(define-constructor (deposit amount)
+  #:type-constructor DepositT
+  #:with Deposit (DepositT Int)
+  #:with DepositRequest (DepositT ★/t))
+
+(define-type-alias ds-type
+  (U Account
+     (Observe AccountRequest)
+     (Observe (Observe AccountRequest))
+     Deposit
+     (Observe DepositRequest)
+     (Observe (Observe DepositRequest))))
+
+(define-type-alias account-manager-role
+  (Role (account-manager)
+        (Shares Account)
+        (Reacts (Know (Deposit Int)))))
+
+(define-type-alias client-role
+  (Role (client)
+        (Reacts (Know Account))))
+
+(run-ground-dataspace ds-type
+
+  (spawn ds-type
+    (print-role
+    (start-facet account-manager
+      (field [balance Int 0])
+      (assert (account (ref balance)))
+      (on (asserted (deposit (bind amount Int)))
+          (set! balance (+ (ref balance) amount))))))
+
+  (spawn ds-type
+    (print-role
+    (start-facet observer
+      (on (asserted (account (bind amount Int)))
+          (displayln amount)))))
+
+  (spawn ds-type
+    (print-role
+    (start-facet buyer
+      (on (asserted (observe (deposit discard)))
+          (start-facet deposits
+            (assert (deposit 100))
+            (assert (deposit -30))))))))

racket/typed/examples/roles/book-club.rkt

@@ -0,0 +1,174 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; leader learns that there are 5 copies of The Wind in the Willows
+;; tony responds to suggested book The Wind in the Willows: #f
+;; sam responds to suggested book The Wind in the Willows: #f
+;; leader finds enough negative nancys for The Wind in the Willows
+;; leader learns that there are 2 copies of Catch 22
+;; leader learns that there are 3 copies of Candide
+;; tony responds to suggested book Candide: #t
+;; sam responds to suggested book Candide: #t
+;; leader finds enough affirmation for Candide
+
+(define-constructor (price v)
+  #:type-constructor PriceT
+  #:with Price (PriceT Int))
+
+(define-constructor (book-quote title quantity)
+  #:type-constructor BookQuoteT
+  #:with BookQuote (BookQuoteT String Int))
+
+(define-constructor (club-member name)
+  #:type-constructor ClubMemberT
+  #:with ClubMember (ClubMemberT String))
+
+(define-constructor (book-interest title client id)
+  #:type-constructor BookInterestT
+  #:with BookInterest (BookInterestT String String Bool))
+
+(define-constructor (book-of-the-month title)
+  #:type-constructor BookOfTheMonthT
+  #:with BookOfTheMonth (BookOfTheMonthT String))
+
+(define-type-alias τc
+  (U BookQuote
+     (Observe (BookQuoteT String ★/t))
+     (Observe (Observe (BookQuoteT ★/t ★/t)))
+     ClubMember
+     (Observe (ClubMemberT ★/t))
+     BookInterest
+     (Observe (BookInterestT String ★/t ★/t))
+     (Observe (Observe (BookInterestT ★/t ★/t ★/t)))
+     BookOfTheMonth
+     (Observe (BookOfTheMonthT ★/t))))
+
+(define-type-alias Inventory (List (Tuple String Int)))
+
+(define (lookup [title : String]
+                [inv : Inventory] -> Int)
+  (for/fold [stock 0]
+            [item inv]
+    (if (equal? title (select 0 item))
+        (select 1 item)
+        stock)))
+
+(define-type-alias seller-role
+  (Role (seller)
+   (Reacts (Know (Observe (BookQuoteT String ★/t)))
+           (Role (_)
+                 ;; nb no mention of retracting this assertion
+                 (Shares (BookQuoteT String Int))))))
+
+(define (spawn-seller [inventory : Inventory])
+  (spawn τc
+    (start-facet seller
+      (field [books Inventory inventory])
+
+      ;; Give quotes to interested parties.
+      (during (observe (book-quote (bind title String) discard))
+        ;; TODO - lookup
+        (assert (book-quote title (lookup title (ref books))))))))
+
+(define-type-alias leader-role
+  (Role (leader)
+        (Reacts (Know (BookQuoteT String Int))
+                (Role (poll)
+                      (Reacts (Know (BookInterestT String String Bool))
+                              ;; this is actually implemented indirectly through dataflow
+                              (U (Stop leader
+                                       (Role (_)
+                                             (Shares (BookOfTheMonthT String))))
+                                 (Stop poll)))))))
+
+(define-type-alias leader-actual
+  (Role (get-quotes31)
+        (Reacts (Know (BookQuoteT String (Bind Int)))
+                (Stop get-quotes)
+                (Role (poll-members36)
+                      (Reacts OnDataflow
+                              (Stop poll-members
+                                    (Stop get-quotes))
+                              (Stop get-quotes
+                                    (Role (announce39)
+                                          (Shares (BookOfTheMonthT String)))))
+                      (Reacts (¬Know (BookInterestT String (Bind String) Bool)))
+                      (Reacts (Know (BookInterestT String (Bind String) Bool)))
+                      (Reacts (¬Know (BookInterestT String (Bind String) Bool)))
+                      (Reacts (Know (BookInterestT String (Bind String) Bool)))))
+        (Reacts (¬Know (ClubMemberT (Bind String))))
+        (Reacts (Know (ClubMemberT (Bind String))))))
+
+(define (spawn-leader [titles : (List String)])
+  (spawn τc
+   (print-role
+   (start-facet get-quotes
+     (field [book-list (List String) (rest titles)]
+            [title String (first titles)])
+     (define (next-book)
+       (cond
+         [(empty? (ref book-list))
+          (printf "leader fails to find a suitable book\n")
+          (stop get-quotes)]
+         [#t
+          (set! title (first (ref book-list)))
+          (set! book-list (rest (ref book-list)))]))
+
+     ;; keep track of book club members
+     (define/query-set members (club-member (bind name String)) name
+         #;#:on-add #;(printf "leader acknowledges member ~a\n" name))
+
+     (on (asserted (book-quote (ref title) (bind quantity Int)))
+         (printf "leader learns that there are ~a copies of ~a\n" quantity (ref title))
+         (cond
+           [(< quantity (+ 1 (set-count (ref members))))
+            ;; not enough in stock for each member
+            (next-book)]
+           [#t
+            ;; find out if at least half of the members want to read the book
+            (start-facet poll-members
+             (define/query-set yays (book-interest (ref title) (bind name String) #t) name)
+             (define/query-set nays (book-interest (ref title) (bind name String) #f) name)
+             (begin/dataflow
+               ;; count the leader as a 'yay'
+               (when (>= (set-count (ref yays))
+                         (/ (set-count (ref members)) 2))
+                 (printf "leader finds enough affirmation for ~a\n" (ref title))
+                 (stop get-quotes
+                       (start-facet announce
+                         (assert (book-of-the-month (ref title))))))
+               (when (> (set-count (ref nays))
+                        (/ (set-count (ref members)) 2))
+                 (printf "leader finds enough negative nancys for ~a\n" (ref title))
+                 (stop poll-members (next-book)))))]))))))
+
+(define-type-alias member-role
+  (Role (member)
+        (Shares (ClubMemberT String))
+        ;; should this be the type of the pattern? or lowered to concrete types?
+        (Reacts (Know (Observe (BookInterestT String ★/t ★/t)))
+                (Role (_)
+                      (Shares (BookInterestT String String Bool))))))
+                       
+(define (spawn-club-member [name : String]
+                           [titles : (List String)])
+  (spawn τc
+   (start-facet member
+     ;; assert our presence
+     (assert (club-member name))
+     ;; respond to polls
+     (during (observe (book-interest (bind title String) discard discard))
+       (define answer (member? title titles))
+       (printf "~a responds to suggested book ~a: ~a\n" name title answer)
+       (assert (book-interest title name answer))))))
+
+(run-ground-dataspace τc
+  (spawn-seller (list (tuple "The Wind in the Willows" 5)
+                      (tuple "Catch 22" 2)
+                      (tuple "Candide" 3)))
+  (spawn-leader (list "The Wind in the Willows"
+                      "Catch 22"
+                      "Candide"
+                      "Encyclopaedia Brittannica"))
+  (spawn-club-member "tony" (list "Candide"))
+  (spawn-club-member "sam" (list "Encyclopaedia Brittannica" "Candide")))

racket/typed/examples/roles/cell.rkt

@@ -0,0 +1,71 @@
+#lang typed/syndicate/roles
+
+;; adapted from section 8.3 of Tony's dissertation
+
+(define-constructor* (cell : CellT id value))
+(define-constructor* (create-cell : CreateCellT id value))
+(define-constructor* (update-cell : UpdateCellT id value))
+(define-constructor* (delete-cell : DeleteCellT id))
+
+(define-type-alias ID Int)
+(define-type-alias Value String)
+
+(define-type-alias Cell
+  (Role (cell)
+        (Shares (CellT ID Value))
+        (Reacts (Message (UpdateCellT ID ★/t))
+                )
+        (Reacts (Message (DeleteCellT ID))
+                (Stop cell))))
+
+(define-type-alias CellFactory
+  (Role (cell-factory)
+        (Reacts (Message (CreateCellT ID Value))
+                ;; want to say that what it spawns is a Cell
+                (Spawn ★/t))))
+
+(define-type-alias Reader
+  (Role (reader)
+        (Shares (Observe (Cell ID ★/t)))))
+
+(define-type-alias Writer
+  (Role (writer)
+        ;; sends update and delete messages
+        ))
+
+(define-type-alias ds-type
+  (U (CellT ID Value)
+     (Observe (CellT ID ★/t))
+     (Message (CreateCellT ID Value))
+     (Message (UpdateCellT ID Value))
+     (Message (DeleteCellT ID))
+     (Observe (CreateCellT ★/t ★/t))
+     (Observe (UpdateCellT ID ★/t))
+     (Observe (DeleteCellT ID))))
+
+(define (spawn-cell! [initial-value : Value])
+  (define id 1234)
+  (send! (create-cell id initial-value))
+  id)
+
+(define (spawn-cell-factory)
+  (spawn ds-type
+   (start-facet cell-factory
+     (on (message (create-cell (bind id ID) (bind init Value)))
+         (spawn ds-type
+           (start-facet the-cell
+             (field [value Value init])
+             (assert (cell id (ref value)))
+             (on (message (update-cell id (bind new-value Value)))
+                 (set! value new-value))
+             (on (message (delete-cell id))
+                 (stop the-cell))))))))
+
+
+(define (spawn-cell-monitor [id : ID])
+  (spawn ds-type
+    (start-facet monitor
+      (on (asserted (cell id (bind value Value)))
+          (printf "Cell ~a updated to: ~a\n" id value))
+      (on (retracted (cell id discard))
+          (printf "Cell ~a deleted\n" id)))))

racket/typed/examples/roles/chat-tcp2.rkt

@@ -0,0 +1,42 @@
+#lang typed/syndicate/roles
+
+(require "../../drivers/tcp.rkt")
+
+;; message
+(define-constructor (speak who what)
+  #:type-constructor SpeakT
+  #:with Speak (SpeakT Symbol String))
+
+(define-constructor (present who)
+  #:type-constructor PresentT
+  #:with Present (PresentT Symbol))
+
+(define-type-alias chat-comm
+  (U Present
+     (Message Speak)
+     (Observe (PresentT ★/t))
+     (Observe (SpeakT Symbol ★/t))))
+
+(define-type-alias chat-ds
+  (U chat-comm
+     Tcp2Driver))
+
+(run-ground-dataspace chat-ds
+  (activate!)
+
+  (spawn chat-ds
+   (start-facet chat-server
+     ;; TODO - should be during/spawn
+     (during (tcp-connection (bind id Symbol) (tcp-listener 5999))
+             (assert (tcp-accepted id))
+             (let ([me (gensym 'user)])
+               (assert (present me))
+               (on (message (tcp-in-line id (bind bs ByteString)))
+                   (send! (speak me (bytes->string/utf-8 bs))))
+               (during (present (bind user Symbol))
+                 (on start
+                     (send! (tcp-out id (string->bytes/utf-8 (~a user " arrived\n")))))
+                 (on stop
+                     (send! (tcp-out id (string->bytes/utf-8 (~a user " left\n")))))
+                 (on (message (speak user (bind text String)))
+                     (send! (tcp-out id (string->bytes/utf-8 (~a user " says '" text "'\n")))))))))))

racket/typed/examples/roles/file-system.rkt

@@ -0,0 +1,34 @@
+#lang typed/syndicate/roles
+
+(define-constructor (file name content)
+  #:type-constructor FileT
+  #:with File (FileT String String))
+
+(define-type-alias FileDemand
+  (Observe (FileT String ★/t)))
+
+(define-constructor (save name content)
+  #:type-constructor SaveT
+  #:with Save (SaveT String String))
+
+(define-constructor (delete name)
+  #:type-constructor DeleteT
+  #:with Delete (DeleteT String))
+
+;; unique role
+(define-type-alias Server
+  (Role (server)
+        (Reacts (Know FileDemand)
+                (Role (_)
+                      (Shares File)))
+        (Reacts (Message Save))
+        (Reacts (Message Delete))))
+
+(define-type-alias Reader
+  (Role (reader)
+        (Shares FileDemand)))
+
+(define-type-alias Writer
+  (Role (writer)
+        (Sends Save)
+        (Sends Delete)))

racket/typed/examples/roles/ping-pong.rkt

@@ -0,0 +1,20 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; pong: 8339
+
+(define-type-alias ds-type
+  (U (Message (Tuple String Int))
+     (Observe (Tuple String ★/t))))
+
+(run-ground-dataspace ds-type
+  (spawn ds-type
+    (start-facet echo
+      (on (message (tuple "ping" (bind x Int)))
+          (send! (tuple "pong" x)))))
+  (spawn ds-type
+    (start-facet serve
+      (on start
+          (send! (tuple "ping" 8339)))
+      (on (message (tuple "pong" (bind x Int)))
+          (printf "pong: ~v\n" x)))))

racket/typed/examples/roles/provides.rkt

@@ -0,0 +1,8 @@
+#lang typed/syndicate/roles
+
+(provide a-fun)
+
+(define (a-fun [x : Int] -> Int)
+  (+ x 1))
+
+#;(a-fun 5)

racket/typed/examples/roles/require-struct/client.rkt

@@ -0,0 +1,13 @@
+#lang typed/syndicate/roles
+
+(require-struct msg #:as Msg
+                #:from "driver.rkt")
+
+(define m (msg 1 "hi"))
+
+(match m
+  [(msg (bind x Int) discard)
+   (displayln x)])
+
+;; error: msg/checked: arity mismatch
+#;(msg 1 2 3)

racket/typed/examples/roles/require-struct/driver.rkt

@@ -0,0 +1,5 @@
+#lang racket
+
+(provide (struct-out msg))
+
+(struct msg (in out) #:transparent)

racket/typed/examples/roles/require:typed/client.rkt

@@ -0,0 +1,5 @@
+#lang typed/syndicate/roles
+
+(require/typed "lib.rkt" [x : Int])
+
+(displayln (+ x 1))

racket/typed/examples/roles/require:typed/lib.rkt

@@ -0,0 +1,5 @@
+#lang racket
+
+(provide x)
+
+(define x 42)

racket/typed/examples/roles/requires.rkt

@@ -0,0 +1,5 @@
+#lang typed/syndicate/roles
+
+(require "provides.rkt")
+
+(a-fun 5)

racket/typed/examples/roles/simple-dataflow.rkt

@@ -0,0 +1,21 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; f: 0
+;; f: 18
+
+(define-type-alias ds-type
+  (U (Tuple String Int)
+     (Observe ★/t)))
+
+(run-ground-dataspace ds-type
+  (spawn ds-type
+    (start-facet server
+      (field [f Int 0])
+      (begin/dataflow
+        (printf "f = ~v\n" (ref f)))
+      (on (asserted (tuple "key" (bind v Int)))
+          (set! f v))))
+  (spawn ds-type
+    (start-facet client
+      (assert (tuple "key" 18)))))

racket/typed/examples/roles/simple-dataspace.rkt

@@ -0,0 +1,6 @@
+#lang typed/syndicate/roles
+
+(run-ground-dataspace Int
+  (spawn Int
+    (start-facet _
+      (assert 42))))

racket/typed/examples/roles/simple-during.rkt

@@ -0,0 +1,29 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; +GO
+;; +ready
+;; -GO
+;; -ready
+
+(define-type-alias ds-type
+  (U (Tuple String) (Observe (Tuple ★/t))))
+
+(run-ground-dataspace ds-type
+  (spawn ds-type
+    (start-facet _
+      (during (tuple "GO")
+        (assert (tuple "ready")))))
+  (spawn ds-type
+    (start-facet flag
+      ;; type error when this was mistakenly just "GO"
+      (assert (tuple "GO"))
+      (on (asserted (tuple "ready"))
+          (stop flag))))
+  (spawn ds-type
+    (start-facet obs
+      (during (tuple (bind s String))
+        (on start
+            (printf "+~a\n" s))
+        (on stop
+            (printf "-~a\n" s))))))

racket/typed/examples/roles/simple-query-set.rkt

@@ -0,0 +1,22 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; size: 0
+;; size: 2
+
+(define-type-alias ds-type
+  (U (Tuple String Int)
+     (Observe ★/t)))
+
+(run-ground-dataspace ds-type
+  (spawn ds-type
+    (start-facet querier
+      (define/query-set key (tuple "key" (bind v Int)) v)
+      (assert (tuple "size" (set-count (ref key))))))
+  (spawn ds-type
+    (start-facet client
+      (assert (tuple "key" 18))
+      (assert (tuple "key" 88))
+      (during (tuple "size" (bind v Int))
+        (on start
+            (printf "size: ~v\n" v))))))

racket/typed/examples/roles/simple-query-value.rkt

@@ -0,0 +1,21 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; query: 0
+;; query: 19
+
+(define-type-alias ds-type
+  (U (Tuple String Int)
+     (Observe ★/t)))
+
+(run-ground-dataspace ds-type
+  (spawn ds-type
+    (start-facet querier
+      (define/query-value key 0 (tuple "key" (bind v Int)) (+ v 1))
+      (assert (tuple "query" (ref key)))))
+  (spawn ds-type
+    (start-facet client
+      (assert (tuple "key" 18))
+      (during (tuple "query" (bind v Int))
+        (on start
+            (printf "query: ~v\n" v))))))

racket/typed/examples/roles/simple-stop-facet.rkt

@@ -0,0 +1,38 @@
+#lang typed/syndicate/roles
+
+;; Expected Output:
+;; +42
+;; +18
+;; +9
+;; +88
+;; -18
+;; -9
+
+(define-type-alias ds-type
+  (U (Tuple Int)
+     (Observe (Tuple ★/t))))
+
+(run-ground-dataspace ds-type
+  (spawn ds-type
+   (print-role
+   (start-facet doomed
+     (assert (tuple 18))
+     (on (asserted (tuple 42))
+         (stop doomed
+                (start-facet the-afterlife
+                  (assert (tuple 88))))))))
+
+  (spawn ds-type
+    (start-facet obs
+      (assert (tuple 42))
+      (on (asserted (tuple (bind x Int)))
+          (printf "+~v\n" x))
+      (on (retracted (tuple (bind x Int)))
+          (printf "-~v\n" x))))
+
+  ;; null-ary stop
+  (spawn ds-type
+    (start-facet meep
+      (assert (tuple 9))
+      (on (asserted (tuple 88))
+          (stop meep)))))

racket/typed/examples/roles/two-buyer-protocol.rkt

@@ -0,0 +1,148 @@
+#lang typed/syndicate/roles
+
+;; Expected Output
+;; Completed Order:
+;; Catch 22
+;; 10001483
+;; March 9th
+
+(define-constructor (price v)
+  #:type-constructor PriceT
+  #:with Price (PriceT Int))
+
+(define-constructor (out-of-stock)
+  #:type-constructor OutOfStockT
+  #:with OutOfStock (OutOfStockT))
+
+(define-type-alias QuoteAnswer
+  (U Price OutOfStock))
+
+(define-constructor (quote title answer)
+  #:type-constructor QuoteT
+  #:with Quote (QuoteT String QuoteAnswer)
+  #:with QuoteRequest (Observe (QuoteT String ★/t))
+  #:with QuoteInterest (Observe (QuoteT ★/t ★/t)))
+
+(define-constructor (split-proposal title price contribution accepted)
+  #:type-constructor SplitProposalT
+  #:with SplitProposal (SplitProposalT String Int Int Bool)
+  #:with SplitRequest (Observe (SplitProposalT String Int Int ★/t))
+  #:with SplitInterest (Observe (SplitProposalT ★/t ★/t ★/t ★/t)))
+
+(define-constructor (order-id id)
+  #:type-constructor OrderIdT
+  #:with OrderId (OrderIdT Int))
+
+(define-constructor (delivery-date date)
+  #:type-constructor DeliveryDateT
+  #:with DeliveryDate (DeliveryDateT String))
+
+(define-type-alias (Maybe t)
+  (U t Bool))
+
+(define-constructor (order title price id delivery-date)
+  #:type-constructor OrderT
+  #:with Order (OrderT String Int (Maybe OrderId) (Maybe DeliveryDate))
+  #:with OrderRequest (Observe (OrderT String Int ★/t ★/t))
+  #:with OrderInterest (Observe (OrderT ★/t ★/t ★/t ★/t)))
+
+(define-type-alias ds-type
+  (U ;; quotes
+   Quote
+   QuoteRequest
+   (Observe QuoteInterest)
+   ;; splits
+   SplitProposal
+   SplitRequest
+   (Observe SplitInterest)
+   ;; orders
+   Order
+   OrderRequest
+   (Observe OrderInterest)))
+
+(define-type-alias seller-role
+  (Role (seller)
+    (Reacts (Know (Observe (QuoteT String ★/t)))
+            (Role (_)
+              (Shares (QuoteT String Int))))))
+
+(run-ground-dataspace ds-type
+
+;; seller
+(spawn ds-type
+  (start-facet _
+    (field [book (Tuple String Int) (tuple "Catch 22" 22)]
+           [next-order-id Int 10001483])
+    (on (asserted (observe (quote (bind title String) discard)))
+        (start-facet x
+          (on (retracted (observe (quote title discard)))
+              (stop x))
+          (match title
+            ["Catch 22"
+             (assert (quote title (price 22)))]
+            [discard
+             (assert (quote title (out-of-stock)))])))
+    (on (asserted (observe (order (bind title String) (bind offer Int) discard discard)))
+        (start-facet x
+          (on (retracted (observe (order title offer discard discard)))
+              (stop x))
+          (let ([asking-price 22])
+            (if (and (equal? title "Catch 22") (>= offer asking-price))
+                (let ([id (ref next-order-id)])
+                  (set! next-order-id (+ 1 id))
+                  (assert (order title offer (order-id id) (delivery-date "March 9th"))))
+                (assert (order title offer #f #f))))))))
+
+;; buyer A
+(spawn ds-type
+  (start-facet buyer
+    (field [title String "Catch 22"]
+           [budget Int 1000])
+    (on (asserted (quote (ref title) (bind answer QuoteAnswer)))
+        (match answer
+          [(out-of-stock)
+           (stop buyer)]
+          [(price (bind amount Int))
+           (start-facet negotiation
+             (field [contribution Int (/ amount 2)])
+             (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool)))
+                 (if accept?
+                     (stop buyer)
+                     (if (> (ref contribution) (- amount 5))
+                         (stop negotiation (displayln "negotiation failed"))
+                         (set! contribution
+                               (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))]))))
+
+;; buyer B
+(spawn ds-type
+  (start-facet buyer-b
+    (field [funds Int 5])
+    (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard)))
+        (let ([my-contribution (- price their-contribution)])
+          (cond
+            [(> my-contribution (ref funds))
+             (start-facet decline
+               (assert (split-proposal title price their-contribution #f))
+               (on (retracted (observe (split-proposal title price their-contribution discard)))
+                   (stop decline)))]
+            [#t
+             (start-facet accept
+               (assert (split-proposal title price their-contribution #t))
+               (on (retracted (observe (split-proposal title price their-contribution discard)))
+                   (stop accept))
+               (on start
+                   (spawn ds-type
+                     (start-facet purchase
+                       (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate))))
+                           (match (tuple order-id? delivery-date?)
+                             [(tuple (order-id (bind id Int)) (delivery-date (bind date String)))
+                              ;; complete!
+                              (begin (displayln "Completed Order:")
+                                     (displayln title)
+                                     (displayln id)
+                                     (displayln date)
+                                     (stop purchase))]
+                             [discard
+                              (begin (displayln "Order Rejected")
+                                     (stop purchase))]))))))])))))
+)

racket/typed/examples/two-buyer-protocol.rkt

@@ -0,0 +1,147 @@
+#lang typed/syndicate
+
+;; Expected Output
+;; Completed Order:
+;; Catch 22
+;; 10001483
+;; March 9th
+
+(define-constructor (price v)
+  #:type-constructor PriceT
+  #:with Price (PriceT Int))
+
+(define-constructor (out-of-stock)
+  #:type-constructor OutOfStockT
+  #:with OutOfStock (OutOfStockT))
+
+(define-type-alias QuoteAnswer
+  (U Price OutOfStock))
+
+(define-constructor (quote title answer)
+  #:type-constructor QuoteT
+  #:with Quote (QuoteT String QuoteAnswer)
+  #:with QuoteRequest (Observe (QuoteT String ★))
+  #:with QuoteInterest (Observe (QuoteT ★ ★)))
+
+(define-constructor (split-proposal title price contribution accepted)
+  #:type-constructor SplitProposalT
+  #:with SplitProposal (SplitProposalT String Int Int Bool)
+  #:with SplitRequest (Observe (SplitProposalT String Int Int ★))
+  #:with SplitInterest (Observe (SplitProposalT ★ ★ ★ ★)))
+
+(define-constructor (order-id id)
+  #:type-constructor OrderIdT
+  #:with OrderId (OrderIdT Int))
+
+(define-constructor (delivery-date date)
+  #:type-constructor DeliveryDateT
+  #:with DeliveryDate (DeliveryDateT String))
+
+(define-type-alias (Maybe t)
+  (U t Bool))
+
+(define-constructor (order title price id delivery-date)
+  #:type-constructor OrderT
+  #:with Order (OrderT String Int (Maybe OrderId) (Maybe DeliveryDate))
+  #:with OrderRequest (Observe (OrderT String Int ★ ★))
+  #:with OrderInterest (Observe (OrderT ★ ★ ★ ★)))
+
+(define-type-alias ds-type
+  (U ;; quotes
+   Quote
+   QuoteRequest
+   (Observe QuoteInterest)
+   ;; splits
+   SplitProposal
+   SplitRequest
+   (Observe SplitInterest)
+   ;; orders
+   Order
+   OrderRequest
+   (Observe OrderInterest)))
+
+(dataspace ds-type
+
+;; seller
+(spawn ds-type
+       (facet _
+              (fields [book (Tuple String Int) (tuple "Catch 22" 22)]
+                      [next-order-id Int 10001483])
+              (on (asserted (observe (quote (bind title String) discard)))
+                  (facet x
+                         (fields)
+                         (on (retracted (observe (quote title discard)))
+                             (stop x (begin)))
+                         (match title
+                           ["Catch 22"
+                            (assert (quote title (price 22)))]
+                           [discard
+                            (assert (quote title (out-of-stock)))])))
+              (on (asserted (observe (order (bind title String) (bind offer Int) discard discard)))
+                  (facet x
+                         (fields)
+                         (on (retracted (observe (order title offer discard discard)))
+                             (stop x (begin)))
+                         (let [asking-price 22]
+                           (if (and (equal? title "Catch 22") (>= offer asking-price))
+                               (let [id (ref next-order-id)]
+                                 (begin (set! next-order-id (+ 1 id))
+                                        (assert (order title offer (order-id id) (delivery-date "March 9th")))))
+                               (assert (order title offer #f #f))))))))
+
+;; buyer A
+(spawn ds-type
+       (facet buyer
+              (fields [title String "Catch 22"]
+                      [budget Int 1000])
+              (on (asserted (quote (ref title) (bind answer QuoteAnswer)))
+                  (match answer
+                    [(out-of-stock)
+                     (stop buyer (begin))]
+                    [(price (bind amount Int))
+                     (facet negotiation
+                            (fields [contribution Int (/ amount 2)])
+                            (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool)))
+                                (if accept?
+                                    (stop buyer (begin))
+                                    (if (> (ref contribution) (- amount 5))
+                                        (stop negotiation (displayln "negotiation failed"))
+                                        (set! contribution
+                                              (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))]))))
+
+;; buyer B
+(spawn ds-type
+       (facet buyer-b
+              (fields [funds Int 5])
+              (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard)))
+                  (let [my-contribution (- price their-contribution)]
+                    (cond
+                      [(> my-contribution (ref funds))
+                       (facet decline
+                              (fields)
+                              (assert (split-proposal title price their-contribution #f))
+                              (on (retracted (observe (split-proposal title price their-contribution discard)))
+                                  (stop decline (begin))))]
+                      [#t
+                       (facet accept
+                              (fields)
+                              (assert (split-proposal title price their-contribution #t))
+                              (on (retracted (observe (split-proposal title price their-contribution discard)))
+                                  (stop accept (begin)))
+                              (on start
+                                  (spawn ds-type
+                                         (facet purchase
+                                                (fields)
+                                                (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate))))
+                                                    (match (tuple order-id? delivery-date?)
+                                                      [(tuple (order-id (bind id Int)) (delivery-date (bind date String)))
+                                                       ;; complete!
+                                                       (begin (displayln "Completed Order:")
+                                                              (displayln title)
+                                                              (displayln id)
+                                                              (displayln date)
+                                                              (stop purchase (begin)))]
+                                                      [discard
+                                                       (begin (displayln "Order Rejected")
+                                                           (stop purchase (begin)))]))))))])))))
+)

racket/typed/main.rkt

@@ -0,0 +1,947 @@
+#lang turnstile
+
+(provide (rename-out [syndicate:#%module-begin #%module-begin])
+         (rename-out [typed-app #%app])
+         (rename-out [syndicate:begin-for-declarations declare-types])
+         #%top-interaction
+         require only-in
+         ;; Types
+         Int Bool String Tuple Bind Discard Case → Behavior FacetName Field ★
+         Observe Inbound Outbound Actor U
+         ;; Statements
+         let spawn dataspace facet set! begin stop unsafe-do
+         ;; endpoints
+         assert on
+         ;; expressions
+         tuple λ ref observe inbound outbound
+         ;; values
+         #%datum
+         ;; patterns
+         bind discard
+         ;; primitives
+         + - * / and or not > < >= <= = equal? displayln
+         ;; making types
+         define-type-alias
+         define-constructor
+         ;; DEBUG and utilities
+         print-type
+         (rename-out [printf- printf])
+         ;; Extensions
+         match if cond
+         )
+
+(require (rename-in racket/match [match-lambda match-lambda-]))
+(require (rename-in racket/math [exact-truncate exact-truncate-]))
+(require (prefix-in syndicate: syndicate/actor-lang))
+
+(module+ test
+  (require rackunit)
+  (require turnstile/rackunit-typechecking))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Types
+
+(define-base-types Int Bool String Discard ★ FacetName)
+(define-type-constructor Field #:arity = 1)
+;; (Behavior τv τi τo τa)
+;; τv is the type of thing it evaluates to
+;; τi is the type of patterns used to consume incoming assertions
+;; τo is the type of assertions made
+;; τa is the type of spawned actors
+(define-type-constructor Behavior #:arity = 4)
+(define-type-constructor Bind #:arity = 1)
+(define-type-constructor Tuple #:arity >= 0)
+(define-type-constructor U #:arity >= 0)
+(define-type-constructor Case #:arity >= 0)
+(define-type-constructor → #:arity > 0)
+(define-type-constructor Observe #:arity = 1)
+(define-type-constructor Inbound #:arity = 1)
+(define-type-constructor Outbound #:arity = 1)
+(define-type-constructor Actor #:arity = 1)
+
+(define-for-syntax (type-eval t)
+  ((current-type-eval) t))
+
+;; this needs to be here until I stop 'compiling' patterns and just have them expand to the right
+;; thing
+(begin-for-syntax
+  (current-use-stop-list? #f))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; User Defined Types, aka Constructors
+
+;; τ.norm in 1st case causes "not valid type" error when file is compiled
+;; (copied from ext-stlc example)
+(define-syntax define-type-alias
+  (syntax-parser
+    [(_ alias:id τ:any-type)
+     #'(define-syntax- alias
+         (make-variable-like-transformer #'τ.norm))]
+    [(_ (f:id x:id ...) ty)
+     #'(define-syntax- (f stx)
+         (syntax-parse stx
+           [(_ x ...)
+            #:with τ:any-type #'ty
+            #'τ.norm]))]))
+
+(begin-for-syntax
+  (define-splicing-syntax-class type-constructor-decl
+    (pattern (~seq #:type-constructor TypeCons:id))
+    (pattern (~seq) #:attr TypeCons #f))
+
+  (struct user-ctor (typed-ctor untyped-ctor)
+    #:property prop:procedure
+    (lambda (v stx)
+      (define transformer (user-ctor-typed-ctor v))
+      (syntax-parse stx
+        [(_ e ...)
+         #`(#,transformer e ...)]))))
+
+(define-syntax (define-constructor stx)
+  (syntax-parse stx
+    [(_ (Cons:id slot:id ...)
+        ty-cons:type-constructor-decl
+        (~seq #:with
+              Alias AliasBody) ...)
+     #:with TypeCons (or (attribute ty-cons.TypeCons) (format-id stx "~a/t" (syntax-e #'Cons)))
+     #:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)
+     #:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)
+     #:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)
+     #:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)
+     #:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons))
+     (define arity (stx-length #'(slot ...)))
+     #`(begin-
+         (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
+         (define-syntax (TypeConsExtraInfo stx)
+           (syntax-parse stx
+             [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)]))
+         (define-type-constructor TypeCons
+           #:arity = #,arity
+           #:extra-info 'TypeConsExtraInfo)
+         (define-syntax (MakeTypeCons stx)
+           (syntax-parse stx
+             [(_ t (... ...))
+              #:fail-unless (= #,arity (stx-length #'(t (... ...)))) "arity mismatch"
+              #'(TypeCons t (... ...))]))
+         (define-syntax (GetTypeParams stx)
+           (syntax-parse stx
+             [(_ (TypeConsExpander t (... ...)))
+              #'(t (... ...))]))
+         (define-syntax Cons
+           (user-ctor #'Cons- #'StructName))
+         (define-typed-syntax (Cons- e (... ...)) ≫
+           #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch"
+           [⊢ e ≫ e- (⇒ : τ)] (... ...)
+           ----------------------
+           [⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...)))
+              (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+         (define-type-alias Alias AliasBody) ...)]))
+
+(begin-for-syntax
+  (define-syntax ~constructor-extra-info
+    (pattern-expander
+     (syntax-parser
+       [(_ tag mk get)
+        #'(_ (_ tag) (_ mk) (_ get))])))
+
+  (define-syntax ~constructor-type
+    (pattern-expander
+     (syntax-parser
+       [(_ tag . rst)
+        #'(~and it
+                (~fail #:unless (user-defined-type? #'it))
+                (~parse tag (get-type-tag #'it))
+                (~Any _ . rst))])))
+
+  (define-syntax ~constructor-exp
+    (pattern-expander
+     (syntax-parser
+       [(_ cons . rst)
+        #'(~and (cons . rst)
+                (~fail #:unless (ctor-id? #'cons)))])))
+
+  (define (inspect t)
+    (syntax-parse t
+      [(~constructor-type tag t ...)
+       (list (syntax-e #'tag) (stx-map type->str #'(t ...)))]))
+
+  (define (tags-equal? t1 t2)
+    (equal? (syntax-e t1) (syntax-e t2)))
+    
+  (define (user-defined-type? t)
+    (get-extra-info (type-eval t)))
+
+  (define (get-type-tag t)
+    (syntax-parse (get-extra-info t)
+      [(~constructor-extra-info tag _ _)
+       (syntax-e #'tag)]))
+
+  (define (get-type-args t)
+    (syntax-parse (get-extra-info t)
+      [(~constructor-extra-info _ _ get)
+       (define f (syntax-local-value #'get))
+       (syntax->list (f #`(get #,t)))]))
+
+  (define (make-cons-type t args)
+    (syntax-parse (get-extra-info t)
+      [(~constructor-extra-info _ mk _)
+       (define f (syntax-local-value #'mk))
+        (type-eval (f #`(mk #,@args)))]))
+
+  (define (ctor-id? stx)
+    (and (identifier? stx)
+         (user-ctor? (syntax-local-value stx (const #f)))))
+
+  (define (untyped-ctor stx)
+    (user-ctor-untyped-ctor (syntax-local-value stx (const #f)))))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Syntax
+
+(begin-for-syntax
+
+#|
+it's expensive and inflexible to fully parse these, but this is what the language
+is meant to be
+  (define-syntax-class stmt
+    #:datum-literals (:
+                      begin
+                      let
+                      set!
+                      spawn
+                      dataspace
+                      stop
+                      facet
+                      unsafe-do
+                      fields)
+    (pattern (~or (begin seq:stmt ...)
+                  (e1:exp e2:exp)
+                  (let [f:id e:exp] let-fun-body:stmt)
+                  (set! x:id e:exp)
+                  (spawn τ:type s:stmt)
+                  (dataspace τ:type nested:stmt ...)
+                  (stop x:id s:stmt)
+                  (facet x:id (fields [fn:id τf:type ef:exp] ...) ep:endpoint ...+)
+                  ;; note racket expr, not exp
+                  (unsafe-do rkt:expr ...))))
+  
+  (define-syntax-class exp
+    #:datum-literals (tuple λ ref)
+    (pattern (~or (o:prim-op es:exp ...)
+                  basic-val
+                  (k:kons1 e:exp)
+                  (tuple es:exp ...)
+                  (ref x:id)
+                  (λ [p:pat s:stmt] ...))))
+|#
+
+  ;; constructors with arity one
+  (define-syntax-class kons1
+    (pattern (~or (~datum observe)
+                  (~datum inbound)
+                  (~datum outbound))))
+
+  (define (kons1->constructor stx)
+    (syntax-parse stx
+      #:datum-literals (observe inbound outbound)
+      [observe #'syndicate:observe]
+      [inbound #'syndicate:inbound]
+      [outbound #'syndicate:outbound]))
+
+  (define-syntax-class basic-val
+    (pattern (~or boolean
+                  integer
+                  string)))
+
+  (define-syntax-class prim-op
+    (pattern (~or (~literal +)
+                  (~literal -)
+                  (~literal displayln))))
+
+  #;(define-syntax-class endpoint
+    #:datum-literals (on start stop)
+    (pattern (~or (on ed:event-desc s)
+                  (assert e:expr))))
+
+  #;(define-syntax-class event-desc
+    #:datum-literals (start stop asserted retracted)
+    (pattern (~or start
+                  stop
+                  (asserted p:pat)
+                  (retracted p:pat))))
+                  
+  #;(define-syntax-class pat
+    #:datum-literals (tuple _ discard bind)
+    #:attributes (syndicate-pattern match-pattern)
+    (pattern (~or (~and (tuple ps:pat ...)
+                        (~bind [syndicate-pattern #'(list 'tuple ps.syndicate-pattern ...)]
+                               [match-pattern #'(list 'tuple ps.match-pattern ...)]))
+                  (~and (k:kons1 p:pat)
+                        (~bind [syndicate-pattern #`(#,(kons1->constructor #'k) p.syndicate-pattern)]
+                               [match-pattern #`(#,(kons1->constructor #'k) p.match-pattern)]))
+                  (~and (bind ~! x:id τ:type)
+                        (~bind [syndicate-pattern #'($ x)]
+                               [match-pattern #'x]))
+                  (~and discard
+                        (~bind [syndicate-pattern #'_]
+                               [match-pattern #'_]))
+                  (~and x:id
+                        (~bind [syndicate-pattern #'x]
+                               [match-pattern #'(== x)]))
+                  (~and e:expr
+                        (~bind [syndicate-pattern #'e]
+                               [match-pattern #'(== e)])))))
+
+  (define (compile-pattern pat bind-id-transformer exp-transformer)
+    (let loop ([pat pat])
+      (syntax-parse pat
+        #:datum-literals (tuple discard bind)
+        [(tuple p ...)
+         #`(list 'tuple #,@(stx-map loop #'(p ...)))]
+        [(k:kons1 p)
+         #`(#,(kons1->constructor #'k) #,(loop #'p))]
+        [(bind x:id τ:type)
+         (bind-id-transformer #'x)]
+        [discard
+         #'_]
+        [(~constructor-exp ctor p ...)
+         (define/with-syntax uctor (untyped-ctor #'ctor))
+         #`(uctor #,@(stx-map loop #'(p ...)))]
+        [_
+         (exp-transformer pat)])))
+
+  (define (compile-match-pattern pat)
+    (compile-pattern pat
+                     identity
+                     (lambda (exp) #`(== #,exp))))
+
+  (define (compile-syndicate-pattern pat)
+    (compile-pattern pat
+                     (lambda (id) #`($ #,id))
+                     identity)))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Subtyping
+
+;; TODO: subtyping for facets
+
+;; Type Type -> Bool
+(define-for-syntax (<: t1 t2)
+  #;(printf "Checking ~a <: ~a\n" (type->str t1) (type->str t2))
+  ;; should add a check for type=?
+  (syntax-parse #`(#,t1 #,t2)
+    #;[(τ1 τ2) #:do [(displayln (type->str #'τ1))
+                     (displayln (type->str #'τ2))]
+               #:when #f
+               (error "")]
+    [((~U τ1 ...) _)
+     (stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
+    [(_ (~U τ2:type ...))
+     (stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
+    [((~Actor τ1:type) (~Actor τ2:type))
+     ;; should these be .norm? Is the invariant that inputs are always fully
+     ;; evalutated/expanded?
+     (and (<: #'τ1 #'τ2)
+          (<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
+    [((~Tuple τ1:type ...) (~Tuple τ2:type ...))
+     #:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
+     (stx-andmap <: #'(τ1 ...) #'(τ2 ...))]
+    [(_ ~★)
+     (flat-type? t1)]
+    [((~Observe τ1:type) (~Observe τ2:type))
+     (<: #'τ1 #'τ2)]
+    [((~Inbound τ1:type) (~Inbound τ2:type))
+     (<: #'τ1 #'τ2)]
+    [((~Outbound τ1:type) (~Outbound τ2:type))
+     (<: #'τ1 #'τ2)]
+    [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...))
+     #:when (tags-equal? #'t1 #'t2)
+     (and (stx-length=? #'(τ1 ...) #'(τ2 ...))
+          (stx-andmap <: #'(τ1 ...) #'(τ2 ...)))]
+    [((~Behavior τ-v1 τ-i1 τ-o1 τ-a1) (~Behavior τ-v2 τ-i2 τ-o2 τ-a2))
+     (and (<: #'τ-v1 #'τ-v2)
+          ;; HMMMMMM. i2 and i1 are types of patterns. TODO
+          ;; Want: ∀σ. project-safe(σ, τ-i2) ⇒ project-safe(σ, τ-i1)
+          (<: #'τ-i2 #'τ-i1)
+          (<: #'τ-o1 #'τ-o2)
+          (<: (type-eval #'(Actor τ-a1)) (type-eval #'(Actor τ-a2))))]
+    [((~→ τ-in1 ... τ-out1) (~→ τ-in2 ... τ-out2))
+     #:when (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...))
+     (and (stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...))
+          (<: #'τ-out1 #'τ-out2))]
+    [((~Field τ1) (~Field τ2))
+     (and (<: #'τ1 #'τ2)
+          (<: #'τ2 #'τ1))]
+    [(~Discard _)
+     #t]
+    [((~Bind τ1) (~Bind τ2))
+     (<: #'τ1 #'τ2)]
+    ;; should probably put this first.
+    [_ (type=? t1 t2)]))
+
+;; Flat-Type Flat-Type -> Type
+(define-for-syntax (∩ t1 t2)
+  (unless (and (flat-type? t1) (flat-type? t2))
+    (error '∩ "expected two flat-types"))
+  (syntax-parse #`(#,t1 #,t2)
+    [(_ ~★)
+     t1]
+    [(~★ _)
+     t2]
+    [(_ _)
+     #:when (type=? t1 t2)
+     t1]
+    [((~U τ1:type ...) _)
+     (type-eval #`(U #,@(stx-map (lambda (t) (∩ t t2)) #'(τ1 ...))))]
+    [(_ (~U τ2:type ...))
+     (type-eval #`(U #,@(stx-map (lambda (t) (∩ t1 t)) #'(τ2 ...))))]
+    ;; all of these fail-when/unless clauses are meant to cause this through to
+    ;; the last case and result in ⊥.
+    ;; Also, using <: is OK, even though <: refers to ∩, because <:'s use of ∩ is only
+    ;; in the Actor case.
+    [((~Tuple τ1:type ...) (~Tuple τ2:type ...))
+     #:fail-unless (stx-length=? #'(τ1 ...) #'(τ2 ...)) #f
+     #:with (τ ...) (stx-map ∩ #'(τ1 ...) #'(τ2 ...))
+     ;; I don't think stx-ormap is part of the documented api of turnstile *shrug*
+     #:fail-when (stx-ormap (lambda (t) (<: t (type-eval #'(U)))) #'(τ ...)) #f
+     (type-eval #'(Tuple τ ...))]
+    [((~constructor-type tag1 τ1:type ...) (~constructor-type tag2 τ2:type ...))
+     #:when (tags-equal? #'tag1 #'tag2)
+     #:with (τ ...) (stx-map ∩ #'(τ1 ...) #'(τ2 ...))
+     #:fail-when (stx-ormap (lambda (t) (<: t (type-eval #'(U)))) #'(τ ...)) #f
+     (make-cons-type t1 #'(τ ...))]
+    ;; these three are just the same :(
+    [((~Observe τ1:type) (~Observe τ2:type))
+     #:with τ (∩ #'τ1 #'τ2)
+     #:fail-when (<: #'τ (type-eval #'(U))) #f
+     (type-eval #'(Observe τ))]
+    [((~Inbound τ1:type) (~Inbound τ2:type))
+     #:with τ (∩ #'τ1 #'τ2)
+     #:fail-when (<: #'τ (type-eval #'(U))) #f
+     (type-eval #'(Inbound τ))]
+    [((~Outbound τ1:type) (~Outbound τ2:type))
+     #:with τ (∩ #'τ1 #'τ2)
+     #:fail-when (<: #'τ (type-eval #'(U))) #f
+     (type-eval #'(Outbound τ))]
+    [_ (type-eval #'(U))]))
+
+;; Type Type -> Bool
+;; first type is the contents of the set
+;; second type is the type of a pattern
+(define-for-syntax (project-safe? t1 t2)
+  (syntax-parse #`(#,t1 #,t2)
+    [(_ (~Bind τ2:type))
+     (and (finite? t1) (<: t1 #'τ2))]
+    [(_ ~Discard)
+     #t]
+    [((~U τ1:type ...) _)
+     (stx-andmap (lambda (t) (project-safe? t t2)) #'(τ1 ...))]
+    [(_ (~U τ2:type ...))
+     (stx-andmap (lambda (t) (project-safe? t1 t)) #'(τ2 ...))]
+    [((~Tuple τ1:type ...) (~Tuple τ2:type ...))
+     #:when (overlap? t1 t2)
+     (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))]
+    [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...))
+     #:when (tags-equal? #'t1 #'t2)
+     (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))]
+    [((~Observe τ1:type) (~Observe τ2:type))
+     (project-safe? #'τ1 #'τ2)]
+    [((~Inbound τ1:type) (~Inbound τ2:type))
+     (project-safe? #'τ1 #'τ2)]
+    [((~Outbound τ1:type) (~Outbound τ2:type))
+     (project-safe? #'τ1 #'τ2)]
+    [_ #t]))
+
+;; AssertionType PatternType -> Bool
+;; Is it possible for things of these two types to match each other?
+;; Flattish-Type = Flat-Types + ★, Bind, Discard (assertion and pattern types)
+(define-for-syntax (overlap? t1 t2)
+  (syntax-parse #`(#,t1 #,t2)
+    [(~★ _) #t]
+    [(_ (~Bind _)) #t]
+    [(_ ~Discard) #t]
+    [((~U τ1:type ...) _)
+     (stx-ormap (lambda (t) (overlap? t t2)) #'(τ1 ...))]
+    [(_ (~U τ2:type ...))
+     (stx-ormap (lambda (t) (overlap? t1 t)) #'(τ2 ...))]
+    [((~Tuple τ1:type ...) (~Tuple τ2:type ...))
+     (and (stx-length=? #'(τ1 ...) #'(τ2 ...))
+          (stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))]
+    [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...))
+     (and (tags-equal? #'t1 #'t2)
+          (stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))]
+    [((~Observe τ1:type) (~Observe τ2:type))
+     (overlap? #'τ1 #'τ2)]
+    [((~Inbound τ1:type) (~Inbound τ2:type))
+     (overlap? #'τ1 #'τ2)]
+    [((~Outbound τ1:type) (~Outbound τ2:type))
+     (overlap? #'τ1 #'τ2)]
+    [_ (<: t1 t2)]))
+    
+
+;; Flattish-Type -> Bool
+(define-for-syntax (finite? t)
+  (syntax-parse t
+    [~★ #f]
+    [(~U τ:type ...)
+     (stx-andmap finite? #'(τ ...))]
+    [(~Tuple τ:type ...)
+     (stx-andmap finite? #'(τ ...))]
+    [(~constructor-type _ τ:type ...)
+     (stx-andmap finite? #'(τ ...))]
+    [(~Observe τ:type)
+     (finite? #'τ)]
+    [(~Inbound τ:type)
+     (finite? #'τ)]
+    [(~Outbound τ:type)
+     (finite? #'τ)]
+    [_ #t]))
+
+;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+;; MODIFYING GLOBAL TYPECHECKING STATE!!!!!
+;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+
+(begin-for-syntax
+  (current-typecheck-relation <:))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Statements
+
+;; CONVENTIONS
+;; The `:` key is for evaluated expressions
+;; The `:i` key is for input patterns
+;; The `:o` key is for output assertions
+;; The `:a` key is for spawned actors
+
+(define-typed-syntax (set! x:id e:expr) ≫
+  [⊢ e ≫ e- (⇒ : τ)]
+  [⊢ x ≫ x- (⇒ : (~Field τ-x:type))]
+  #:fail-unless (<: #'τ #'τ-x) "Ill-typed field write"
+  ----------------------------------------------------
+  [⊢ (x- e-) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax (stop facet-name:id cont) ≫
+  [⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
+  [⊢ cont ≫ cont- (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)]
+  --------------------------------------------------
+  [⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : (U)) (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)])
+
+(define-typed-syntax (facet name:id ((~datum fields) [x:id τ:type e:expr] ...) ep ...+) ≫
+  #:fail-unless (stx-andmap flat-type? #'(τ ...)) "keep your uppity data outa my fields"
+  [⊢ e ≫ e- (⇐ : τ)] ...
+  [[name ≫ name- : FacetName] [x ≫ x- : (Field τ)] ...
+   ⊢ [ep ≫ ep- (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)] ...]
+  --------------------------------------------------------------
+  ;; name NOT name- here because I get an error that way.
+  ;; Since name is just an identifier I think it's OK?
+  [⊢ (syndicate:react (let- ([name- (syndicate:current-facet-id)])
+                            #,(make-fields #'(x- ...) #'(e- ...))
+                            #;(syndicate:field [x- e-] ...)
+                            ep- ...))
+     (⇒ : (U)) (⇒ :i (U τ-i ...)) (⇒ :o (U τ-o ...)) (⇒ :a (U τ-a ...))])
+
+(define-for-syntax (make-fields names inits)
+  (syntax-parse #`(#,names #,inits)
+    [((x:id ...) (e ...))
+     #'(syndicate:field [x e] ...)]))
+
+(define-typed-syntax (dataspace τ-c:type s ...) ≫
+  ;; #:do [(printf "τ-c: ~a\n" (type->str #'τ-c.norm))]
+  #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
+  [⊢ s ≫ s- (⇒ :i τ-i:type) (⇒ :o τ-o:type) (⇒ :a τ-s:type)] ...
+  ;; #:do [(printf "dataspace types: ~a\n" (stx-map type->str #'(τ-s.norm ...)))
+  ;;      (printf "dataspace type: ~a\n" (type->str ((current-type-eval) #'(Actor τ-c.norm))))]
+  #:fail-unless (stx-andmap (lambda (t) (<: (type-eval #`(Actor #,t))
+                                            (type-eval #'(Actor τ-c.norm))))
+                            #'(τ-s.norm ...))
+                "Not all actors conform to communication type"
+  #:fail-unless (stx-andmap (lambda (t) (<: t (type-eval #'(U))))
+                            #'(τ-i.norm ...)) "dataspace init should only be a spawn"
+  #:fail-unless (stx-andmap (lambda (t) (<: t (type-eval #'(U))))
+                            #'(τ-o.norm ...)) "dataspace init should only be a spawn"
+  #:with τ-ds-i (strip-inbound #'τ-c.norm)
+  #:with τ-ds-o (strip-outbound #'τ-c.norm)
+  #:with τ-relay (relay-interests #'τ-c.norm)
+  -----------------------------------------------------------------------------------
+  [⊢ (syndicate:dataspace s- ...) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U τ-ds-i τ-ds-o τ-relay))])
+
+(define-for-syntax (strip-? t)
+  (type-eval
+   (syntax-parse t
+     ;; TODO: probably need to `normalize` the result
+     [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
+     [~★ #'★]
+     [(~Observe τ) #'τ]
+     [_ #'(U)])))
+
+(define-for-syntax (strip-inbound t)
+  (type-eval
+   (syntax-parse t
+     ;; TODO: probably need to `normalize` the result
+     [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
+     [~★ #'★]
+     [(~Inbound τ) #'τ]
+     [_ #'(U)])))
+
+(define-for-syntax (strip-outbound t)
+  (type-eval
+   (syntax-parse t
+     ;; TODO: probably need to `normalize` the result
+     [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
+     [~★ #'★]
+     [(~Outbound τ) #'τ]
+     [_ #'(U)])))
+
+(define-for-syntax (relay-interests t)
+  (type-eval
+   (syntax-parse t
+     ;; TODO: probably need to `normalize` the result
+     [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
+     [~★ #'★]
+     [(~Observe (~Inbound τ)) #'(Observe τ)]
+     [_ #'(U)])))
+
+(define-typed-syntax (spawn τ-c:type s) ≫
+  #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
+  [⊢ s ≫ s- (⇒ :i τ-i:type) (⇒ :o τ-o:type) (⇒ :a τ-a:type)]
+  ;; TODO: s shouldn't refer to facets or fields!
+  #:fail-unless (<: #'τ-o.norm #'τ-c.norm)
+                (format "Output ~a not valid in dataspace ~a" (type->str #'τ-o.norm) (type->str #'τ-c.norm))
+  #:fail-unless (<: (type-eval #'(Actor τ-a.norm))
+                    (type-eval #'(Actor τ-c.norm))) "Spawned actors not valid in dataspace"
+  #:fail-unless (project-safe? (∩ (strip-? #'τ-o.norm) #'τ-c.norm)
+                               #'τ-i.norm) "Not prepared to handle all inputs"
+  ;; #:do [(printf "spawning: ~v\n" #'s-)]
+  --------------------------------------------------------------------------------------------
+  [⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a τ-c)])
+
+(define-typed-syntax (let [f:id e:expr] body:expr) ≫
+  [⊢ e ≫ e- (⇒ : τ:type)]
+  #:fail-unless (or (procedure-type? #'τ.norm) (flat-type? #'τ.norm))
+                (format "let doesn't bind actions; got ~a" (type->str #'τ.norm))
+  [[f ≫ f- : τ] ⊢ body ≫ body- (⇒ : τ-body) (⇒ :i τ-body-i) (⇒ :o τ-body-o) (⇒ :a τ-body-a)]
+   ------------------------------------------------------------------------
+  [⊢ (let- ([f- e-]) body-) (⇒ : τ-body) (⇒ :i τ-body-i) (⇒ :o τ-body-o) (⇒ :a τ-body-a)])
+
+(define-for-syntax (procedure-type? τ)
+  (syntax-parse τ
+    [(~→ τ ...+) #t]
+    [_ #f]))
+
+(define-typed-syntax (begin s ...) ≫
+  [⊢ s ≫ s- (⇒ :i τ1) (⇒ :o τ2) (⇒ :a τ3)] ...
+  ------------------------------------------
+  [⊢ (begin- (void-) s- ...) (⇒ : (U)) (⇒ :i (U τ1 ...)) (⇒ :o (U τ2 ...)) (⇒ :a (U τ3 ...))])
+
+(define-for-syntax (flat-type? τ)
+  (syntax-parse τ
+    [(~→ τ ...) #f]
+    [(~Field _) #f]
+    [(~Behavior _ _ _ _) #f]
+    [_ #t]))
+
+(define-typed-syntax (unsafe-do rkt:expr ...) ≫
+  ------------------------
+  [⊢ (let- () rkt ...) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Endpoints
+
+(begin-for-syntax
+  (define-syntax-class asserted-or-retracted
+    #:datum-literals (asserted retracted)
+    (pattern (~or (~and asserted
+                        (~bind [syndicate-kw #'syndicate:asserted]))
+                  (~and retracted
+                        (~bind [syndicate-kw #'syndicate:retracted]))))))
+
+(define-typed-syntax on
+  [(on (~literal start) s) ≫
+   [⊢ s ≫ s- (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]
+   -----------------------------------
+   [⊢ (syndicate:on-start s-) (⇒ : (U)) (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]]
+  [(on (~literal stop) s) ≫
+   [⊢ s ≫ s- (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]
+   -----------------------------------
+   [⊢ (syndicate:on-stop s-) (⇒ : (U)) (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]]
+  [(on (a/r:asserted-or-retracted p) s) ≫
+   [⊢ p ≫ _ (⇒ : τp)]
+   #:with p- (compile-syndicate-pattern #'p)
+   #:with ([x:id τ:type] ...) (pat-bindings #'p)
+   [[x ≫ x- : τ] ... ⊢ s ≫ s- (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]
+   ;; the type of subscriptions to draw assertions to the pattern
+   #:with pat-sub (replace-bind-and-discard-with-★ #'τp)
+   -----------------------------------
+   [⊢ (syndicate:on (a/r.syndicate-kw p-)
+                    (let- ([x- x] ...) s-))
+      (⇒ : (U))
+      (⇒ :i (U τi τp))
+      (⇒ :o (U (Observe pat-sub) τ-o))
+      (⇒ :a τ-a)]])
+
+;; FlattishType -> FlattishType
+(define-for-syntax (replace-bind-and-discard-with-★ t)
+  (syntax-parse t
+    [(~Bind _)
+     (type-eval #'★)]
+    [~Discard
+     (type-eval #'★)]
+    [(~U τ ...)
+     (type-eval #`(U #,@(stx-map replace-bind-and-discard-with-★ #'(τ ...))))]
+    [(~Tuple τ ...)
+     (type-eval #`(Tuple #,@(stx-map replace-bind-and-discard-with-★ #'(τ ...))))]
+    [(~Observe τ)
+     (type-eval #`(Observe #,(replace-bind-and-discard-with-★ #'τ)))]
+    [(~Inbound τ)
+     (type-eval #`(Inbound #,(replace-bind-and-discard-with-★ #'τ)))]
+    [(~Outbound τ)
+     (type-eval #`(Outbound #,(replace-bind-and-discard-with-★ #'τ)))]
+    [(~constructor-type _ τ ...)
+     (make-cons-type t (stx-map replace-bind-and-discard-with-★ #'(τ ...)))]
+    [_ t]))
+
+(define-typed-syntax (assert e:expr) ≫
+  [⊢ e ≫ e- (⇒ : τ:type)]
+  #:with τ-in (strip-? #'τ.norm)
+  -------------------------------------
+  [⊢ (syndicate:assert e-) (⇒ : (U)) (⇒ :i τ-in) (⇒ :o τ) (⇒ :a (U))])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Expressions
+
+(define-typed-syntax (tuple e:expr ...) ≫
+  [⊢ e ≫ e- (⇒ : τ)] ...
+  -----------------------
+  [⊢ (list 'tuple e- ...) (⇒ : (Tuple τ ...)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax (ref x:id) ≫
+  [⊢ x ≫ x- ⇒ (~Field τ)]
+  ------------------------
+  [⊢ (x-) (⇒ : τ) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax (λ [p s] ...) ≫
+  #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
+  [[x ≫ x- : τ :i (U) :o (U) :a (U)] ... ⊢ s ≫ s- (⇒ : τv) (⇒ :i τ1) (⇒ :o τ2) (⇒ :a τ3)] ...
+  ;; REALLY not sure how to handle p/p-/p.match-pattern,
+  ;; particularly w.r.t. typed terms that appear in p.match-pattern
+  [⊢ p ≫ _ ⇒ τ-p] ...
+  #:with (p- ...) (stx-map compile-match-pattern #'(p ...))
+  #:with (τ-in ...) (stx-map lower-pattern-type #'(τ-p ...))
+  --------------------------------------------------------------
+  ;; TODO: add a catch-all error clause
+  [⊢ (match-lambda- [p- (let- ([x- x] ...) s-)] ...)
+     (⇒ : (→ (U τ-p ...) (Behavior (U τv ...) (U τ1 ...) (U τ2 ...) (U τ3 ...))))
+     (⇒ :i (U))
+     (⇒ :o (U))
+     (⇒ :a (U))])
+
+;; FlattishType -> FlattishType
+;; replaces (Bind τ) with τ and Discard with ★
+(define-for-syntax (lower-pattern-type t)
+  (syntax-parse t
+    [(~Bind τ)
+     #'τ]
+    [~Discard
+     (type-eval #'★)]
+    [(~U τ ...)
+     (type-eval #`(U #,@(stx-map lower-pattern-type #'(τ ...))))]
+    [(~Tuple τ ...)
+     (type-eval #`(Tuple #,@(stx-map lower-pattern-type #'(τ ...))))]
+    [(~Observe τ)
+     (type-eval #`(Observe #,(lower-pattern-type #'τ)))]
+    [(~Inbound τ)
+     (type-eval #`(Inbound #,(lower-pattern-type #'τ)))]
+    [(~Outbound τ)
+     (type-eval #`(Outbound #,(lower-pattern-type #'τ)))]
+    [(~constructor-type _ τ ...)
+     (make-cons-type t (stx-map lower-pattern-type #'(τ ...)))]
+    [_ t]))
+
+(define-typed-syntax (typed-app e_fn e_arg ...) ≫
+  [⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in:type ... (~Behavior τ-v τ-i τ-o τ-a)))]
+  #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+                (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+  [⊢ e_arg ≫ e_arg- (⇒ : τ_arg:type)] ...
+  ;; #:do [(printf "~a\n" (stx-map type->str #'(τ_arg.norm ...)))
+  ;;      (printf "~a\n" (stx-map type->str #'(τ_in.norm ...) #;(stx-map lower-pattern-type #'(τ_in.norm ...))))]
+  #:fail-unless (stx-andmap <: #'(τ_arg.norm ...) (stx-map lower-pattern-type #'(τ_in.norm ...)))
+  "argument mismatch"
+  #:fail-unless (stx-andmap project-safe? #'(τ_arg.norm ...) #'(τ_in.norm ...))
+  "match error"
+  ------------------------------------------------------------------------
+  [⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ-v) (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)])
+
+;; it would be nice to abstract over these three
+(define-typed-syntax (observe e:expr) ≫
+  [⊢ e ≫ e- (⇒ : τ)]
+  ---------------------------------------------------------------------------
+  [⊢ (syndicate:observe e-) (⇒ : (Observe τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax (inbound e:expr) ≫
+  [⊢ e ≫ e- ⇒ τ]
+  ---------------------------------------------------------------------------
+  [⊢ (syndicate:inbound e-) (⇒ : (Inbound τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax (outbound e:expr) ≫
+  [⊢ e ≫ e- ⇒ τ]
+  ---------------------------------------------------------------------------
+  [⊢ (syndicate:outbound e-) (⇒ : (Outbound τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Patterns
+
+(define-typed-syntax (bind x:id τ:type) ≫
+  ----------------------------------------
+  ;; TODO: at some point put $ back in
+  [⊢ (void-) (⇒ : (Bind τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax discard
+  [_ ≫
+   --------------------
+   ;; TODO: change void to _
+   [⊢ (void-) (⇒ : Discard) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]])
+
+;; pat -> ([Id Type] ...)
+(define-for-syntax (pat-bindings stx)
+  (syntax-parse stx
+    #:datum-literals (bind tuple)
+    [(bind x:id τ:type)
+     #'([x τ])]
+    [(tuple p ...)
+     #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
+     #'([x τ] ... ...)]
+    [(k:kons1 p)
+     (pat-bindings #'p)]
+    [(~constructor-exp cons p ...)
+     #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
+     #'([x τ] ... ...)]
+    [_
+     #'()]))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Primitives
+
+;; hmmm
+(define-primop + (→ Int Int (Behavior Int (U) (U) (U))))
+(define-primop - (→ Int Int (Behavior Int (U) (U) (U))))
+(define-primop * (→ Int Int (Behavior Int (U) (U) (U))))
+#;(define-primop and (→ Bool Bool (Behavior Bool (U) (U) (U))))
+(define-primop or (→ Bool Bool (Behavior Bool (U) (U) (U))))
+(define-primop not (→ Bool (Behavior Bool (U) (U) (U))))
+(define-primop < (→ Int Int (Behavior Bool (U) (U) (U))))
+(define-primop > (→ Int Int (Behavior Bool (U) (U) (U))))
+(define-primop <= (→ Int Int (Behavior Bool (U) (U) (U))))
+(define-primop >= (→ Int Int (Behavior Bool (U) (U) (U))))
+(define-primop = (→ Int Int (Behavior Bool (U) (U) (U))))
+
+(define-typed-syntax (/ e1 e2) ≫
+  [⊢ e1 ≫ e1- (⇐ : Int)]
+  [⊢ e2 ≫ e2- (⇐ : Int)]
+  ------------------------
+  [⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+;; for some reason defining `and` as a prim op doesn't work
+(define-typed-syntax (and e ...) ≫
+  [⊢ e ≫ e- (⇐ : Bool)] ...
+  ------------------------
+  [⊢ (and- e- ...) (⇒ : Bool) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax (equal? e1:expr e2:expr) ≫
+  [⊢ e1 ≫ e1- (⇒ : τ1:type)]
+  #:fail-unless (flat-type? #'τ1.norm)
+  (format "equality only available on flat data; got ~a" (type->str #'τ1))
+  [⊢ e2 ≫ e2- (⇐ : τ1)]
+  ---------------------------------------------------------------------------
+  [⊢ (equal?- e1- e2-) (⇒ : Bool) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+
+(define-typed-syntax (displayln e:expr) ≫
+  [⊢ e ≫ e- ⇒ τ]
+  ---------------
+  [⊢ (displayln- e-) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
+  
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Basic Values
+
+(define-typed-syntax #%datum
+  [(_ . n:integer) ≫
+  ----------------
+  [⊢ (#%datum- . n) (⇒ : Int) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]]
+  [(_ . b:boolean) ≫
+  ----------------
+  [⊢ (#%datum- . b) (⇒ : Bool) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]]
+  [(_ . s:string) ≫
+  ----------------
+  [⊢ (#%datum- . s) (⇒ : String) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Utilities
+
+#;(define-syntax (begin/void-default stx)
+  (syntax-parse stx
+    [(_)
+     (syntax/loc stx (void))]
+    [(_ expr0 expr ...)
+     (syntax/loc stx (begin- expr0 expr ...))]))
+
+
+
+(define-typed-syntax (print-type e) ≫
+  [⊢ e ≫ e- ⇒ τ]
+  #:do [(displayln (type->str #'τ))]
+  ----------------------------------
+  [⊢ e- ⇒ τ])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Extensions
+
+(define-syntax (match stx)
+  (syntax-parse stx
+    [(match e [pat body] ...+)
+     (syntax/loc stx
+       (typed-app (λ [pat body] ...) e))]))
+
+(define-syntax (if stx)
+  (syntax-parse stx
+    [(if e1 e2 e3)
+     (syntax/loc stx
+       (typed-app (λ [#f e3] [discard e2]) e1))]))
+
+(define-typed-syntax (cond [pred:expr s] ...+) ≫
+  [⊢ pred ≫ pred- (⇐ : Bool)] ...
+  [⊢ s ≫ s- (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)] ...
+  ------------------------------------------------
+  [⊢ (cond- [pred- s-] ...) (⇒ : (U)) (⇒ :i (U τ-i ...)) (⇒ :o (U τ-o ...)) (⇒ :a (U τ-a ...))])
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Tests
+
+;; WANTED UNIT TESTS
+;; (check-true (<: #'(U String) #'String))
+;; (check-true (<: #'(U (U)) #'String))
+;; (check-true (<: #'(Actor (U (U))) #'(Actor String))
+;; (check-true (<: #'(Actor (U (U))) #'(Actor (U (Observe ★) String)))
+;; (check-true (<: ((current-type-eval) #'(U (U) (U))) ((current-type-eval) #'(U))))
+;; (check-false (<: ((current-type-eval) #'(Actor (U (Observe ★) String Int)))
+;;                  ((current-type-eval) #'(Actor (U (Observe ★) String)))))
+;; (check-true (<: (Actor (U (Observe ★) String)) (Actor (U (Observe ★) String)))
+
+(module+ test
+  (check-type 1 : Int)
+
+  (check-type (tuple 1 2 3) : (Tuple Int Int Int))
+
+  (check-type (tuple discard 1 (bind x Int)) : (Tuple Discard Int (Bind Int)))
+
+  #;(check-type (λ [(bind x Int) (begin)]) : (Case [→ (Bind Int) (Facet (U) (U) (U))]))
+  #;(check-true (void? ((λ [(bind x Int) (begin)]) 1))))
+
+(define-syntax (test-syntax-class stx)
+  (syntax-parse stx
+    [(_ e class:id)
+     #`(let ()
+         (define-syntax (test-result stx)
+           (syntax-parse e
+             [(~var _ class) #'#t]
+             [_ #'#f]))
+         (test-result))]))

racket/typed/syndicate/core/lang/reader.rkt

@@ -0,0 +1,2 @@
+#lang s-exp syntax/module-reader
+typed/core

racket/typed/syndicate/lang/reader.rkt

@@ -0,0 +1,2 @@
+#lang s-exp syntax/module-reader
+typed/main

racket/typed/syndicate/roles/lang/reader.rkt

@@ -0,0 +1,2 @@
+#lang s-exp syntax/module-reader
+typed/roles