fsub.rkt (3204B)
1 #lang turnstile/lang 2 (extends "stlc+reco+sub.rkt" #:except +) 3 (require (rename-in (only-in "sysf.rkt" ∀? ∀ ~∀) [~∀ ~sysf:∀] [∀ sysf:∀])) 4 5 ;; System F<: 6 ;; Types: 7 ;; - types from sysf.rkt and stlc+reco+sub 8 ;; - extend ∀ with bounds 9 ;; Terms: 10 ;; - terms from sysf.rkt and stlc+reco+sub 11 ;; - extend Λ and inst 12 ;; - redefine + with Nat 13 ;; Other 14 ;; - current-promote, expose 15 ;; - extend current-sub? to call current-promote 16 17 (provide <: ∀ 18 (typed-out [+ : (→ Nat Nat Nat)]) 19 Λ inst) 20 21 ; can't just call expose in type-eval, 22 ; otherwise typevars will have bound as type, rather than instantiated type 23 ; only need expose during 24 ; 1) subtype checking 25 ; 2) pattern matching -- including base types 26 (begin-for-syntax 27 (define (expose t) 28 (cond [(identifier? t) 29 (define sub (detach t '<:)) 30 (if sub (expose sub) t)] 31 [else t])) 32 (current-promote expose) 33 (define stlc:sub? (current-sub?)) 34 (define (sub? t1 t2) 35 (stlc:sub? ((current-promote) t1) t2)) 36 (current-sub? sub?) 37 (current-typecheck-relation sub?)) 38 39 ; quasi-kind, but must be type constructor because its arguments are types 40 (define-type-constructor <: #:arity >= 0) 41 (begin-for-syntax 42 (current-type? (λ (t) (or (type? t) (<:? (typeof t)))))) 43 44 ;; Type annotations used in two places: 45 ;; 1) typechecking the body of 46 ;; 2) instantiation of ∀ 47 ;; Problem: need type annotations, even in expanded form 48 ;; Solution: store type annotations in a (quasi) kind <: 49 (define-typed-syntax (∀ ([tv:id (~datum <:) τ:type] ...) τ_body) ≫ 50 -------- 51 ; eval first to overwrite the old #%type 52 [⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ (<: τ.norm ...)]) 53 (begin-for-syntax 54 (define-syntax ~∀ 55 (pattern-expander 56 (syntax-parser #:datum-literals (<:) #:literals (...) 57 [(_ ([tv:id <: τ_sub] ooo:...) τ) 58 #'(~and ∀τ 59 (~parse (~sysf:∀ (tv ooo) τ) #'∀τ) 60 (~parse (~<: τ_sub ooo) (typeof #'∀τ)))] 61 [(_ . args) 62 #'(~and ∀τ 63 (~parse (~sysf:∀ (tv (... ...)) τ) #'∀τ) 64 (~parse (~<: τ_sub (... ...)) (typeof #'∀τ)) 65 (~parse args #'(([tv τ_sub] (... ...)) τ)))]))) 66 (define-syntax ~∀* 67 (pattern-expander 68 (syntax-parser #:datum-literals (<:) 69 [(_ . args) 70 #'(~or 71 (~∀ . args) 72 (~and any (~do 73 (type-error 74 #:src #'any 75 #:msg "Expected ∀ type, got: ~a" #'any))))])))) 76 77 (define-typed-syntax (Λ ([tv:id (~datum <:) τsub:type] ...) e) ≫ 78 ;; NOTE: store the subtyping relation of tv and τsub in the 79 ;; environment with a syntax property using another tag: '<: 80 ;; The "expose" function looks for this tag to enforce the bound, 81 ;; as in TaPL (fig 28-1) 82 [[tv ≫ tv- :: #%type <: τsub] ... ⊢ e ≫ e- ⇒ τ_e] 83 -------- 84 [⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)]) 85 (define-typed-syntax (inst e τ:type ...) ≫ 86 [⊢ e ≫ e- ⇒ (~∀ ([tv <: τ_sub] ...) τ_body)] 87 [τ.norm τ⊑ τ_sub #:for τ] ... 88 #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body) 89 -------- 90 [⊢ e- ⇒ τ_inst]) 91