lin+chan.rkt (1380B)
1 #lang turnstile/lang 2 (extends "lin+tup.rkt") 3 4 (provide (type-out InChan OutChan) 5 make-channel channel-put channel-get 6 thread sleep) 7 8 (define-type-constructor InChan #:arity = 1) 9 (define-type-constructor OutChan #:arity = 1) 10 11 (begin-for-syntax 12 (current-linear-type? (or/c InChan? (current-linear-type?)))) 13 14 15 (define-typed-syntax make-channel 16 [(_ {ty:type}) ≫ 17 #:with σ #'ty.norm 18 #:with tmp (generate-temporary) 19 -------- 20 [⊢ (let ([tmp (#%app- make-channel-)]) 21 (list tmp tmp)) 22 ⇒ (⊗ (InChan σ) (OutChan σ))]]) 23 24 25 (define-typed-syntax channel-put 26 [(_ ch e) ≫ 27 [⊢ ch ≫ ch- ⇒ (~OutChan σ)] 28 [⊢ e ≫ e- ⇐ σ] 29 -------- 30 [⊢ (channel-put- ch- e-) ⇒ Unit]]) 31 32 33 (define-typed-syntax channel-get 34 [(_ ch) ≫ 35 [⊢ ch ≫ ch- ⇒ (~InChan σ)] 36 #:with tmp (generate-temporary #'ch) 37 -------- 38 [⊢ (let ([tmp ch-]) 39 (list tmp (channel-get- tmp))) 40 ⇒ (⊗ (InChan σ) σ)]]) 41 42 43 (define-typed-syntax thread 44 [(_ f) ≫ 45 [⊢ f ≫ f- ⇒ (~-o _)] 46 -------- 47 [⊢ (void (thread- f-)) ⇒ Unit]]) 48 49 50 (define-typed-syntax sleep 51 [(_) ≫ 52 -------- 53 [⊢ (sleep-) ⇒ Unit]] 54 55 [(_ e) ≫ 56 [⊢ e ≫ e- ⇒ σ] 57 #:fail-unless (or (Int? #'σ) 58 (Float? #'σ)) 59 "invalid sleep time, expected Int or Float" 60 -------- 61 [⊢ (sleep- e-) ⇒ Unit]])