diff --git a/racket/typed/examples/roles/bank-account.rkt b/racket/typed/examples/roles/bank-account.rkt index 4ca998f..45bfb4c 100644 --- a/racket/typed/examples/roles/bank-account.rkt +++ b/racket/typed/examples/roles/bank-account.rkt @@ -22,6 +22,15 @@ (Observe DepositRequest) (Observe (Observe DepositRequest)))) +(define-type-alias account-manager-role + (Role (account-manager) + (Shares Account) + (Reacts (Know (Deposit Int))))) + +(define-type-alias client-role + (Role (client) + (Reacts (Know Account)))) + (dataspace ds-type (spawn ds-type diff --git a/racket/typed/examples/roles/book-club.rkt b/racket/typed/examples/roles/book-club.rkt index 070cd0f..0f83ace 100644 --- a/racket/typed/examples/roles/book-club.rkt +++ b/racket/typed/examples/roles/book-club.rkt @@ -53,6 +53,13 @@ (select 1 item) stock))) +(define-type-alias seller-role + (Role (seller) + (Reacts (Know (Observe (BookQuoteT String ★/t))) + (Role (_) + ;; nb no mention of retracting this assertion + (Shares (BookQuoteT String Int)))))) + (define (spawn-seller [inventory : Inventory]) (spawn τc (start-facet seller @@ -63,8 +70,38 @@ ;; TODO - lookup (assert (book-quote title (lookup title (ref books)))))))) +(define-type-alias leader-role + (Role (leader) + (Reacts (Know (BookQuoteT String Int)) + (Role (poll) + (Reacts (Know (BookInterestT String String Bool)) + ;; this is actually implemented indirectly through dataflow + (U (Stop leader + (Role (_) + (Shares (BookOfTheMonthT String)))) + (Stop poll))))))) + +(define-type-alias leader-actual + (Role (get-quotes31) + (Reacts (Know (BookQuoteT String (Bind Int))) + (Stop get-quotes) + (Role (poll-members36) + (Reacts OnDataflow + (Stop poll-members + (Stop get-quotes)) + (Stop get-quotes + (Role (announce39) + (Shares (BookOfTheMonthT String))))) + (Reacts (¬Know (BookInterestT String (Bind String) Bool))) + (Reacts (Know (BookInterestT String (Bind String) Bool))) + (Reacts (¬Know (BookInterestT String (Bind String) Bool))) + (Reacts (Know (BookInterestT String (Bind String) Bool))))) + (Reacts (¬Know (ClubMemberT (Bind String)))) + (Reacts (Know (ClubMemberT (Bind String)))))) + (define (spawn-leader [titles : (List String)]) (spawn τc + (print-role (start-facet get-quotes (field [book-list (List String) (rest titles)] [title String (first titles)]) @@ -103,8 +140,16 @@ (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)))))]))))) + (stop poll-members (next-book)))))])))))) +(define-type-alias member-role + (Role (member) + (Shares (ClubMemberT String)) + ;; should this be the type of the pattern? or lowered to concrete types? + (Reacts (Know (Observe (BookInterestT String ★/t ★/t))) + (Role (_) + (Shares (BookInterestT String String Bool)))))) + (define (spawn-club-member [name : String] [titles : (List String)]) (spawn τc diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 4efff58..9664b19 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -475,6 +475,13 @@ ;; should probably put this first. [_ (type=? t1 t2)])) +;; shortcuts for mapping +(define-for-syntax ((<:l l) r) + (<: l r)) + +(define-for-syntax ((<:r r) l) + (<: l r)) + ;; Flat-Type Flat-Type -> Type (define-for-syntax (∩ t1 t2) (unless (and (flat-type? t1) (flat-type? t2)) @@ -610,6 +617,244 @@ (finite? #'τ)] [_ #t])) +;; PatternType -> Type +(define-for-syntax (pattern-matching-assertions t) + (syntax-parse t + [(~Bind τ) + #'τ] + [~Discard + (type-eval #'★/t)] + [(~U* τ ...) + (type-eval #`(U #,@(stx-map pattern-matching-assertions #'(τ ...))))] + [(~Tuple τ ...) + (type-eval #`(Tuple #,@(stx-map pattern-matching-assertions #'(τ ...))))] + [(~Observe τ) + (type-eval #`(Observe #,(pattern-matching-assertions #'τ)))] + [(~Inbound τ) + (type-eval #`(Inbound #,(pattern-matching-assertions #'τ)))] + [(~Outbound τ) + (type-eval #`(Outbound #,(pattern-matching-assertions #'τ)))] + [(~constructor-type _ τ ...) + (make-cons-type t (stx-map pattern-matching-assertions #'(τ ...)))] + [_ t])) + +;; it's ok for x to respond to strictly more events than y +(define-for-syntax (condition-covers? x y) + (or + ;; covers Start,Stop,Dataflow + (type=? x y) + (syntax-parse #`(#,x #,y) + [((~Know τ1) (~Know τ2)) + (<: (pattern-matching-assertions #'τ2) + (pattern-matching-assertions #'τ1))] + [((~¬Know τ1) (¬Know τ2)) + (<: (pattern-matching-assertions #'τ2) + (pattern-matching-assertions #'τ1))] + [_ #f]))) + +;; RoleType RoleType -> Bool +;; Check that role r implements role spec (possibly does more) +(define-for-syntax (role-implements? r spec) + (syntax-parse #`(#,r #,spec) + ;; TODO: cases for unions, stop + [((~Role (x:id) (~or (~Shares τ-s1) (~Reacts τ-if1 τ-then1 ...)) ...) + (~Role (y:id) (~or (~Shares τ-s2) (~Reacts τ-if2 τ-then2 ...)) ...)) + #:when (free-identifier=? #'x #'y) + (and + ;; for each assertion in the spec, there must be a suitable assertion in the actual + ;; TODO: this kinda ignores numerosity, can one assertion in r cover multiple assertions in spec? + (for/and [(s2 (in-syntax #'(τ-s2 ...)))] + (stx-ormap (<:l s2) #'(τ-s1 ...))) + (for/and [(s2 (in-syntax #'((τ-if2 (τ-then2 ...)) ...)))] + (define/syntax-parse (τ-if2 (τ-then2 ...)) s2) + (for/or [(s1 (in-syntax #'((τ-if1 (τ-then1 ...)) ...)))] + (define/syntax-parse (τ-if1 (τ-then1 ...)) s1) + ;; the event descriptors need to line up + (and (condition-covers? #'τ-if1 #'τ-if2) + ;; and for each specified response to the event, there needs to be a similar one in the + ;; the actual + (stx-andmap (lambda (s) (stx-ormap (lambda (r) (role-implements? r s)) #'(τ-then1 ...))) + #'(τ-then2 ...))))))] + [((~Role (x:id) _ ...) + (~Role (y:id) _ ...)) + (role-implements? (subst #'y #'x r) spec)] + [((~Stop x:id τ1 ...) + (~Stop y:id τ2 ...)) + (and + (free-identifier=? #'x #'y) + (for/and ([t2 (in-syntax #'(τ2 ...))]) + (for/or ([t1 (in-syntax #'(τ1 ...))]) + (role-implements? t1 t2))))] + [((~Actor _) + (~Actor _)) + ;; spawned actor OK in specified dataspace + (<: r spec)])) + +(module+ test + (begin-for-syntax + ;; TESTS + (let () + ;; utils + (local-require syntax/parse/define + rackunit) + (define te type-eval) + (define-syntax-parser check-role-implements? + [(_ r1 r2) + (quasisyntax/loc this-syntax + (check-true (role-implements? (te #'r1) (te #'r2))))]) + (define-syntax-parser check-role-not-implements? + [(_ r1 r2) + (quasisyntax/loc this-syntax + (check-false (role-implements? (te #'r1) (te #'r2))))]) + ;; Name Related + (check-role-implements? (Role (x)) (Role (x))) + (check-role-implements? (Role (x)) (Role (y))) + ;; Assertion Related + (check-role-not-implements? (Role (x)) (Role (y) (Shares Int))) + (check-role-implements? (Role (x) (Shares Int)) (Role (y))) + (check-role-implements? (Role (x) (Shares Int)) (Role (y) (Shares Int))) + (check-role-implements? (Role (x) + (Shares Int) + (Shares String)) + (Role (y) + (Shares Int) + (Shares String))) + (check-role-implements? (Role (x) + (Shares String) + (Shares Int)) + (Role (y) + (Shares Int) + (Shares String))) + (check-role-not-implements? (Role (x) + (Shares Int)) + (Role (y) + (Shares Int) + (Shares String))) + ;; Reactions + (check-role-implements? (Role (x) + (Reacts (Know Int))) + (Role (y) + (Reacts (Know Int)))) + (check-role-implements? (Role (x) + (Reacts (Know Int)) + (Shares String)) + (Role (y) + (Reacts (Know Int)))) + (check-role-implements? (Role (x) + (Reacts (Know Int) + (Role (y) (Shares String)))) + (Role (y) + (Reacts (Know Int)))) + (check-role-not-implements? (Role (x)) + (Role (y) + (Reacts (Know Int)))) + (check-role-not-implements? (Role (x) + (Reacts (Know String))) + (Role (y) + (Reacts (Know Int)))) + ;; these two might need to be reconsidered + (check-role-not-implements? (Role (x) + (Shares (Observe ★/t))) + (Role (y) + (Reacts (Know Int)))) + (check-role-not-implements? (Role (x) + (Shares (Observe Int))) + (Role (y) + (Reacts (Know Int)))) + (check-role-implements? (Role (x) + (Reacts (Know Int) + (Role (x2) (Shares String)))) + (Role (y) + (Reacts (Know Int) + (Role (y2) (Shares String))))) + (check-role-implements? (Role (x) + (Reacts (¬Know Int) + (Role (x2) (Shares String)))) + (Role (y) + (Reacts (¬Know Int) + (Role (y2) (Shares String))))) + (check-role-implements? (Role (x) + (Reacts OnStart + (Role (x2) (Shares String)))) + (Role (y) + (Reacts OnStart + (Role (y2) (Shares String))))) + (check-role-implements? (Role (x) + (Reacts OnStop + (Role (x2) (Shares String)))) + (Role (y) + (Reacts OnStop + (Role (y2) (Shares String))))) + (check-role-implements? (Role (x) + (Reacts OnDataflow + (Role (x2) (Shares String)))) + (Role (y) + (Reacts OnDataflow + (Role (y2) (Shares String))))) + (check-role-not-implements? (Role (x) + (Reacts (Know Int) + (Role (x2) (Shares String)))) + (Role (y) + (Reacts (Know Int) + (Role (y2) (Shares String)) + (Role (y3) (Shares Int))))) + (check-role-implements? (Role (x) + (Reacts (Know Int) + (Role (x3) (Shares Int)) + (Role (x2) (Shares String)))) + (Role (y) + (Reacts (Know Int) + (Role (y2) (Shares String)) + (Role (y3) (Shares Int))))) + ;; also not sure about this one + (check-role-implements? (Role (x) + (Reacts (Know Int) + (Role (x2) + (Shares String) + (Shares Int)))) + (Role (y) + (Reacts (Know Int) + (Role (y2) (Shares String)) + (Role (y3) (Shares Int))))) + ;; Stop + ;; these all error when trying to create the Stop type :< +#| + (check-role-implements? (Role (x) + (Reacts OnStart (Stop x))) + (Role (x) + (Reacts OnStart (Stop x)))) + (check-role-implements? (Role (x) + (Reacts OnStart (Stop x))) + (Role (y) + (Reacts OnStart (Stop y)))) + (check-role-implements? (Role (x) + (Reacts OnStart (Stop x (Role (x2) (Shares Int))))) + (Role (y) + (Reacts OnStart (Stop y) (Role (y2) (Shares Int))))) + (check-role-not-implements? (Role (x) + (Reacts OnStart (Stop x (Role (x2) (Shares String))))) + (Role (y) + (Reacts OnStart (Stop y) (Role (y2) (Shares Int))))) + (check-role-not-implements? (Role (x) + (Reacts OnStart)) + (Role (y) + (Reacts OnStart (Stop y) (Role (y2) (Shares Int))))) +|# + ;; Spawning Actors + (check-role-implements? (Role (x) + (Reacts OnStart (Actor Int))) + (Role (x) + (Reacts OnStart (Actor Int)))) + (check-role-implements? (Role (x) + (Reacts OnStart (Actor Int))) + (Role (x) + (Reacts OnStart (Actor (U Int String))))) + (check-role-not-implements? (Role (x) + (Reacts OnStart (Actor Bool))) + (Role (x) + (Reacts OnStart (Actor (U Int String))))) + ))) + ;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ;; MODIFYING GLOBAL TYPECHECKING STATE!!!!! ;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! @@ -1083,7 +1328,7 @@ #:fail-unless (pure? #'e-) "expression must be pure" #:with x- (generate-temporary #'x) -------- - [⊢ (define/intermediate x x- τ.norm e-) (⇒ : ★/t)]] + [⊢ (define/intermediate #,(syntax-local-identifier-as-binding #'x) x- τ.norm e-) (⇒ : ★/t)]] [(_ x:id e) ≫ ;This won't work with mutually recursive definitions [⊢ e ≫ e- ⇒ τ]