diff --git a/racket/typed/examples/roles/bank-account.rkt b/racket/typed/examples/roles/bank-account.rkt
index 61d65ff..4ca998f 100644
--- a/racket/typed/examples/roles/bank-account.rkt
+++ b/racket/typed/examples/roles/bank-account.rkt
@@ -27,7 +27,7 @@
   (spawn ds-type
     (print-role
     (start-facet account-manager
-      (fields [balance Int 0])
+      (field [balance Int 0])
       (assert (account (ref balance)))
       (on (asserted (deposit (bind amount Int)))
           (set! balance (+ (ref balance) amount))))))
@@ -35,16 +35,13 @@
   (spawn ds-type
     (print-role
     (start-facet observer
-      (fields)
       (on (asserted (account (bind amount Int)))
           (displayln amount)))))
 
   (spawn ds-type
     (print-role
     (start-facet buyer
-      (fields)
       (on (asserted (observe (deposit discard)))
           (start-facet deposits
-            (fields)
             (assert (deposit 100))
             (assert (deposit -30))))))))
\ No newline at end of file
diff --git a/racket/typed/examples/roles/ping-pong.rkt b/racket/typed/examples/roles/ping-pong.rkt
index 16a1b9f..cae9503 100644
--- a/racket/typed/examples/roles/ping-pong.rkt
+++ b/racket/typed/examples/roles/ping-pong.rkt
@@ -10,14 +10,11 @@
 (dataspace ds-type
   (spawn ds-type
     (start-facet echo
-      (fields)
       (on (asserted (tuple "ping" (bind x Int)))
           (start-facet _
-            (fields)
             (assert (tuple "pong" x))))))
   (spawn ds-type
     (start-facet serve
-      (fields)
       (assert (tuple "ping" 8339))
       (on (asserted (tuple "pong" (bind x Int)))
           (printf "pong: ~v\n" x)))))
\ No newline at end of file
diff --git a/racket/typed/examples/roles/simple-dataspace.rkt b/racket/typed/examples/roles/simple-dataspace.rkt
index 350a980..3ab69c9 100644
--- a/racket/typed/examples/roles/simple-dataspace.rkt
+++ b/racket/typed/examples/roles/simple-dataspace.rkt
@@ -3,5 +3,4 @@
 (dataspace Int
   (spawn Int
     (start-facet _
-      (fields)
       (assert 42))))
