fomega2.rkt (5464B)
1 #lang s-exp macrotypes/typecheck 2 (reuse Int + #:from "sysf.rkt") 3 (require (prefix-in sysf: (only-in "sysf.rkt" →- → #%app λ)) 4 (only-in "sysf.rkt" ~→ →?)) 5 (reuse define-type-alias String #%datum #:from "stlc+reco+var.rkt") 6 7 ; same as fomega.rkt except λ and #%app works as both type and terms, 8 ; - uses definition from stlc, but tweaks type? and kind? predicates 9 ;; → is also both type and kind 10 11 ;; System F_omega 12 ;; Type relation: 13 ;; Types: 14 ;; - types from sysf.rkt 15 ;; - String from stlc+reco+var 16 ;; Terms: 17 ;; - extend ∀ Λ inst from sysf 18 ;; - #%datum from stlc+reco+var 19 20 (provide (kind-out ★ ∀★) (type-out ∀) → λ #%app Λ inst 21 (for-syntax current-kind-eval kindcheck?)) 22 23 (define-syntax-category :: kind) 24 25 ;; modify predicates to recognize → (function type) as both type and kind 26 (begin-for-syntax 27 (define old-kind? (current-kind?)) 28 (current-kind? (λ (k) (or (#%type? k) (old-kind? k)))) 29 30 ;; well-formed types, eg not types with kind → 31 ;; must allow kinds as types, for → 32 (current-type? (λ (t) (define k (kindof t)) 33 (and k ((current-kind?) k) (not (→? k))))) 34 35 ;; o.w., a valid type is one with any valid kind 36 (current-any-type? (λ (t) (define k (kindof t)) 37 (and k ((current-kind?) k))))) 38 39 ;; extend → to serve as both type and kind 40 (define-syntax (→ stx) 41 (syntax-parse stx 42 [(_ k:kind ...) ; kind 43 (add-orig (mk-kind #'(sysf:→- k.norm ...)) stx)] 44 [(_ . tys) #'(sysf:→ . tys)])) ; type 45 46 (define-base-kind ★) 47 (define-kind-constructor ∀★ #:arity >= 0) 48 (define-binding-type ∀ #:arr ∀★) 49 50 ;; alternative: normalize before type=? 51 ; but then also need to normalize in current-promote 52 (begin-for-syntax 53 (define (normalize τ) 54 (syntax-parse τ #:literals (#%plain-app #%plain-lambda) 55 [x:id #'x] 56 [(#%plain-app 57 (#%plain-lambda (tv ...) τ_body) τ_arg ...) 58 (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] 59 [(#%plain-lambda (x ...) . bodys) 60 #:with bodys_norm (stx-map normalize #'bodys) 61 (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)] 62 [(#%plain-app x:id . args) 63 #:with args_norm (stx-map normalize #'args) 64 (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)] 65 [(#%plain-app . args) 66 #:with args_norm (stx-map normalize #'args) 67 (transfer-stx-props (normalize #'(#%plain-app . args_norm)) τ #:ctx τ)] 68 [_ τ])) 69 70 (define old-eval (current-type-eval)) 71 (define (type-eval τ) (normalize (old-eval τ))) 72 (current-type-eval type-eval) 73 74 (define old-typecheck? (current-typecheck-relation)) 75 (define (new-typecheck? t1 t2) 76 (and (kindcheck? (kindof t1) (kindof t2)) 77 (old-typecheck? t1 t2))) 78 (current-typecheck-relation new-typecheck?) 79 80 ;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind= 81 (define old-kind=? (current-kind=?)) 82 (define (new-kind=? k1 k2) 83 (or (and (★? k1) (#%type? k2)) 84 (and (#%type? k1) (★? k2)) 85 (old-kind=? k1 k2))) 86 (current-kind=? new-kind=?) 87 (current-kindcheck-relation new-kind=?)) 88 89 (define-typed-syntax Λ 90 [(_ bvs:kind-ctx e) 91 #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e) 92 (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))]) 93 94 (define-typed-syntax inst 95 [(_ e τ:any-type ...) 96 ; #:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀) 97 #:with [e- τ_e] (infer+erase #'e) 98 #:with (~∀ (tv ...) τ_body) #'τ_e 99 #:with (~∀★ k ...) (kindof #'τ_e) 100 ; #:with ([τ- k_τ] ...) (infers+erase #'(τ ...)) 101 #:with (k_τ ...) (stx-map kindof #'(τ.norm ...)) 102 #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) 103 (typecheck-fail-msg/multi 104 #'(k ...) #'(k_τ ...) #'(τ ...)) 105 #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body) 106 (⊢ e- : τ_inst)]) 107 108 ;; extend λ to also work as a type 109 (define-typed-syntax λ 110 [(_ bvs:kind-ctx τ) ; type 111 #:with (Xs- τ- k_res) (infer/ctx+erase #'bvs #'τ #:tag '::) 112 (assign-kind #'(λ- Xs- τ-) #'(→ bvs.kind ... k_res))] 113 [(_ . rst) #'(sysf:λ . rst)]) ; term 114 115 ;; extend #%app to also work as a type 116 (define-typed-syntax #%app 117 [(_ τ_fn τ_arg ...) ; type 118 ; #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒) 119 #:with [τ_fn- k_fn] (infer+erase #'τ_fn #:tag '::) 120 #:when (syntax-e #'k_fn) ; non-false 121 #:with (~→ k_in ... k_out ~!) #'k_fn 122 #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:tag '::) 123 #:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...)) 124 (string-append 125 (format 126 "~a (~a:~a) Arguments to function ~a have wrong kinds(s), " 127 (syntax-source stx) (syntax-line stx) (syntax-column stx) 128 (syntax->datum #'τ_fn)) 129 "or wrong number of arguments:\nGiven:\n" 130 (string-join 131 (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line 132 (syntax->datum #'(τ_arg ...)) 133 (stx-map type->str #'(k_arg ...))) 134 "\n" #:after-last "\n") 135 (format "Expected: ~a arguments with type(s): " 136 (stx-length #'(k_in ...))) 137 (string-join (stx-map type->str #'(k_in ...)) ", ")) 138 (assign-kind #'(#%app- τ_fn- τ_arg- ...) #'k_out)] 139 [(_ . rst) #'(sysf:#%app . rst)]) ; term