stlc.rkt (1169B)
1 #lang turnstile/lang 2 3 (provide (type-out →) λ #%app ann) 4 5 (define-type-constructor → #:arity >= 1 6 #:arg-variances (λ (stx) 7 (syntax-parse stx 8 [(_ τ_in ... τ_out) 9 (append 10 (make-list (stx-length #'[τ_in ...]) contravariant) 11 (list covariant))]))) 12 13 (define-typed-syntax λ #:datum-literals (:) 14 [(_ ([x:id : τ_in:type] ...) e) ≫ 15 [[x ≫ x- : τ_in.norm] ... ⊢ e ≫ e- ⇒ τ_out] 16 ------- 17 [⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]] 18 [(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫ 19 [[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out] 20 --------- 21 [⊢ (λ- (x- ...) e-)]]) 22 23 (define-typed-syntax (#%app e_fn e_arg ...) ≫ 24 [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)] 25 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 26 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 27 [⊢ e_arg ≫ e_arg- ⇐ τ_in] ... 28 -------- 29 [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out]) 30 31 (define-typed-syntax (ann e (~datum :) τ:type) ≫ 32 [⊢ e ≫ e- ⇐ τ.norm] 33 -------- 34 [⊢ e- ⇒ τ.norm])