add WritesField effect

racket/typed/examples/flink.rkt

@@ -479,8 +479,8 @@ The JobManager then performs the job and, when finished, asserts
          (log "JM begins on task ~a" this-id)
 
          ;; ID -> ...
-         (define (assign-task [mngr : ID]
-                              [request-again! : (→fn ★/t)])
+         (define (∀ (ρ) (assign-task [mngr : ID]
+                                     [request-again! : (proc -> ★/t #:effects (ρ))]))
            (start-facet assign
             (on (retracted (task-manager mngr _))
                 ;; our task manager has crashed

racket/typed/syndicate/core-types.rkt

@@ -459,13 +459,35 @@
 ;; sequence of effects
 (define-type-constructor Effs #:arity >= 0)
 (define-base-types OnStart OnStop OnDataflow)
+
 ;; (MakesField x τ)
 (define-type-constructor MakesField #:arity = 2)
+
 ;; (ReadsField x)
 (define-type-constructor ReadsField #:arity = 1)
-;; (VarAssert x [--> τ τ])
+;; need the original name so that we can re-typecheck an assert expression with
+;; different types for that name. Could also subst the original name in after
+;; constructing a valid type.
+(begin-for-syntax
+  (define RF-KEY 'ReadsField)
+  (define (mk-ReadsField x x-)
+    (attach (type-eval #`(ReadsField #,x-)) RF-KEY x))
+  (define (get-ReadsField-orig-field RF)
+    (detach RF RF-KEY)))
+
+;; (WritesField x τ)
+(define-type-constructor WritesField #:arity = 2)
+(begin-for-syntax
+  (define WF-KEY 'WritesField)
+  (define (mk-WritesField x x- t)
+    (attach (type-eval #`(WritesField #,x- #,t)) WF-KEY x))
+  (define (get-WritesField-orig-field WF)
+    (detach WF WF-KEY)))
+
+;; (VarAssert x [--> τ-field τ-assert])
 (define-type-constructor VarAssert #:arity > 1)
 (define-type-constructor --> #:arity = 2)
+
 (define-type-constructor Actor #:arity = 1)
 (define-type-constructor ActorWithRole #:arity >= 1)
 ;; usage: (ActorWithRole τc τr)
@@ -1280,6 +1302,9 @@
      (values bot bot bot (mk-Realize- #'(τ-m)) bot)]
     [(~Start _)
      (values bot bot bot bot bot)]
+    [(~or* (~ReadsField _)
+           (~WritesField _ _))
+     (values bot bot bot bot bot)]
     [(~WithFacets ([nm impl] ...) fst)
      (apply values (syntax->list (analyze-roles #'(impl ...))))]
     [(~Role+Body (_)
@@ -1292,11 +1317,14 @@
        ;; TODO - is this sub-role clause acutally needed?
        ;;(~and (~Role+Body _ _ ...) sub-role) ...
        )
-     #:with ((~or (~Shares τ-s)
-                  (~Know τ-k)
-                  #;(~Sends τ-m)
-                  #;(~Realizes τ-rlz)
-                  (~Reacts τ-if τ-then ...))
+     #:with ((~alt (~Shares τ-s)
+                   (~VarAssert _ [~--> _ τ-va] _ ...)
+                   (~Know τ-k)
+                   #;(~Sends τ-m)
+                   #;(~Realizes τ-rlz)
+                   (~Reacts τ-if τ-then ...)
+                   (~ReadsField _)
+                   (~WritesField _ _))
              ...) (flatten-effects #'(EP ...))
      ;; #:with (msg ...) (for/list ([m (in-syntax #'(τ-m ...))])
                         ;; (mk-Message- (list m)))
@@ -1315,7 +1343,7 @@
      (define pat-types/ext (map event-desc-type ifs/ext))
      (define pat-types/int (map event-desc-type ifs/int))
      (values (mk-U- #`(#,@is/e #,@pat-types/ext))
-             (mk-U- #`(τ-s ... #;msg #;... #,@os/e #,@(map pattern-sub-type pat-types/ext)))
+             (mk-U- #`(τ-s ... τ-va ... #;msg #;... #,@os/e #,@(map pattern-sub-type pat-types/ext)))
              (mk-U- #`(#,@is/i #,@pat-types/int))
              (mk-U- #`(τ-k ... #;rlz #;... #,@os/i #,@(map pattern-sub-type pat-types/int)))
              (mk-U- ss))]))

racket/typed/syndicate/roles.rkt

@@ -159,6 +159,9 @@
         (Know? eff)
         (Reacts? eff)
         (MakesField? eff)
+        (ReadsField? eff)
+        (WritesField? eff)
+        (VarAssert? eff)
         (row-variable? eff)))
 
   ;; Any -> Bool
@@ -170,6 +173,8 @@
         (Realizes? eff)
         (AnyActor? eff)
         (Start? eff)
+        (ReadsField? eff)
+        (WritesField? eff)
         (row-variable? eff)))
 
   (define endpoint-effects? (curry effects-andmap endpoint-effect?))
@@ -272,9 +277,18 @@
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"
   #:fail-unless (allowed-interest? #'τ) "overly broad interest, ?̱̱★ and ??★ not allowed"
   #:with τs (mk-Shares- #'(τ))
-  #:with kont (if (stx-null? #'(F ...))
-                  #'(just-assert e-)
-                  #'(type-varying-assert e e-))
+  #:with kont (syntax-parse #'(F ...)
+                [(~and ((~and RF (~ReadsField _)))
+                       #;(~do (displayln 0))
+                       (~parse x (get-ReadsField-orig-field #'RF))
+                       (~typecheck [⊢ x ≫ x- (⇒ : (~Field τ-f))])
+                       #;(~do (displayln 'B))
+                       (~parse (~and τ-U (~U* τ1 τ2)) (find-union #'τ-f)))
+                 #'(type-varying-assert e e- x x- τ-f τ-U)]
+                [_ #'(just-assert e-)])
+  ;; #:with kont (if (stx-null? #'(F ...))
+  ;;                 #'(just-assert e-)
+  ;;                 #'(type-varying-assert e e-))
   -------------------------------------
   [≻ kont])
 
@@ -287,20 +301,25 @@
      (⇒ ν (τs))])
 
 ;; need to make sure that the type has exactly one, binary union
-(define-typed-syntax (type-varying-assert e e-) ≫
-  #:with ((~ReadsField x)) (detach #'e- EFF-KEY)
+(define-typed-syntax (type-varying-assert e e- x x- τ-f τ-U) ≫
+  #:do [(displayln 'A)]
   #:with τe (detach #'e- ':)
-  [⊢ x ≫ x- (⇒ : (~Field τ))]
-  #:with (~and union (~U* τi ...)) (find-union #'τ)
+  #:do [(displayln 'B)]
+  #:with (~U* τi ...) #'τ-U
+  #:do [(displayln 'C)]
   #:with ((τ-specific τe_i) ...) (for/list ([ti (in-syntax #'(τi ...))])
-                      (define specific (type-subst #'union ti #'τ))
-                      (syntax-parse/typecheck null
-                        [_ ≫
-                           [[x ≫ _ : (Field #,specific)] ⊢ e ≫ _ (⇒ : τe_i)]
-                           --------------------
-                           [≻ (#,specific τe_i)]]))
+                                   (define specific (type-subst #'τ-U ti #'τ-f))
+                                   (syntax-parse/typecheck null
+                                     [_ ≫
+                                        ;; perhaps I should make sure the result is a subtype of the original?
+                                        [[x ≫ _ : (Field #,specific)] ⊢ e ≫ _ (⇒ : τe_i)]
+                                        ----------------------------------------
+                                        [≻ (#,specific τe_i)]]))
+  #:do [(displayln 'D)]
   [[x ≫ _ : Type] ⊢ x ≫ x--]
-  #:with VA (type-eval #`(VarAssert x-- [--> τ τe] [--> τ-specific τe_i] ...))
+  #:do [(displayln 'E)]
+  #:with VA (type-eval #`(VarAssert x-- [--> τ-f τe] [--> τ-specific τe_i] ...))
+  #:do [(pretty-display (type->strX #'VA))]
   -------------------------------------------------------------------------
   [⊢ (syndicate:assert e-)
      (⇒ : ★/t)
@@ -676,8 +695,10 @@
   [⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
   [⊢ x ≫ x- (⇒ : (~Field τ-x:type))]
   #:fail-unless (<: #'τ #'τ-x) "Ill-typed field write"
+  [[x- ≫ _ : Type] ⊢ x- ≫ x--]
+  #:with WF (mk-WritesField #'x #'x-- #'τ-x)
   ----------------------------------------------------
-  [⊢ (#%app- x- e-) (⇒ : ★/t) (⇒ ν (F ...))])
+  [⊢ (#%app- x- e-) (⇒ : ★/t) (⇒ ν (WF F ...))])
 
 (define-simple-macro (:= e ...)
   (set! e ...))
@@ -913,7 +934,7 @@
 (define-typed-syntax (ref x:id) ≫
   [⊢ x ≫ x- ⇒ (~Field τ)]
   [[x- ≫ _ : Type] ⊢ x- ≫ x--]
-  #:with RF (mk-ReadsField- #'(x--))
+  #:with RF (mk-ReadsField #'x #'x--)
   ------------------------
   [⊢ (#%app- x-)
      (⇒ : τ)