sysf.rkt (559B)
1 #lang turnstile/lang 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 (Λ (tv:id ...) e) ≫ 17 [[tv ≫ tv- :: #%type] ... ⊢ e ≫ e- ⇒ τ] 18 -------- 19 [⊢ e- ⇒ (∀ (tv- ...) τ)]) 20 21 (define-typed-syntax inst 22 [(_ e τ:type ...) ≫ 23 [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)] 24 -------- 25 [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]] 26 [(_ e) ≫ --- [≻ e]]) 27