diff --git a/racket/typed/examples/roles/simple-during.rkt b/racket/typed/examples/roles/simple-during.rkt
index 7faa029..335821e 100644
--- a/racket/typed/examples/roles/simple-during.rkt
+++ b/racket/typed/examples/roles/simple-during.rkt
@@ -12,19 +12,16 @@
 (dataspace ds-type
   (spawn ds-type
     (start-facet _
-      (fields)
       (during (tuple "GO")
         (assert (tuple "ready")))))
   (spawn ds-type
     (start-facet flag
-      (fields)
       ;; type error when this was mistakenly just "GO"
       (assert (tuple "GO"))
       (on (asserted (tuple "ready"))
           (stop flag))))
   (spawn ds-type
     (start-facet obs
-      (fields)
       (during (tuple (bind s String))
         (on start
             (printf "+~a\n" s))
diff --git a/racket/typed/examples/roles/simple-stop-facet.rkt b/racket/typed/examples/roles/simple-stop-facet.rkt
index 710bd19..fbf54a5 100644
--- a/racket/typed/examples/roles/simple-stop-facet.rkt
+++ b/racket/typed/examples/roles/simple-stop-facet.rkt
@@ -16,17 +16,14 @@
   (spawn ds-type
    (print-role
    (start-facet doomed
-     (fields)
      (assert (tuple 18))
      (on (asserted (tuple 42))
          (stop doomed
                 (start-facet the-afterlife
-                  (fields)
                   (assert (tuple 88))))))))
 
   (spawn ds-type
     (start-facet obs
-      (fields)
       (assert (tuple 42))
       (on (asserted (tuple (bind x Int)))
           (printf "+~v\n" x))
@@ -36,7 +33,6 @@
   ;; null-ary stop
   (spawn ds-type
     (start-facet meep
-      (fields)
       (assert (tuple 9))
       (on (asserted (tuple 88))
           (stop meep)))))
\ No newline at end of file
diff --git a/racket/typed/examples/roles/two-buyer-protocol.rkt b/racket/typed/examples/roles/two-buyer-protocol.rkt
index 27b6593..f7cf11a 100644
--- a/racket/typed/examples/roles/two-buyer-protocol.rkt
+++ b/racket/typed/examples/roles/two-buyer-protocol.rkt
@@ -65,11 +65,10 @@
 ;; seller
 (spawn ds-type
   (start-facet _
-    (fields [book (Tuple String Int) (tuple "Catch 22" 22)]
-            [next-order-id Int 10001483])
+    (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
-          (fields)
           (on (retracted (observe (quote title discard)))
               (stop x))
           (match title
@@ -79,7 +78,6 @@
              (assert (quote title (out-of-stock)))])))
     (on (asserted (observe (order (bind title String) (bind offer Int) discard discard)))
         (start-facet x
-          (fields)
           (on (retracted (observe (order title offer discard discard)))
               (stop x))
           (let ([asking-price 22])
@@ -92,15 +90,15 @@
 ;; buyer A
 (spawn ds-type
   (start-facet buyer
-    (fields [title String "Catch 22"]
-            [budget Int 1000])
+    (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
-             (fields [contribution Int (/ amount 2)])
+             (field [contribution Int (/ amount 2)])
              (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool)))
                  (if accept?
                      (stop buyer)
@@ -112,26 +110,23 @@
 ;; buyer B
 (spawn ds-type
   (start-facet buyer-b
-    (fields [funds Int 5])
+    (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
-               (fields)
                (assert (split-proposal title price their-contribution #f))
                (on (retracted (observe (split-proposal title price their-contribution discard)))
                    (stop decline)))]
             [#t
              (start-facet accept
-               (fields)
                (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
-                       (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)))
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index d9b4e9e..034d8ba 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -9,12 +9,13 @@
          Role Reacts Shares Know ¬Know Message Stop
          FacetName Field ★/t
          Observe Inbound Outbound Actor U
+         Computation Value Endpoints Roles Spawns
          ;; Statements
          let let* if spawn dataspace start-facet set! begin stop #;unsafe-do
          ;; Derived Forms
          during
          ;; endpoints
-         assert on
+         assert on field
          ;; expressions
          tuple lambda ref observe inbound outbound
          ;; making types
@@ -56,14 +57,12 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; : describes the immediate result of evaluation
-;; a key aggregates `assert` endpoints as `Shares`
-;; r key aggregates each `on` endpoint as a `Reacts`
+;; ep key aggregates endpoint affects:
+;;   `Shares`, `Reacts`, and `MakesField`
+;; Note thar MakesField is only an effect, not a type
 ;; f key aggregates facet effects (starting a facet) as `Role`s
 ;; s key aggregates spawned actors as `Actor`s
 
-;; TODO - chan the `a` and `r` keys be merged into one 'endpoint' key?
-
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Types
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -77,7 +76,9 @@
 (define-type-constructor Message #:arity = 1)
 (define-type-constructor Field #:arity = 1)
 (define-type-constructor Bind #:arity = 1)
-(define-base-types OnStart OnStop)
+(define-base-types OnStart OnStop MakesField)
+;; MakesField has a syntax property ([x x- τ] ...)
+(define-for-syntax field-prop-name 'fields)
 
 
 (define-type-constructor Tuple #:arity >= 0)
@@ -93,10 +94,9 @@
 (define-type-constructor → #:arity > 0)
 ;; for describing the RHS
 ;; a value and a description of the effects
-(define-type-constructor Computation #:arity = 5)
+(define-type-constructor Computation #:arity = 4)
 (define-type-constructor Value #:arity = 1)
-(define-type-constructor Asserts #:arity >= 0)
-(define-type-constructor Reactions #:arity >= 0)
+(define-type-constructor Endpoints #:arity >= 0)
 (define-type-constructor Roles #:arity >= 0)
 (define-type-constructor Spawns #:arity >= 0)
 
@@ -209,7 +209,8 @@
            (user-ctor #'Cons- #'StructName))
          (define-typed-syntax (Cons- e (... ...)) ≫
            #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch"
-           [⊢ e ≫ e- (⇒ : τ) (⇒ a (~effs)) (⇒ r (~effs)) (⇒ f (~effs)) (⇒ s (~effs))] (... ...)
+           [⊢ e ≫ e- (⇒ : τ)] (... ...)
+           #:fail-unless (all-pure? #'(e- (... ...))) "expressions must be pure"
            ----------------------
            [⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...)))])
          (define-type-alias Alias AliasBody) ...)]))
@@ -626,7 +627,7 @@
 
 ;; DesugaredSyntax -> Bool
 (define-for-syntax (pure? e-)
-  (for/and ([key (in-list '(a r f s))])
+  (for/and ([key (in-list '(ep f s))])
     (effect-free? e- key)))
 
 ;; (SyntaxOf DesugaredSyntax ...) -> Bool
@@ -635,53 +636,83 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Core forms
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(define-typed-syntax (start-facet name:id ((~datum fields) [x:id τ-f:type e:expr] ...) ep ...+) ≫
+(define-typed-syntax (start-facet name:id ep ...+) ≫
+  #:with name- (syntax-local-identifier-as-binding (syntax-local-introduce (generate-temporary #'name)))
+  #:with name+ (syntax-local-identifier-as-binding #'name)
+  #:with facet-name-ty (type-eval #'FacetName)
+  #:do [(define ctx (syntax-local-make-definition-context))
+        (define unique (gensym 'start-facet))
+        (define name-- (internal-definition-context-introduce ctx #'name- 'add))
+        (syntax-local-bind-syntaxes (list #'name-) #f ctx)
+        (syntax-local-bind-syntaxes (list #'name+)
+                                    #'(make-rename-transformer
+                                       (add-orig (assign-type #'name- #'facet-name-ty #:wrap? #f) #'name))
+                                    ctx)
+        (define-values (rev-endpoints- endpoint-effects)
+          (for/fold ([rev-eps- '()]
+                     [effects '()])
+                    ([e (in-syntax #'(ep ...))])
+            (define ep- (local-expand e (list unique) (list #'erased) ctx))
+            (unless (and (effect-free? ep- 'f) (effect-free? ep- 's))
+              (type-error #:src e #:msg "only endpoint effects allowed"))
+            (define effects (or (syntax-property ep- 'ep) #'()))
+            (define more-effects
+              (syntax-parse effects
+                [((~or (~and MF ~MakesField)
+                       other-eff) ...)
+                 #:with (([x x- τ] ...) ...) (stx-map (lambda (stx) (syntax-local-introduce (syntax-property stx field-prop-name))) #'(MF ...))
+                 (for ([orig-name (in-syntax (stx-map syntax-local-identifier-as-binding #'(x ... ...)))]
+                       [new-name (in-syntax (stx-map syntax-local-identifier-as-binding #'(x- ... ...)))]
+                       [field-ty (in-syntax #'(τ ... ...))])
+                   (syntax-local-bind-syntaxes (list new-name) #f ctx)
+                   (syntax-local-bind-syntaxes (list orig-name)
+                                               #`(make-rename-transformer
+                                                  (add-orig (assign-type #'#,new-name #'#,field-ty #:wrap? #f) #'#,orig-name))
+                                               ctx))
+                 (syntax->list #'(other-eff ...))]))
+            (values (cons ep- rev-eps-)
+                    (append more-effects effects))))]
+  #:with ((~or (~and τ-a (~Shares _))
+              (~and τ-r (~Reacts _ ...)))
+          ...)
+         endpoint-effects
+  #:with τ (type-eval #`(Role (#,name--)
+                          τ-a ...
+                          τ-r ...))
+  --------------------------------------------------------------
+  [⊢ (syndicate:react (let- ([#,name-- (syndicate:current-facet-id)])
+                        #,@(reverse rev-endpoints-)))
+     (⇒ : ★/t)
+     (⇒ f (τ))])
+
+(define-typed-syntax (field [x:id τ-f:type e:expr] ...) ≫
   #:fail-unless (stx-andmap flat-type? #'(τ-f ...)) "keep your uppity data outta my fields"
   [⊢ e ≫ e- (⇐ : τ-f)] ...
   #:fail-unless (stx-andmap pure? #'(e- ...)) "field initializers not allowed to have effects"
-  [[name ≫ name- : FacetName] [x ≫ x- : (Field τ-f.norm)] ...
-   ⊢ [ep ≫ ep- (⇒ r (~effs τ-r ...))
-                (⇒ a (~effs τ-a ...))
-                (⇒ f (~effs))
-                (⇒ s (~effs))] ...]
-  #:with τ (type-eval #'(Role (name-)
-                          τ-a ... ...
-                          τ-r ... ...))
-  --------------------------------------------------------------
-  [⊢ (syndicate:react (let- ([name- (syndicate:current-facet-id)])
-                            #,(make-fields #'(x- ...) #'(e- ...))
-                            ep- ...))
+  #:with (x- ...) (generate-temporaries #'(x ...))
+  #:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
+  #:with MF (syntax-property (type-eval #'MakesField) field-prop-name (syntax-local-introduce #'([x x- τ] ...)))
+  ----------------------------------------------------------------------
+  [⊢ (syndicate:field [x- e-] ...)
      (⇒ : ★/t)
-     (⇒ r ())
-     (⇒ a ())
-     (⇒ s ())
-     (⇒ f (τ))])
-
-(define-for-syntax (make-fields names inits)
-  (syntax-parse #`(#,names #,inits)
-    [((x:id ...) (e ...))
-     #'(syndicate:field [x e] ...)]))
+     (⇒ ep (MF))])
 
 (define-typed-syntax (assert e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"
+  #:with τs (type-eval #'(Shares τ))
   -------------------------------------
   [⊢ (syndicate:assert e-) (⇒ : ★/t)
-                           (⇒ a ((Shares τ)))
-                           (⇒ r ())
-                           (⇒ f ())
-                           (⇒ s ())])
+                           (⇒ ep (τs))])
 
 (define-typed-syntax (stop facet-name:id cont ...) ≫
   [⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
-  [⊢ (begin #f cont ...) ≫ cont- (⇒ a (~effs)) (⇒ r (~effs)) (⇒ s (~effs)) (⇒ f (~effs τ-f ...))]
+  [⊢ (begin #f cont ...) ≫ cont- (⇒ ep (~effs)) (⇒ s (~effs)) (⇒ f (~effs τ-f ...))]
   #:with τ (mk-Stop- #`(facet-name- τ-f ...))
   ---------------------------------------------------------------------------------
   [⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
-                                              (⇒ s ())
-                                              (⇒ a ())
-                                              (⇒ r ())
                                               (⇒ f (τ))])
 
 (begin-for-syntax
@@ -696,48 +727,36 @@
 
 (define-typed-syntax on
   [(on (~literal start) s ...) ≫
-   [⊢ (begin s ...) ≫ s- (⇒ a (~effs))
-                          (⇒ r (~effs))
+   [⊢ (begin s ...) ≫ s- (⇒ ep (~effs))
                           (⇒ f (~effs τ-f ...))
                           (⇒ s (~effs τ-s ...))]
-   #:with τ-r #'(Reacts OnStart τ-f ... τ-s ...)
+   #:with τ-r (type-eval #'(Reacts OnStart τ-f ... τ-s ...))
    -----------------------------------
    [⊢ (syndicate:on-start s-) (⇒ : ★/t)
-      (⇒ a ())
-      (⇒ r (τ-r))
-      (⇒ f ())
-      (⇒ s ())]]
+      (⇒ ep (τ-r))]]
   [(on (~literal stop) s ...) ≫
-   [⊢ (begin s ...) ≫ s- (⇒ a (~effs))
-                          (⇒ r (~effs))
+   [⊢ (begin s ...) ≫ s- (⇒ ep (~effs))
                           (⇒ f (~effs τ-f ...))
                           (⇒ s (~effs τ-s ...))]
-   #:with τ-r #'(Reacts OnStop τ-f ... τ-s ...)
+   #:with τ-r (type-eval #'(Reacts OnStop τ-f ... τ-s ...))
    -----------------------------------
    [⊢ (syndicate:on-stop s-) (⇒ : ★/t)
-      (⇒ a ())
-      (⇒ r (τ-r))
-      (⇒ f ())
-      (⇒ s ())]]
+      (⇒ ep (τ-r))]]
   [(on (a/r:asserted-or-retracted p) s ...) ≫
    [⊢ p ≫ p-- (⇒ : τp)]
    #:fail-unless (pure? #'p--) "pattern not allowed to have effects"
    #:with ([x:id τ:type] ...) (pat-bindings #'p)
    [[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s-
-                 (⇒ a (~effs))
-                 (⇒ r (~effs))
+                 (⇒ ep (~effs))
                  (⇒ f (~effs τ-f ...))
                  (⇒ s (~effs τ-s ...))]
    #:with p- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'p))
-   #:with τ-r #'(Reacts (a/r.react-con τp) τ-f ... τ-s ...)
+   #:with τ-r (type-eval #'(Reacts (a/r.react-con τp) τ-f ... τ-s ...))
    -----------------------------------
    [⊢ (syndicate:on (a/r.syndicate-kw p-)
                     s-)
       (⇒ : ★/t)
-      (⇒ r (τ-r))
-      (⇒ f ())
-      (⇒ a ())
-      (⇒ s ())]])
+      (⇒ ep (τ-r))]])
 
 ;; pat -> ([Id Type] ...)
 (define-for-syntax (pat-bindings stx)
@@ -793,7 +812,7 @@
 (define-typed-syntax (spawn τ-c:type s) ≫
   #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
   ;; TODO: check that each τ-f is a Role
-  [⊢ s ≫ s- (⇒ a (~effs)) (⇒ r (~effs)) (⇒ s (~effs)) (⇒ f (~effs τ-f ...))]
+  [⊢ s ≫ s- (⇒ ep (~effs)) (⇒ s (~effs)) (⇒ f (~effs τ-f ...))]
   ;; TODO: s shouldn't refer to facets or fields!
   #:with (τ-i τ-o τ-a) (analyze-roles #'(τ-f ...))
   #:fail-unless (<: #'τ-o #'τ-c.norm)
@@ -807,14 +826,11 @@
   #:with τ-final (type-eval #'(Actor τ-c.norm))
   --------------------------------------------------------------------------------------------
   [⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
-                                               (⇒ s (τ-final))
-                                               (⇒ a ())
-                                               (⇒ r ())
-                                               (⇒ f ())])
+                                               (⇒ s (τ-final))])
 
 (define-typed-syntax (dataspace τ-c:type s ...) ≫
   #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
-  [⊢ s ≫ s- (⇒ a (~effs)) (⇒ r (~effs)) (⇒ s (~effs τ-s ...)) (⇒ f (~effs))] ...
+  [⊢ s ≫ s- (⇒ ep (~effs)) (⇒ s (~effs τ-s ...)) (⇒ f (~effs))] ...
   #:with τ-actor (type-eval #'(Actor τ-c.norm))
   #:fail-unless (stx-andmap (lambda (t) (<: t #'τ-actor)) #'(τ-s ... ...))
                 "Not all actors conform to communication type"
@@ -823,10 +839,7 @@
   #:with τ-relay (relay-interests #'τ-c.norm)
   -----------------------------------------------------------------------------------
   [⊢ (syndicate:dataspace s- ...) (⇒ : ★/t)
-                                  (⇒ s ((Actor (U τ-ds-i τ-ds-o τ-relay))))
-                                  (⇒ a ())
-                                  (⇒ r ())
-                                  (⇒ f ())])
+                                  (⇒ s ((Actor (U τ-ds-i τ-ds-o τ-relay))))])
 
 (define-typed-syntax (set! x:id e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
@@ -845,7 +858,6 @@
   ----------------------------------------
   [≻ (on (asserted p)
          (start-facet during-inner
-           (fields)
            (on (retracted inst-p)
                (stop during-inner))
            s ...))])
@@ -874,27 +886,26 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (define-typed-syntax (ref x:id) ≫
+  ;; #:do [(printf "reference info ~a\n" (syntax-debug-info #'x))]
   [⊢ x ≫ x- ⇒ (~Field τ)]
+  ;; #:do [(printf "~a ≫ ~a\n" #'x #'x-)]
   ------------------------
   [⊢ (x-) (⇒ : τ)])
 
 (define-typed-syntax (lambda ([x:id (~optional (~datum :)) τ:type] ...) body ...+) ≫
   [[x ≫ x- : τ] ... ⊢ (begin body ...) ≫ body- (⇒ : τ-e)
-                (⇒ a (~effs τ-a ...))
-                (⇒ r (~effs τ-r ...))
+                (⇒ ep (~effs τ-ep ...))
                 (⇒ s (~effs τ-s ...))
                 (⇒ f (~effs τ-f ...))]
   ----------------------------------------
   [⊢ (lambda- (x- ...) body-) (⇒ : (→ τ ... (Computation (Value τ-e)
-                                                         (Asserts τ-a ...)
-                                                         (Reactions τ-r ...)
+                                                         (EndPoints τ-ep ...)
                                                          (Roles τ-f ...)
                                                          (Spawns τ-s ...))))])
 
 (define-typed-syntax (typed-app e_fn e_arg ...) ≫
   [⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in ... (~Computation (~Value τ-out)
-                                                  (~Asserts τ-a ...)
-                                                  (~Reactions τ-r ...)
+                                                  (~Endpoints τ-ep ...)
                                                   (~Roles τ-f ...)
                                                   (~Spawns τ-s ...))))]
   #:fail-unless (pure? #'e_fn-) "expression not allowed to have effects"
@@ -904,8 +915,7 @@
   #:fail-unless (stx-andmap pure? #'(e_arg- ...)) "expressions not allowed to have effects"
   ------------------------------------------------------------------------
   [⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ-out)
-     (⇒ a (τ-a ...))
-     (⇒ r (τ-r ...))
+     (⇒ ep (τ-ep ...))
      (⇒ s (τ-s ...))
      (⇒ f (τ-f ...))])
 
@@ -996,8 +1006,7 @@
    --------
    [≻ (begin-
         (define-typed-variable-rename f ≫ f- : (→ ty ... (Compuation (Value ty_out)
-                                                                     (Asserts)
-                                                                     (Reactions)
+                                                                     (Endpoints)
                                                                      (Roles)
                                                                      (Spawns))))
         (define- f-
@@ -1010,27 +1019,25 @@
    [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
    #:fail-unless (pure? #'e_tst-) "expression must be pure"
    [⊢ e1 ≫ e1- (⇐ : τ-expected)
-      (⇒ a (~effs as1 ...)) (⇒ r (~effs rs1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))]
+      (⇒ ep (~effs eps1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))]
    [⊢ e2 ≫ e2- (⇐ : τ-expected)
-      (⇒ a (~effs as2 ...)) (⇒ r (~effs rs2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
+      (⇒ ep (~effs eps2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
    --------
    [⊢ (if- e_tst- e1- e2-)
-      (⇒ a (as1 ... as2 ...))
-      (⇒ r (rs1 ... rs2 ...))
+      (⇒ ep (eps1 ... eps2 ...))
       (⇒ f (fs1 ... fs2 ...))
       (⇒ s (ss1 ... ss2 ...))]]
   [(_ e_tst e1 e2) ≫
    [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
    #:fail-unless (pure? #'e_tst-) "expression must be pure"
    [⊢ e1 ≫ e1- (⇒ : τ1)
-      (⇒ a (~effs as1 ...)) (⇒ r (~effs rs1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))]
+      (⇒ ep (~effs eps1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))]
    [⊢ e2 ≫ e2- (⇒ : τ2)
-      (⇒ a (~effs as2 ...)) (⇒ r (~effs rs2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
+      (⇒ ep (~effs eps2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
    #:with τ (type-eval #'(U τ1 τ2))
    --------
    [⊢ (if- e_tst- e1- e2-) (⇒ : τ)
-      (⇒ a (as1 ... as2 ...))
-      (⇒ r (rs1 ... rs2 ...))
+      (⇒ ep (eps1 ... eps2 ...))
       (⇒ f (fs1 ... fs2 ...))
       (⇒ s (ss1 ... ss2 ...))]])
 
@@ -1038,24 +1045,22 @@
 (define-typed-syntax begin
   [(_ e_unit ... e) ⇐ τ_expected ≫
    [⊢ e_unit ≫ e_unit- (⇒ : _)
-      (⇒ a (~effs as1 ...)) (⇒ r (~effs rs1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))] ...
+      (⇒ ep (~effs eps1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))] ...
    [⊢ e ≫ e- (⇐ : τ_expected)
-      (⇒ a (~effs as2 ...)) (⇒ r (~effs rs2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
+      (⇒ ep (~effs eps2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
    --------
    [⊢ (begin- e_unit- ... e-)
-      (⇒ a (as1 ... ... as2 ...))
-      (⇒ r (rs1 ... ... rs2 ...))
+      (⇒ ep (eps1 ... ... eps2 ...))
       (⇒ f (fs1 ... ... fs2 ...))
       (⇒ s (ss1 ... ... ss2 ...))]]
   [(_ e_unit ... e) ≫
    [⊢ e_unit ≫ e_unit- (⇒ : _)
-      (⇒ a (~effs as1 ...)) (⇒ r (~effs rs1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))] ...
+      (⇒ ep (~effs eps1 ...)) (⇒ f (~effs fs1 ...)) (⇒ s (~effs ss1 ...))] ...
    [⊢ e ≫ e- (⇒ : τ_e)
-      (⇒ a (~effs as2 ...)) (⇒ r (~effs rs2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
+      (⇒ ep (~effs eps2 ...)) (⇒ f (~effs fs2 ...)) (⇒ s (~effs ss2 ...))]
    --------
    [⊢ (begin- e_unit- ... e-) (⇒ : τ_e)
-      (⇒ a (as1 ... ... as2 ...))
-      (⇒ r (rs1 ... ... rs2 ...))
+      (⇒ ep (eps1 ... ... eps2 ...))
       (⇒ f (fs1 ... ... fs2 ...))
       (⇒ s (ss1 ... ... ss2 ...))]])
 
@@ -1065,28 +1070,24 @@
    [⊢ e ≫ e- ⇒ : τ_x] ...
    #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
    [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇐ : τ_expected)
-                   (⇒ a (~effs as ...))
-                   (⇒ r (~effs rs ...))
+                   (⇒ ep (~effs eps ...))
                    (⇒ f (~effs fs ...))
                    (⇒ s (~effs ss ...))]
    ----------------------------------------------------------
    [⊢ (let- ([x- e-] ...) e_body-)
-      (⇒ a (as ...))
-      (⇒ r (rs ...))
+      (⇒ ep (eps ...))
       (⇒ f (fs ...))
       (⇒ s (ss ...))]]
   [(_ ([x e] ...) e_body ...) ≫
    [⊢ e ≫ e- ⇒ : τ_x] ...
    #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
    [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- (⇒ : τ_body)
-                   (⇒ a (~effs as ...))
-                   (⇒ r (~effs rs ...))
+                   (⇒ ep (~effs eps ...))
                    (⇒ f (~effs fs ...))
                    (⇒ s (~effs ss ...))]
    ----------------------------------------------------------
    [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body)
-      (⇒ a (as ...))
-      (⇒ r (rs ...))
+      (⇒ ep (eps ...))
       (⇒ f (fs ...))
       (⇒ s (ss ...))]])
 
@@ -1103,14 +1104,12 @@
   [⊢ pred ≫ pred- (⇐ : Bool)] ...
   #:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure"
   [⊢ (begin s ...) ≫ s- (⇒ : τ-s)
-                   (⇒ a (~effs as ...))
-                   (⇒ r (~effs rs ...))
+                   (⇒ ep (~effs eps ...))
                    (⇒ f (~effs fs ...))
                    (⇒ s (~effs ss ...))] ...
   ------------------------------------------------
   [⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...))
-     (⇒ a (as ... ...))
-     (⇒ r (rs ... ...))
+     (⇒ ep (eps ... ...))
      (⇒ f (fs ... ...))
      (⇒ s (ss ... ...))])
 
@@ -1119,8 +1118,7 @@
   #:fail-unless (pure? #'e-) "expression must be pure"
   #:with (([x τ] ...) ...) (stx-map pat-bindings #'(p ...))
   [[x ≫ x- : τ] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s)
-                (⇒ a (~effs as ...))
-                (⇒ r (~effs rs ...))
+                (⇒ ep (~effs eps ...))
                 (⇒ f (~effs fs ...))
                 (⇒ s (~effs ss ...))] ...
   ;; REALLY not sure how to handle p/p-/p.match-pattern,
@@ -1136,8 +1134,7 @@
   [⊢ (match- e- [p- s-] ...
                 [_ (error "incomplete pattern match")])
      (⇒ : (U τ-s ...))
-     (⇒ a (as ... ...))
-     (⇒ r (rs ... ...))
+     (⇒ ep (eps ... ...))
      (⇒ f (fs ... ...))
      (⇒ s (ss ... ...))])
 
@@ -1146,17 +1143,17 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;; hmmm
-(define-primop + (→ Int Int (Computation (Value Int) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop - (→ Int Int (Computation (Value Int) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop * (→ Int Int (Computation (Value Int) (Asserts) (Reactions) (Roles) (Spawns))))
+(define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
+(define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
+(define-primop * (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
 #;(define-primop and (→ Bool Bool Bool))
-(define-primop or (→ Bool Bool (Computation (Value Bool) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop not (→ Bool (Computation (Value Bool) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop < (→ Int Int (Computation (Value Bool) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop > (→ Int Int (Computation (Value Bool) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop <= (→ Int Int (Computation (Value Bool) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop >= (→ Int Int (Computation (Value Bool) (Asserts) (Reactions) (Roles) (Spawns))))
-(define-primop = (→ Int Int (Computation (Value Bool) (Asserts) (Reactions) (Roles) (Spawns))))
+(define-primop or (→ Bool Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop not (→ Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop < (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop > (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
 
 (define-typed-syntax (/ e1 e2) ≫
   [⊢ e1 ≫ e1- (⇐ : Int)]
@@ -1215,17 +1212,17 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (define-typed-syntax (print-type e) ≫
-  [⊢ e ≫ e- (⇒ : τ) (⇒ a as) (⇒ r rs) (⇒ f es)]
+  [⊢ e ≫ e- (⇒ : τ) (⇒ ep (~effs eps ...)) (⇒ f (~effs fs ...)) (⇒ s (~effs ss ...))]
   #:do [(displayln (type->str #'τ))]
   ----------------------------------
-  [⊢ e- (⇒ : τ) (⇒ a as) (⇒ r rs) (⇒ f es)])
+  [⊢ e- (⇒ : τ) (⇒ ep (eps ...)) (⇒ f (fs ...)) (⇒ s (ss ...))])
 
 (define-typed-syntax (print-role e) ≫
-  [⊢ e ≫ e- (⇒ : τ) (⇒ a as) (⇒ r rs) (⇒ f es)]
-  #:do [(for ([r (in-syntax #'es)])
+  [⊢ e ≫ e- (⇒ : τ) (⇒ ep (~effs eps ...)) (⇒ f (~effs fs ...)) (⇒ s (~effs ss ...))]
+  #:do [(for ([r (in-syntax #'(fs ...))])
           (displayln (type->str r)))]
   ----------------------------------
-  [⊢ e- (⇒ : τ) (⇒ a as) (⇒ r rs) (⇒ f es)])
+  [⊢ e- (⇒ : τ) (⇒ ep (eps ...)) (⇒ f (fs ...)) (⇒ s (ss ...))])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Lists
@@ -1259,15 +1256,13 @@
   [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] ...
   #:fail-unless (all-pure? #'(e-list- ...)) "expressions must be pure"
   [[x ≫ x- : τ-l] ... ⊢ (begin e-body ...) ≫ e-body- (⇒ : τ-b)
-                  (⇒ a (~effs as ...))
-                  (⇒ r (~effs rs ...))
+                  (⇒ ep (~effs eps ...))
                   (⇒ f (~effs fs ...))
                   (⇒ s (~effs ss ...))]
   -------------------------------------------------------
   [⊢ (for- ([x- (in-list- e-list-)] ...)
        e-body-) (⇒ : ★/t)
-                (⇒ a (as ...))
-                (⇒ r (rs ...))
+                (⇒ ep (eps ...))
                 (⇒ f (fs ...))
                 (⇒ s (ss ...))])