fsub.rkt (3218B)
1 #lang s-exp macrotypes/typecheck 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 (current-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 ∀ #:datum-literals (<:) 50 [(_ ([tv:id <: τ:type] ...) τ_body) 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 (<:) 57 [(_ ([tv:id <: τ_sub] ...) τ) 58 #'(~and ∀τ 59 (~parse (~sysf:∀ (tv ...) τ) #'∀τ) 60 (~parse (~<: τ_sub ...) (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 Λ #:datum-literals (<:) 78 [(_ ([X:id <: τsub:type] ...) e) 79 ;; NOTE: store the subtyping relation of tv and τsub in another 80 ;; "environment", ie, a syntax property with another tag: '<: 81 ;; The "expose" function looks for this tag to enforce the bound, 82 ;; as in TaPL (fig 28-1) 83 #:with ((X- ...) e- τ_e) (infer/ctx #'([X :: #%type <: τsub] ...) #'e) 84 (⊢ e- : (∀ ([X- <: τsub] ...) τ_e))]) 85 (define-typed-syntax inst 86 [(_ e τ:type ...) 87 #:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀) 88 #:when (typechecks? #'(τ.norm ...) #'(τ_sub ...)) 89 (⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))]) 90