diff --git a/racket/typed/examples/roles/book-club.rkt b/racket/typed/examples/roles/book-club.rkt new file mode 100644 index 0000000..070cd0f --- /dev/null +++ b/racket/typed/examples/roles/book-club.rkt @@ -0,0 +1,129 @@ +#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 (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 (spawn-leader [titles : (List String)]) + (spawn τc + (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 (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)))))) + +(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"))) \ No newline at end of file diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index ffc5d9e..4efff58 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -12,12 +12,13 @@ Computation Value Endpoints Roles Spawns ;; Statements let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do + when unless ;; Derived Forms during define/query-value define/query-set ;; endpoints assert on field ;; expressions - tuple lambda ref observe inbound outbound + tuple select lambda ref observe inbound outbound ;; making types define-type-alias define-constructor @@ -28,7 +29,7 @@ ;; primitives + - * / and or not > < >= <= = equal? displayln printf define ;; lists - list first rest member? empty? for for/fold + list cons first rest member? empty? for for/fold ;; sets Set set set-member? set-add set-remove set-count set-union set-subtract set-intersect list->set set->list @@ -958,6 +959,7 @@ (on (retracted p) (set! x e0-)))]) +;; TODO: #:on-add (define-typed-syntax (define/query-set x:id p e) ≫ #:with ([y τ] ...) (pat-bindings #'p) ;; e will be re-expanded :/ @@ -985,7 +987,7 @@ (⇒ f (~effs τ-f ...))] ---------------------------------------- [⊢ (lambda- (x- ...) body-) (⇒ : (→ τ ... (Computation (Value τ-e) - (EndPoints τ-ep ...) + (Endpoints τ-ep ...) (Roles τ-f ...) (Spawns τ-s ...))))]) @@ -1069,7 +1071,10 @@ (define-syntax (define/intermediate stx) (syntax-parse stx [(_ x:id x-:id τ e) - #'(define- x- e)])) + ;; typed-variable-rename allows for using at module top level + #'(begin- + (define-typed-variable-rename x ≫ x- : τ) + (define- x- e))])) ;; copied from ext-stlc (define-typed-syntax define @@ -1086,17 +1091,25 @@ #:with x- (generate-temporary #'x) -------- [⊢ (define/intermediate x x- τ e-) (⇒ : ★/t)]] - [(_ (f [x (~optional (~datum :)) ty] ... - (~or (~datum →) (~datum ->)) ty_out) + [(_ (f [x (~optional (~datum :)) ty:type] ... + (~or (~datum →) (~datum ->)) ty_out:type) e ...+) ≫ [⊢ (lambda ([x : ty] ...) (begin e ...)) ≫ e- (⇒ : (~and fun-ty - (~Computation (~Value τ-v) - _ ...)))] - #:fail-unless (<: #'τ-v #'ty_out) - (format "expected different return type, got ~a" (type->str #'τ-v)) + (~→ (~not (~Computation _ ...)) ... + (~Computation (~Value τ-v) + _ ...))))] + #:fail-unless (<: #'τ-v #'ty_out.norm) + (format "expected different return type\n got ~a\n expected ~a\n" + #'τ-v #'ty_out + #;(type->str #'τ-v) + #;(type->str #'ty_out)) #:with f- (add-orig (generate-temporary #'f) #'f) -------- - [⊢ (define/intermediate f f- fun-ty e-) (⇒ : ★/t)]]) + [⊢ (define/intermediate f f- fun-ty e-) (⇒ : ★/t)]] + [(_ (f [x (~optional (~datum :)) ty] ...) + e ...+) ≫ + -------- + [≻ (define (f [x ty] ... -> ★/t) e ...)]]) ;; copied from ext-stlc (define-typed-syntax if @@ -1126,6 +1139,14 @@ (⇒ f (fs1 ... fs2 ...)) (⇒ s (ss1 ... ss2 ...))]]) +(define-typed-syntax (when e s ...+) ≫ + ------------------------------------ + [≻ (if e (begin s ...) #f)]) + +(define-typed-syntax (unless e s ...+) ≫ + ------------------------------------ + [≻ (if e #f (begin s ...))]) + ;; copied from ext-stlc (define-typed-syntax begin [(_ e_unit ... e) ≫ @@ -1307,6 +1328,15 @@ ------------------- [⊢ (list- e- ...) ⇒ (List (U τ ...))]) +(define-typed-syntax (cons e1 e2) ≫ + [⊢ e1 ≫ e1- ⇒ τ1] + #:fail-unless (pure? #'e1-) "expression must be pure" + [⊢ e2 ≫ e2- ⇒ (~List τ2)] + #:fail-unless (pure? #'e2-) "expression must be pure" + #:with τ-l (type-eval #'(List (U τ1 τ2))) + ---------------------------------------- + [⊢ (cons- e1- e2-) ⇒ τ-l]) + (define-typed-syntax (for/fold [acc:id e-acc] [x:id e-list] e-body ...+) ≫