fomega2.rkt (5098B)
1 #lang turnstile/lang 2 (extends "sysf.rkt" #:except #%datum ∀ ~∀ ∀? Λ inst λ #%app →) 3 (reuse String #%datum #:from "stlc+reco+var.rkt") 4 5 ; same as fomega.rkt except here λ and #%app works as both type and terms 6 ; - uses definition from stlc, but tweaks type? and kind? predicates 7 ;; → is also both type and kind 8 9 ;; System F_omega 10 ;; Type relation: 11 ;; Types: 12 ;; - types from sysf.rkt 13 ;; - String from stlc+reco+var 14 ;; Terms: 15 ;; - extend ∀ Λ inst from sysf 16 ;; - #%datum from stlc+reco+var 17 18 (provide define-type-alias 19 ★ ∀★ ∀ 20 λ #%app → Λ inst 21 (for-syntax current-kind-eval kindcheck?)) 22 23 (define-syntax-category :: kind) 24 25 (begin-for-syntax 26 (define old-kind? (current-kind?)) 27 (current-kind? (λ (k) (or (#%type? k) (old-kind? k)))) 28 ;; Try to keep "type?" backward compatible with its uses so far, 29 ;; eg in the definition of λ or previous type constuctors. 30 ;; (However, this is not completely possible, eg define-type-alias) 31 ;; So now "type?" no longer validates types, rather it's a subset. 32 ;; But we no longer need type? to validate types, instead we can use 33 ;; (kind? (typeof t)) 34 (current-type? (λ (t) (define k (kindof t)) 35 (and k ((current-kind?) k) (not (→? k))))) 36 37 ;; o.w., a valid type is one with any valid kind 38 (current-any-type? (λ (t) (define k (kindof t)) 39 (and k ((current-kind?) k))))) 40 41 ; must override 42 (define-syntax define-type-alias 43 (syntax-parser 44 [(_ alias:id τ) 45 #:with (τ- _) (infer+erase #'τ #:tag '::) 46 #'(define-syntax alias 47 (syntax-parser [x:id #'τ-][(_ . rst) #'(τ- . rst)]))])) 48 49 ;; extend → to serve as both type and kind 50 (define-syntax (→ stx) 51 (syntax-parse stx 52 [(_ k:kind ...) ; kind 53 (add-orig (mk-kind #'(sysf:→- k.norm ...)) stx)] 54 [(_ . tys) #'(sysf:→ . tys)])) ; type 55 56 (define-base-kind ★) 57 (define-kind-constructor ∀★ #:arity >= 0) 58 (define-binding-type ∀ #:arr ∀★) 59 60 ;; alternative: normalize before type=? 61 ; but then also need to normalize in current-promote 62 (begin-for-syntax 63 (define (normalize τ) 64 (syntax-parse τ #:literals (#%plain-app #%plain-lambda) 65 [x:id #'x] 66 [(#%plain-app 67 (#%plain-lambda (tv ...) τ_body) τ_arg ...) 68 (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] 69 [(#%plain-lambda (x ...) . bodys) 70 #:with bodys_norm (stx-map normalize #'bodys) 71 (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)] 72 [(#%plain-app x:id . args) 73 #:with args_norm (stx-map normalize #'args) 74 (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)] 75 [(#%plain-app . args) 76 #:with args_norm (stx-map normalize #'args) 77 (transfer-stx-props (normalize #'(#%plain-app . args_norm)) τ #:ctx τ)] 78 [_ τ])) 79 80 (define old-eval (current-type-eval)) 81 (define (type-eval τ) (normalize (old-eval τ))) 82 (current-type-eval type-eval) 83 84 ;; must be kind= (and not kindcheck?) since old-kind=? recurs on curr-kind= 85 (define old-kind=? (current-kind=?)) 86 (define (new-kind=? k1 k2) 87 (or (and (★? k1) (#%type? k2)) ; enables use of existing type defs 88 (and (#%type? k1) (★? k2)) 89 (old-kind=? k1 k2))) 90 (current-kind=? new-kind=?) 91 (current-kindcheck-relation new-kind=?) 92 93 (define old-typecheck? (current-typecheck-relation)) 94 (define (new-typecheck? t1 t2) 95 (syntax-parse (list t1 t2) #:datum-literals (:) 96 [((~∀ ([tv1 : k1]) tbody1) 97 (~∀ ([tv2 : k2]) tbody2)) 98 (and (kindcheck? #'k1 #'k2) (typecheck? #'tbody1 #'tbody2))] 99 [_ (old-typecheck? t1 t2)])) 100 (current-typecheck-relation new-typecheck?)) 101 102 (define-typed-syntax (Λ bvs:kind-ctx e) ≫ 103 [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e] 104 -------- 105 [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)]) 106 107 (define-typed-syntax (inst e τ:any-type ...) ≫ 108 [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ :: (~∀★ k ...))] 109 ; [⊢ τ ≫ τ- ⇐ :: k] ... ; doesnt work since def-typed-s ⇐ not using kindcheck? 110 #:with (k_τ ...) (stx-map kindof #'(τ.norm ...)) 111 #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) 112 (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) 113 -------- 114 [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body)]) 115 116 ;; extend λ to also work as a type 117 (define-kinded-syntax λ 118 [(_ bvs:kind-ctx τ) ≫ ; type 119 [[bvs.x ≫ X- :: bvs.kind] ... ⊢ τ ≫ τ- ⇒ k_res] 120 ------------ 121 [⊢ (λ- (X- ...) τ-) ⇒ (→ bvs.kind ... k_res)]] 122 [(_ . rst) ≫ --- [≻ (sysf:λ . rst)]]) ; term 123 124 ;; extend #%app to also work as a type 125 (define-kinded-syntax #%app 126 [(_ τ_fn τ_arg ...) ≫ ; type 127 [⊢ τ_fn ≫ τ_fn- ⇒ (~→ k_in ... k_out)] 128 #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...]) 129 (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...]) 130 [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ... 131 ------------- 132 [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out]] 133 [(_ . rst) ≫ --- [≻ (sysf:#%app . rst)]]) ; term