typed bank account

racket/typed/core.rkt

@@ -9,10 +9,12 @@
          Int Bool String Tuple Bind Discard → ★/t
          Observe Inbound Outbound Actor U (type-out U*)
          Event AssertionSet Patch Instruction
+         ⊥
          ;; Core Forms
          actor dataspace make-assertion-set project ★ patch
          tuple lambda observe inbound outbound
          idle quit transition patch-added patch-removed
+         for/fold
          ;; core-ish forms
          begin define let let* ann if
          ;; values
@@ -268,6 +270,8 @@
         #`(~and (~Patch τ1:type τ2:type)
                 (~parse t #,(type-eval #'(U τ1 τ2))))]))))
 
+(define-type-alias ⊥ (U))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Syntax
 
@@ -1000,4 +1004,10 @@
               -> (make-assertion-set 12))
   (check-type (patch-removed (patch (make-assertion-set 12) (make-assertion-set)))
               : (AssertionSet (U))
-              -> (make-assertion-set)))
+              -> (make-assertion-set)))
+
+(module+ test
+  (check-type (lambda ([e : (Event ⊥)]
+                       [s : ★/t])
+                idle)
+              : (→ (Event ⊥) ★/t (Instruction ⊥ ⊥ ⊥))))

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))