sysf.rkt (536B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+lit.rkt") 3 4 ;; System F 5 ;; Types: 6 ;; - types from stlc+lit.rkt 7 ;; - ∀ 8 ;; Terms: 9 ;; - terms from stlc+lit.rkt 10 ;; - Λ and inst 11 12 (provide (type-out ∀) Λ inst) 13 14 (define-binding-type ∀) 15 16 (define-typed-syntax Λ 17 [(_ (tv:id ...) e) 18 #:with [tvs- e- τ-] (infer/ctx #'(tv ...) #'e) 19 (⊢ e- : (∀ tvs- τ-))]) 20 (define-typed-syntax inst 21 [(_ e τ:type ...) 22 #:with [e- (~∀ tvs τ_body)] (infer+erase #'e) 23 (⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))] 24 [(_ e) #'e])