From 9a3d921de3c9f66299a79a2aa03cbcf1382bfb90 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Wed, 2 May 2018 13:20:59 -0400 Subject: [PATCH] starter for typed/syndicate/core --- racket/typed/core.rkt | 865 ++++++++++++++++++ racket/typed/examples/core/box-and-client.rkt | 33 + racket/typed/main.rkt | 5 + racket/typed/syndicate/core/lang/reader.rkt | 2 + 4 files changed, 905 insertions(+) create mode 100644 racket/typed/core.rkt create mode 100644 racket/typed/examples/core/box-and-client.rkt create mode 100644 racket/typed/syndicate/core/lang/reader.rkt diff --git a/racket/typed/core.rkt b/racket/typed/core.rkt new file mode 100644 index 0000000..9f9de84 --- /dev/null +++ b/racket/typed/core.rkt @@ -0,0 +1,865 @@ +#lang turnstile + +(provide (rename-out [syndicate:#%module-begin #%module-begin]) + (rename-out [typed-app #%app]) + (rename-out [syndicate:begin-for-declarations declare-types]) + #%top-interaction + require only-in + ;; Types + Int Bool String Tuple Bind Discard → ★/t + Observe Inbound Outbound Actor U + Event AssertionSet Patch Instruction + ;; Core Forms + actor dataspace make-assertion-set project ★ patch + tuple lambda observe inbound outbound + quit transition patch-added patch-removed + ;; values + #%datum + ;; patterns + bind discard + ;; primitives + + - * / and or not > < >= <= = equal? displayln + ;; making types + define-type-alias + define-constructor + ;; DEBUG and utilities + print-type + (rename-out [printf- printf]) + ;; Extensions + ) + +(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx)) + +(require (rename-in racket/match [match-lambda match-lambda-])) +(require (rename-in racket/math [exact-truncate exact-truncate-])) +(require (rename-in racket/set [set->list set->list-])) +(require (prefix-in syndicate: syndicate/core-lang) + (prefix-in syndicate: syndicate/trie) + (prefix-in syndicate: syndicate/comprehensions)) + +(module+ test + (require rackunit) + (require turnstile/rackunit-typechecking)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Needed Forms +;; * dataspace DONE +;; * actor DONE +;; * make-assertion-set DONE +;; - ★ DONE +;; * patch DONE +;; * project DONE +;; - bind +;; - discard +;; * transition DONE +;; * quit DONE +;; * fold DONE +;; * list DONE + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Types + +(define-base-types Int Bool String Discard ★/t) + +(define-type-constructor Bind #:arity = 1) +(define-type-constructor Tuple #:arity >= 0) +(define-type-constructor U #:arity >= 0) +(define-type-constructor → #:arity > 0) +(define-type-constructor Observe #:arity = 1) +(define-type-constructor Inbound #:arity = 1) +(define-type-constructor Outbound #:arity = 1) +(define-type-constructor Actor #:arity = 1) +(define-type-constructor AssertionSet #:arity = 1) +(define-type-constructor Patch #:arity = 2) +(define-type-constructor List #:arity = 1) +;; essentially the sum type of a transition or quit +(define-type-constructor Instruction #:arity = 3) + +(define-for-syntax (type-eval t) + ((current-type-eval) t)) + +(begin-for-syntax + (define-syntax ~U/no-order + (pattern-expander + (syntax-parser + [(_ p ...) + #:fail-when (stx-ormap (lambda [x] (and (identifier? x) + (free-identifier=? x #'(... ...)))) + #'(p ...)) + "ellipses not allowed" + #:with ((v ...) ...) (permutations (stx->list #'(p ...))) + #'(~or* (~U v ...) ...)])))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; User Defined Types, aka Constructors + +;; τ.norm in 1st case causes "not valid type" error when file is compiled +;; (copied from ext-stlc example) +(define-syntax define-type-alias + (syntax-parser + [(_ alias:id τ:any-type) + #'(define-syntax- alias + (make-variable-like-transformer #'τ.norm))] + [(_ (f:id x:id ...) ty) + #'(define-syntax- (f stx) + (syntax-parse stx + [(_ x ...) + #:with τ:any-type #'ty + #'τ.norm]))])) + +(begin-for-syntax + (define-splicing-syntax-class type-constructor-decl + (pattern (~seq #:type-constructor TypeCons:id)) + (pattern (~seq) #:attr TypeCons #f)) + + (struct user-ctor (typed-ctor untyped-ctor) + #:property prop:procedure + (lambda (v stx) + (define transformer (user-ctor-typed-ctor v)) + (syntax-parse stx + [(_ e ...) + #`(#,transformer e ...)])))) + +(define-syntax (define-constructor stx) + (syntax-parse stx + [(_ (Cons:id slot:id ...) + ty-cons:type-constructor-decl + (~seq #:with + Alias AliasBody) ...) + #:with TypeCons (or (attribute ty-cons.TypeCons) (format-id stx "~a/t" (syntax-e #'Cons))) + #:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons) + #:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons) + #:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons) + #:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons) + #:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons)) + (define arity (stx-length #'(slot ...))) + #`(begin- + (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent) + (define-syntax (TypeConsExtraInfo stx) + (syntax-parse stx + [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)])) + (define-type-constructor TypeCons + #:arity = #,arity + #:extra-info 'TypeConsExtraInfo) + (define-syntax (MakeTypeCons stx) + (syntax-parse stx + [(_ t (... ...)) + #:fail-unless (= #,arity (stx-length #'(t (... ...)))) "arity mismatch" + #'(TypeCons t (... ...))])) + (define-syntax (GetTypeParams stx) + (syntax-parse stx + [(_ (TypeConsExpander t (... ...))) + #'(t (... ...))])) + (define-syntax Cons + (user-ctor #'Cons- #'StructName)) + (define-typed-syntax (Cons- e (... ...)) ≫ + #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch" + [⊢ e ≫ e- (⇒ : τ)] (... ...) + ---------------------- + [⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...)))]) + (define-type-alias Alias AliasBody) ...)])) + +(begin-for-syntax + (define-syntax ~constructor-extra-info + (pattern-expander + (syntax-parser + [(_ tag mk get) + #'(_ (_ tag) (_ mk) (_ get))]))) + + (define-syntax ~constructor-type + (pattern-expander + (syntax-parser + [(_ tag . rst) + #'(~and it + (~fail #:unless (user-defined-type? #'it)) + (~parse tag (get-type-tag #'it)) + (~Any _ . rst))]))) + + (define-syntax ~constructor-exp + (pattern-expander + (syntax-parser + [(_ cons . rst) + #'(~and (cons . rst) + (~fail #:unless (ctor-id? #'cons)))]))) + + (define (inspect t) + (syntax-parse t + [(~constructor-type tag t ...) + (list (syntax-e #'tag) (stx-map type->str #'(t ...)))])) + + (define (tags-equal? t1 t2) + (equal? (syntax-e t1) (syntax-e t2))) + + (define (user-defined-type? t) + (get-extra-info (type-eval t))) + + (define (get-type-tag t) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info tag _ _) + (syntax-e #'tag)])) + + (define (get-type-args t) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info _ _ get) + (define f (syntax-local-value #'get)) + (syntax->list (f #`(get #,t)))])) + + (define (make-cons-type t args) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info _ mk _) + (define f (syntax-local-value #'mk)) + (type-eval (f #`(mk #,@args)))])) + + (define (ctor-id? stx) + (and (identifier? stx) + (user-ctor? (syntax-local-value stx (const #f))))) + + (define (untyped-ctor stx) + (user-ctor-untyped-ctor (syntax-local-value stx (const #f))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Conveniences + +(define-type-alias (Action τ-a τ-s) + (U (Patch τ-a ★/t) (Actor τ-s))) + +(begin-for-syntax + (define-syntax ~Action + (pattern-expander + (syntax-parser + [(_ p1 p2) + #'(~U/no-order (~Patch p1 _) (~Actor p2))])))) + +(define-type-alias (Event τ) + (Patch τ τ)) + +#;(begin-for-syntax + (define-syntax ~Event + (pattern-expander + (syntax-parser + [(_ t) + #`(~and (~Patch τ1:type τ2:type) + (~parse t #,(type-eval #'(U τ1 τ2))))])))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Syntax + +(begin-for-syntax + + ;; constructors with arity one + (define-syntax-class kons1 + (pattern (~or (~datum observe) + (~datum inbound) + (~datum outbound)))) + + (define (kons1->constructor stx) + (syntax-parse stx + #:datum-literals (observe inbound outbound) + [observe #'syndicate:observe] + [inbound #'syndicate:inbound] + [outbound #'syndicate:outbound])) + + (define-syntax-class basic-val + (pattern (~or boolean + integer + string))) + + (define-syntax-class prim-op + (pattern (~or (~literal +) + (~literal -) + (~literal displayln))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Subtyping + +;; Type Type -> Bool +(define-for-syntax (<: t1 t2) + #;(printf "Checking ~a <: ~a\n" (type->str t1) (type->str t2)) + ;; should add a check for type=? + (syntax-parse #`(#,t1 #,t2) + #;[(τ1 τ2) #:do [(displayln (type->str #'τ1)) + (displayln (type->str #'τ2))] + #:when #f + (error "")] + [((~U τ1 ...) _) + (stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))] + [(_ (~U τ2:type ...)) + (stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))] + [((~Actor τ1:type) (~Actor τ2:type)) + ;; should these be .norm? Is the invariant that inputs are always fully + ;; evalutated/expanded? + (and (<: #'τ1 #'τ2) + (<: (∩ (strip-? #'τ1) #'τ2) #'τ1))] + [((~AssertionSet τ1) (~AssertionSet τ2)) + (<: #'τ1 #'τ2)] + [((~Patch τ11 τ12) (~Patch τ21 τ22)) + (and (<: #'τ11 #'τ21) + (<: #'τ12 #'τ22))] + [((~Instruction τs1 τo1 τa1) (~Instruction τs2 τo2 τa2)) + (and (<: #'τs1 #'τs2) + (<: #'τo1 #'τo2) + (<: (type-eval #'(Actor τa1)) (type-eval #'(Actor τa2))))] + [((~Tuple τ1:type ...) (~Tuple τ2:type ...)) + #:when (stx-length=? #'(τ1 ...) #'(τ2 ...)) + (stx-andmap <: #'(τ1 ...) #'(τ2 ...))] + [(_ ~★/t) + (flat-type? t1)] + [((~Observe τ1:type) (~Observe τ2:type)) + (<: #'τ1 #'τ2)] + [((~Inbound τ1:type) (~Inbound τ2:type)) + (<: #'τ1 #'τ2)] + [((~Outbound τ1:type) (~Outbound τ2:type)) + (<: #'τ1 #'τ2)] + [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...)) + #:when (tags-equal? #'t1 #'t2) + (and (stx-length=? #'(τ1 ...) #'(τ2 ...)) + (stx-andmap <: #'(τ1 ...) #'(τ2 ...)))] + [((~→ τ-in1 ... τ-out1) (~→ τ-in2 ... τ-out2)) + #:when (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...)) + (and (stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...)) + (<: #'τ-out1 #'τ-out2))] + [(~Discard _) + #t] + ;; should probably put this first. + [_ (type=? t1 t2)])) + +(define-for-syntax (bot? t) + (<: t (type-eval #'(U)))) + +;; Flat-Type Flat-Type -> Type +(define-for-syntax (∩ t1 t2) + (unless (and (flat-type? t1) (flat-type? t2)) + (error '∩ "expected two flat-types")) + (syntax-parse #`(#,t1 #,t2) + [(_ ~★/t) + t1] + [(~★/t _) + t2] + [(_ _) + #:when (type=? t1 t2) + t1] + [((~U τ1:type ...) _) + (type-eval #`(U #,@(stx-map (lambda (t) (∩ t t2)) #'(τ1 ...))))] + [(_ (~U τ2:type ...)) + (type-eval #`(U #,@(stx-map (lambda (t) (∩ t1 t)) #'(τ2 ...))))] + [((~AssertionSet τ1) (~AssertionSet τ2)) + #:with τ12 (∩ #'τ1 #'τ2) + (type-eval #'(AssertionSet τ12))] + [((~Patch τ11 τ12) (~Patch τ21 τ22)) + #:with τ1 (∩ #'τ11 #'τ12) + #:with τ2 (∩ #'τ21 #'τ22) + (type-eval #'(Patch τ1 τ2))] + [((~Instruction τs1 τo1 τa1) (~Instruction τs2 τo2 τa2)) + #:with τs (∩ #'τs1 #'τs2) + #:fail-when (bot? #'τs) #f + #:with τa (∩ #'τa1 #'τa2) + #:fail-when (bot? #'τa) #f + #:with τo (∩ #'τo1 #'τo2) + (type-eval #'(Instruction τs τo τa))] + ;; all of these fail-when/unless clauses are meant to cause this through to + ;; the last case and result in ⊥. + ;; Also, using <: is OK, even though <: refers to ∩, because <:'s use of ∩ is only + ;; in the Actor case. + [((~Tuple τ1:type ...) (~Tuple τ2:type ...)) + #:fail-unless (stx-length=? #'(τ1 ...) #'(τ2 ...)) #f + #:with (τ ...) (stx-map ∩ #'(τ1 ...) #'(τ2 ...)) + ;; I don't think stx-ormap is part of the documented api of turnstile *shrug* + #:fail-when (stx-ormap (lambda (t) (<: t (type-eval #'(U)))) #'(τ ...)) #f + (type-eval #'(Tuple τ ...))] + [((~constructor-type tag1 τ1:type ...) (~constructor-type tag2 τ2:type ...)) + #:when (tags-equal? #'tag1 #'tag2) + #:with (τ ...) (stx-map ∩ #'(τ1 ...) #'(τ2 ...)) + #:fail-when (stx-ormap (lambda (t) (<: t (type-eval #'(U)))) #'(τ ...)) #f + (make-cons-type t1 #'(τ ...))] + ;; these three are just the same :( + [((~Observe τ1:type) (~Observe τ2:type)) + #:with τ (∩ #'τ1 #'τ2) + #:fail-when (<: #'τ (type-eval #'(U))) #f + (type-eval #'(Observe τ))] + [((~Inbound τ1:type) (~Inbound τ2:type)) + #:with τ (∩ #'τ1 #'τ2) + #:fail-when (<: #'τ (type-eval #'(U))) #f + (type-eval #'(Inbound τ))] + [((~Outbound τ1:type) (~Outbound τ2:type)) + #:with τ (∩ #'τ1 #'τ2) + #:fail-when (<: #'τ (type-eval #'(U))) #f + (type-eval #'(Outbound τ))] + [_ (type-eval #'(U))])) + +;; Type Type -> Bool +;; first type is the contents of the set +;; second type is the type of a pattern +(define-for-syntax (project-safe? t1 t2) + (syntax-parse #`(#,t1 #,t2) + [(_ (~Bind τ2:type)) + (and (finite? t1) (<: t1 #'τ2))] + [(_ ~Discard) + #t] + [(_ ~★/t) + #t] + [((~U τ1:type ...) _) + (stx-andmap (lambda (t) (project-safe? t t2)) #'(τ1 ...))] + [(_ (~U τ2:type ...)) + (stx-andmap (lambda (t) (project-safe? t1 t)) #'(τ2 ...))] + [((~Tuple τ1:type ...) (~Tuple τ2:type ...)) + #:when (overlap? t1 t2) + (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))] + [((~constructor-type _ τ1:type ...) (~constructor-type _ τ2:type ...)) + #:when (overlap? t1 t2) + (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))] + [((~Observe τ1:type) (~Observe τ2:type)) + (project-safe? #'τ1 #'τ2)] + [((~Inbound τ1:type) (~Inbound τ2:type)) + (project-safe? #'τ1 #'τ2)] + [((~Outbound τ1:type) (~Outbound τ2:type)) + (project-safe? #'τ1 #'τ2)] + [_ #t])) + +;; AssertionType PatternType -> Bool +;; Is it possible for things of these two types to match each other? +;; Flattish-Type = Flat-Types + ★/t, Bind, Discard (assertion and pattern types) +(define-for-syntax (overlap? t1 t2) + (syntax-parse #`(#,t1 #,t2) + [(~★/t _) #t] + [(_ (~Bind _)) #t] + [(_ ~Discard) #t] + [(_ ~★/t) #t] + [((~U τ1:type ...) _) + (stx-ormap (lambda (t) (overlap? t t2)) #'(τ1 ...))] + [(_ (~U τ2:type ...)) + (stx-ormap (lambda (t) (overlap? t1 t)) #'(τ2 ...))] + [((~List _) (~List _)) + ;; share the empty list + #t] + [((~Tuple τ1:type ...) (~Tuple τ2:type ...)) + (and (stx-length=? #'(τ1 ...) #'(τ2 ...)) + (stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))] + [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...)) + (and (tags-equal? #'t1 #'t2) + (stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))] + [((~Observe τ1:type) (~Observe τ2:type)) + (overlap? #'τ1 #'τ2)] + [((~Inbound τ1:type) (~Inbound τ2:type)) + (overlap? #'τ1 #'τ2)] + [((~Outbound τ1:type) (~Outbound τ2:type)) + (overlap? #'τ1 #'τ2)] + [_ (<: t1 t2)])) + + +;; Flattish-Type -> Bool +(define-for-syntax (finite? t) + (syntax-parse t + [~★/t #f] + [(~U τ:type ...) + (stx-andmap finite? #'(τ ...))] + [(~Tuple τ:type ...) + (stx-andmap finite? #'(τ ...))] + [(~constructor-type _ τ:type ...) + (stx-andmap finite? #'(τ ...))] + [(~Observe τ:type) + (finite? #'τ)] + [(~Inbound τ:type) + (finite? #'τ)] + [(~Outbound τ:type) + (finite? #'τ)] + [_ #t])) + +;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! +;; MODIFYING GLOBAL TYPECHECKING STATE!!!!! +;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + +(begin-for-syntax + (current-typecheck-relation <:)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Core forms + +(define-typed-syntax (actor τ-c:type beh st0 as0) ≫ + #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order" + [⊢ beh ≫ beh- ⇒ (~→ (~Patch τ-i1:type τ-i2:type) + τ-s:type + (~Instruction τ-s2:type τ-ta:type τ-ts:type))] + [⊢ st0 ≫ st0- ⇒ τ-st0:type] + [⊢ as0 ≫ as0- ⇒ (~AssertionSet τ-as0:type)] + #:with τ-out:type (type-eval #'(U τ-ta τ-as0)) + #:with τ-in:type (type-eval #'(U τ-i1 τ-i2)) + #:fail-unless (<: #'τ-st0.norm #'τ-s.norm) + "bad initial state" + #:fail-unless (<: #'τ-s2.norm #'τ-s.norm) + "bad state update" + #:fail-unless (<: #'τ-out.norm #'τ-c.norm) + "output not allowed in dataspace" + #:fail-unless (<: (type-eval #'(Actor τ-ts.norm)) + (type-eval #'(Actor τ-c.norm))) + "spawned actors not valid in dataspace" + #:fail-unless (<: (∩ (strip-? #'τ-out.norm) #'τ-c.norm) #'τ-in.norm) + "Not prepared to handle all inputs" + -------------------------------------------------------------------------------------------- + [⊢ (syndicate:actor beh- st0- (list- (syndicate:patch as0- syndicate:trie-empty))) + ⇒ (Actor τ-c)]) + +(define-typed-syntax (dataspace τ-c:type e) ≫ + #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order" + [⊢ e ≫ e- ⇒ (~List τa:type)] + #:fail-unless (<: #'τa.norm (type-eval #'(Actor τ-c.norm))) + "Not all actors conform to communication type" + #:with τ-ds-i (strip-inbound #'τ-c.norm) + #:with τ-ds-o (strip-outbound #'τ-c.norm) + #:with τ-relay (relay-interests #'τ-c.norm) + ----------------------------------------------------------------------------------- + [⊢ (syndicate:dataspace e-) ⇒ (Actor (U τ-ds-i τ-ds-o τ-relay))]) + +(define-typed-syntax (transition e-s e-as) ≫ + [⊢ e-s ≫ e-s- ⇒ τ-s] + [⊢ e-as ≫ e-as- ⇒ (~List (~Action τ-o τ-a))] + ----------------------------------------- + [⊢ (syndicate:transition e-s- e-as-) ⇒ (Instruction τ-s τ-o τ-a)]) + +(define-typed-syntax quit + [(quit) ≫ + ------------------------------------- + [⊢ (syndicate:quit) ⇒ (Instruction (U) (U) (U))]] + [(quit as) ≫ + [⊢ as ≫ as- ⇒ (~List (~Action τ-o τ-a))] + ---------------------------------------- + [⊢ (syndicate:quit as-) ⇒ (Instruction (U) τ-o τ-a)]]) + +(define-typed-syntax ★ + [_ ≫ + ------------------------- + [⊢ syndicate:? ⇒ ★/t]]) + +(define-typed-syntax (make-assertion-set e ...) ≫ + [⊢ e ≫ e- ⇒ τ] ... + #:fail-unless (stx-andmap flat-type? #'(τ ...)) + "assertions must be first-order" + ------------------------------------------------- + [⊢ (syndicate:trie-union-all (list- (syndicate:pattern->trie 'typed e-) ...)) + ⇒ (AssertionSet (U τ ...))]) + +(define-typed-syntax (patch e-add e-sub) ≫ + [⊢ e-add ≫ e-add- ⇒ (~AssertionSet τ-add)] + [⊢ e-sub ≫ e-sub- ⇒ (~AssertionSet τ-sub)] + -------------------------------------------- + [⊢ (syndicate:patch e-add- e-sub-) ⇒ (Patch τ-add τ-sub)]) + +(define-typed-syntax (project [pat e-set] e-body) ≫ + [⊢ e-set ≫ e-set- ⇒ (~AssertionSet τ-s:type)] + [⊢ pat ≫ _ ⇒ τ-p:type] + #:with ([x:id τ:type] ...) (pat-bindings #'pat) + [[x ≫ x- : τ] ... ⊢ e-body ≫ e-body- ⇒ τ-b] + #:fail-unless (project-safe? #'τ-s.norm #'τ-p.norm) + "pattern captures infinite set" + #:with pat- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'pat)) + -------------------------------------------------------- + [⊢ (syndicate:for-trie/list ([pat- e-set-]) + e-body-) + ⇒ (List τ-b)]) + +(begin-for-syntax + (define (compile-pattern pat bind-id-transformer exp-transformer) + (define (l-e stx) (local-expand stx 'expression '())) + (let loop ([pat pat]) + (syntax-parse pat + #:datum-literals (tuple discard bind) + [(tuple p ...) + #`(list- 'tuple #,@(stx-map loop #'(p ...)))] + [(k:kons1 p) + #`(#,(kons1->constructor #'k) #,(loop #'p))] + [(bind x:id τ:type) + (bind-id-transformer #'x)] + [discard + #'_] + [(~constructor-exp ctor p ...) + (define/with-syntax uctor (untyped-ctor #'ctor)) + #`(uctor #,@(stx-map loop #'(p ...)))] + [_ + ;; local expanding "expression-y" syntax allows variable references to transform + ;; according to the mappings set up by turnstile. + (exp-transformer (l-e pat))]))) + + (define (compile-syndicate-pattern pat) + (compile-pattern pat + (lambda (id) #`($ #,id)) + identity))) + +(define-typed-syntax (list e ...) ≫ + [⊢ e ≫ e- ⇒ τ] ... + ------------------- + [⊢ (list- e- ...) ⇒ (List (U τ ...))]) + +(define-typed-syntax (for/fold [acc:id e-acc] + [x:id e-list] + e-body) ≫ + [⊢ e-list ≫ e-list- ⇒ (~List τ-l)] + [⊢ e-acc ≫ e-acc- ⇒ τ-a:type] + [[x ≫ x- : τ-l] [acc ≫ acc- : τ-a] ⊢ e-body ≫ e-body- ⇒ τ-b:type] + #:fail-unless (<: #'τ-b.norm #'τ-a.norm) + "loop body doesn't match accumulator" + ------------------------------------------------------- + [⊢ (for/fold- ([acc- e-acc-]) + ([x- (in-list- e-list-)]) + e-body-) + ⇒ τ-b]) + +(define-for-syntax (strip-? t) + (type-eval + (syntax-parse t + ;; TODO: probably need to `normalize` the result + [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))] + [~★/t #'★/t] + [(~Observe τ) #'τ] + [_ #'(U)]))) + +(define-for-syntax (strip-inbound t) + (type-eval + (syntax-parse t + ;; TODO: probably need to `normalize` the result + [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))] + [~★/t #'★/t] + [(~Inbound τ) #'τ] + [_ #'(U)]))) + +(define-for-syntax (strip-outbound t) + (type-eval + (syntax-parse t + ;; TODO: probably need to `normalize` the result + [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))] + [~★/t #'★/t] + [(~Outbound τ) #'τ] + [_ #'(U)]))) + +(define-for-syntax (relay-interests t) + (type-eval + (syntax-parse t + ;; TODO: probably need to `normalize` the result + [(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))] + [~★/t #'★/t] + [(~Observe (~Inbound τ)) #'(Observe τ)] + [_ #'(U)]))) + +(define-for-syntax (procedure-type? τ) + (syntax-parse τ + [(~→ τ ...+) #t] + [_ #f])) + +(define-for-syntax (flat-type? τ) + (syntax-parse τ + [(~→ τ ...) #f] + [_ #t])) + +(define-typed-syntax (unsafe-do rkt:expr ...) ≫ + ------------------------ + [⊢ (let- () rkt ...) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Expressions + +(define-typed-syntax (lambda ([x:id (~optional (~literal :)) τ:type] ...) e) ≫ + [[x ≫ x- : τ] ... ⊢ e ≫ e- ⇒ τ-e] + ---------------------------------------- + [⊢ (lambda- (x- ...) e-) ⇒ (→ τ ... τ-e)]) + +(define-typed-syntax (tuple e:expr ...) ≫ + [⊢ e ≫ e- (⇒ : τ)] ... + ----------------------- + [⊢ (list- 'tuple e- ...) (⇒ : (Tuple τ ...))]) + +(define-typed-syntax (typed-app e_fn e_arg ...) ≫ + [⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in:type ... τ_out:type))] + #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) + (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) + [⊢ e_arg ≫ e_arg- ⇐ τ_in] ... + ------------------------------------------------------------------------ + [⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ_out)]) + +;; it would be nice to abstract over these three +(define-typed-syntax (observe e:expr) ≫ + [⊢ e ≫ e- (⇒ : τ)] + --------------------------------------------------------------------------- + [⊢ (syndicate:observe e-) (⇒ : (Observe τ))]) + +(define-typed-syntax (inbound e:expr) ≫ + [⊢ e ≫ e- ⇒ τ] + --------------------------------------------------------------------------- + [⊢ (syndicate:inbound e-) (⇒ : (Inbound τ))]) + +(define-typed-syntax (outbound e:expr) ≫ + [⊢ e ≫ e- ⇒ τ] + --------------------------------------------------------------------------- + [⊢ (syndicate:outbound e-) (⇒ : (Outbound τ))]) + +(define-typed-syntax (patch-added e) ≫ + [⊢ e ≫ e- ⇒ (~Patch τ _)] + -------------------------- + [⊢ (syndicate:patch-added e-) ⇒ (AssertionSet τ)]) + +(define-typed-syntax (patch-removed e) ≫ + [⊢ e ≫ e- ⇒ (~Patch _ τ)] + -------------------------- + [⊢ (syndicate:patch-removed e-) ⇒ (AssertionSet τ)]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Patterns + +(define-typed-syntax (bind x:id τ:type) ≫ + ---------------------------------------- + [⊢ (error- 'bind "escaped") ⇒ (Bind τ)]) + +(define-typed-syntax discard + [_ ≫ + -------------------- + ;; TODO: change void to _ + [⊢ (error- 'discard "escaped") ⇒ Discard]]) + +;; pat -> ([Id Type] ...) +(define-for-syntax (pat-bindings stx) + (syntax-parse stx + #:datum-literals (bind tuple) + [(bind x:id τ:type) + #'([x τ])] + [(tuple p ...) + #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) + #'([x τ] ... ...)] + [(k:kons1 p) + (pat-bindings #'p)] + [(~constructor-exp cons p ...) + #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) + #'([x τ] ... ...)] + [_ + #'()])) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Primitives + +;; hmmm +(define-primop + (→ Int Int Int)) +(define-primop - (→ Int Int Int)) +(define-primop * (→ Int Int Int)) +#;(define-primop and (→ Bool Bool Bool)) +(define-primop or (→ Bool Bool Bool)) +(define-primop not (→ Bool Bool)) +(define-primop < (→ Int Int Bool)) +(define-primop > (→ Int Int Bool)) +(define-primop <= (→ Int Int Bool)) +(define-primop >= (→ Int Int Bool)) +(define-primop = (→ Int Int Bool)) + +(define-typed-syntax (/ e1 e2) ≫ + [⊢ e1 ≫ e1- (⇐ : Int)] + [⊢ e2 ≫ e2- (⇐ : Int)] + ------------------------ + [⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int)]) + +;; for some reason defining `and` as a prim op doesn't work +(define-typed-syntax (and e ...) ≫ + [⊢ e ≫ e- (⇐ : Bool)] ... + ------------------------ + [⊢ (and- e- ...) (⇒ : Bool)]) + +(define-typed-syntax (equal? e1:expr e2:expr) ≫ + [⊢ e1 ≫ e1- (⇒ : τ1:type)] + #:fail-unless (flat-type? #'τ1.norm) + (format "equality only available on flat data; got ~a" (type->str #'τ1)) + [⊢ e2 ≫ e2- (⇐ : τ1)] + --------------------------------------------------------------------------- + [⊢ (equal?- e1- e2-) (⇒ : Bool)]) + +(define-typed-syntax (displayln e:expr) ≫ + [⊢ e ≫ e- ⇒ τ] + --------------- + [⊢ (displayln- e-) (⇒ : (U))]) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Basic Values + +(define-typed-syntax #%datum + [(_ . n:integer) ≫ + ---------------- + [⊢ (#%datum- . n) (⇒ : Int)]] + [(_ . b:boolean) ≫ + ---------------- + [⊢ (#%datum- . b) (⇒ : Bool)]] + [(_ . s:string) ≫ + ---------------- + [⊢ (#%datum- . s) (⇒ : String)]]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Utilities + +(define-typed-syntax (print-type e) ≫ + [⊢ e ≫ e- ⇒ τ] + #:do [(displayln (type->str #'τ))] + ---------------------------------- + [⊢ e- ⇒ τ]) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Extensions + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Tests + +;; project +(module+ test + + + (check-type (project [(tuple) (make-assertion-set (tuple 1 2))] + (tuple)) + : (List (Tuple)) + -> (list-)) + + (check-type (project [(tuple) (make-assertion-set (tuple))] + (tuple)) + : (List (Tuple)) + -> (list- (tuple))) + + (check-type (project [(tuple (bind x Int) 2) (make-assertion-set (tuple 1 2))] + x) + : (List Int) + -> (list- 1)) + + (check-type (project [(tuple (bind x Int) 2) (make-assertion-set (tuple 1 2) "hello")] + x) + : (List Int) + -> (list- 1)) + + (check-type (project [(tuple (bind x (U Int (Tuple Int Int))) 2) + (make-assertion-set (tuple 1 2) + "hello" + (tuple (tuple 4 5) 2))] + + x) + : (List (U Int (Tuple Int Int))) + -> (list- (tuple 4 5) 1)) + + ;; nested project to test for ambiguous binding error + (check-type (project [(tuple (bind x Int) 2) (make-assertion-set (tuple 1 2))] + (project [(tuple discard x) (make-assertion-set (tuple "bizboz" 1))] + x)) + : (List (List Int)) + -> (list- (list- 1)))) + +;; fold +(module+ test + (check-type (for/fold (sum 0) + (x (list 1 2 3)) + (typed-app + x sum)) + : Int + -> 6)) + +;; functions +(module+ test + (check-type (lambda ([x Int]) x) : (→ Int Int)) + (check-type (typed-app (lambda ([x : Int]) x) 5) + : Int + -> 5)) + +;; patches +(module+ test + (check-type (patch-added (patch (make-assertion-set 12) (make-assertion-set))) + : (AssertionSet Int) + -> (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 diff --git a/racket/typed/examples/core/box-and-client.rkt b/racket/typed/examples/core/box-and-client.rkt new file mode 100644 index 0000000..411d378 --- /dev/null +++ b/racket/typed/examples/core/box-and-client.rkt @@ -0,0 +1,33 @@ +#lang typed/syndicate/core + +(define-constructor (set-box new-value) + #:type-constructor SetBoxT + #:with SetBox (SetBoxT Int)) + +(define-constructor (box-state value) + #:type-constructor BoxStateT + #:with BoxState (BoxStateT Int)) + +(define-type-alias τ-c + (U BoxState + (Observe (BoxStateT ★/t)) + SetBox + (Observe (SetBoxT ★/t)))) + +(actor τ-c + (lambda ([e : (Event τ-c)] + [current-value : Int]) + (quit)) + 0 + (make-assertion-set (box-state 0) + (observe (set-box ★)))) + +#;(actor (lambda (e current-value) + (match-event e + [(message (set-box new-value)) + (log-info "box: taking on new-value ~v" new-value) + (transition new-value (patch-seq (retract (box-state current-value)) + (assert (box-state new-value))))])) + 0 + (patch-seq (sub (set-box ?)) + (assert (box-state 0)))) \ No newline at end of file diff --git a/racket/typed/main.rkt b/racket/typed/main.rkt index bb2a5f1..07b706f 100644 --- a/racket/typed/main.rkt +++ b/racket/typed/main.rkt @@ -62,6 +62,11 @@ (define-for-syntax (type-eval t) ((current-type-eval) t)) +;; this needs to be here until I stop 'compiling' patterns and just have them expand to the right +;; thing +(begin-for-syntax + (current-use-stop-list? #f)) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; User Defined Types, aka Constructors diff --git a/racket/typed/syndicate/core/lang/reader.rkt b/racket/typed/syndicate/core/lang/reader.rkt new file mode 100644 index 0000000..dceefd1 --- /dev/null +++ b/racket/typed/syndicate/core/lang/reader.rkt @@ -0,0 +1,2 @@ +#lang s-exp syntax/module-reader +typed/core