From 46a833a66ee67072d7fa085932eb76326b2ef1a4 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samcaldwell@utexas.edu>
Date: Mon, 14 May 2018 16:17:52 -0400
Subject: [PATCH] typed bank account

---
 racket/typed/core.rkt                       | 12 +++-
 racket/typed/examples/core/bank-account.rkt | 63 +++++++++++++++++++++
 2 files changed, 74 insertions(+), 1 deletion(-)
 create mode 100644 racket/typed/examples/core/bank-account.rkt

diff --git a/racket/typed/core.rkt b/racket/typed/core.rkt
index 9994c41..c85c975 100644
--- a/racket/typed/core.rkt
+++ b/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)))
\ No newline at end of file
+              -> (make-assertion-set)))
+
+(module+ test
+  (check-type (lambda ([e : (Event ⊥)]
+                       [s : ★/t])
+                idle)
+              : (→ (Event ⊥) ★/t (Instruction ⊥ ⊥ ⊥))))
\ No newline at end of file
diff --git a/racket/typed/examples/core/bank-account.rkt b/racket/typed/examples/core/bank-account.rkt
new file mode 100644
index 0000000..c70ca25
--- /dev/null
+++ b/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))
\ No newline at end of file