stlc.rkt (1228B)
1 #lang s-exp macrotypes/typecheck 2 3 ;; Simply-Typed Lambda Calculus 4 ;; - no base types; can't write any terms 5 ;; Types: multi-arg → (1+) 6 ;; Terms: 7 ;; - var 8 ;; - multi-arg λ (0+) 9 ;; - multi-arg #%app (0+) 10 11 (provide (type-out →) λ #%app) 12 13 (define-type-constructor → #:arity >= 1 14 #:arg-variances (λ (stx) 15 (syntax-parse stx 16 [(_ τ_in ... τ_out) 17 (append 18 (make-list (stx-length #'[τ_in ...]) contravariant) 19 (list covariant))]))) 20 21 (define-typed-syntax λ 22 [(_ bvs:type-ctx e) 23 #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e) 24 (⊢ (λ- xs- e-) : (→ bvs.type ... τ_res))]) 25 26 (define-typed-syntax #%app 27 [(_ e_fn e_arg ...) 28 #:with [e_fn- (~→ τ_in ... τ_out)] (infer+erase #'e_fn) 29 #:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...)) 30 #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...)) 31 (num-args-fail-msg #'e_fn #'(τ_in ...) #'(e_arg ...)) 32 #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) 33 (typecheck-fail-msg/multi 34 #'(τ_in ...) #'(τ_arg ...) #'(e_arg ...)) 35 (⊢/no-teval (#%app- e_fn- e_arg- ...) : τ_out)])