fomega.rkt (3889B)
1 #lang turnstile/lang 2 (reuse λ #%app Int → + #:from "sysf.rkt") 3 (reuse define-type-alias #%datum String #:from "ext-stlc.rkt") 4 5 ;; System F_omega 6 ;; Types: 7 ;; - redefine ∀ 8 ;; - extend sysf with tyλ and tyapp 9 ;; Terms: 10 ;; - extend sysf with Λ inst 11 12 (provide (type-out ∀) (kind-out ★ ⇒ ∀★) Λ inst tyλ tyapp) 13 14 (define-syntax-category :: kind) 15 16 ;; want #%type to be equiv to ★ 17 ;; => extend current-kind? to recognize #%type 18 ;; <= define ★ as rename-transformer expanding to #%type 19 (begin-for-syntax 20 (current-kind? (λ (k) (or (#%type? k) (kind? k)))) 21 ;; any valid type (includes ⇒-kinded types) 22 (current-any-type? (λ (t) (define k (kindof t)) 23 (and k ((current-kind?) k)))) 24 ;; well-formed types, ie not types with ⇒ kind 25 (current-type? (λ (t) (and ((current-any-type?) t) 26 (not (⇒? (kindof t))))))) 27 28 (begin-for-syntax 29 (define ★? #%type?) 30 (define-syntax ~★ (λ _ (error "~★ not implemented")))) ; placeholder 31 (define-syntax ★ (make-rename-transformer #'#%type)) 32 (define-kind-constructor ⇒ #:arity >= 1) 33 (define-kind-constructor ∀★ #:arity >= 0) 34 35 (define-binding-type ∀ #:arr ∀★) 36 37 ;; alternative: normalize before type=? 38 ;; but then also need to normalize in current-promote 39 (begin-for-syntax 40 (define (normalize τ) 41 (syntax-parse τ #:literals (#%plain-app #%plain-lambda) 42 [x:id #'x] 43 [(#%plain-app 44 (#%plain-lambda (tv ...) τ_body) τ_arg ...) 45 (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] 46 [(#%plain-lambda (x ...) . bodys) 47 #:with bodys_norm (stx-map normalize #'bodys) 48 (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)] 49 [(#%plain-app x:id . args) 50 #:with args_norm (stx-map normalize #'args) 51 (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)] 52 [(#%plain-app . args) 53 #:with args_norm (stx-map normalize #'args) 54 #:with res (normalize #'(#%plain-app . args_norm)) 55 (transfer-stx-props #'res τ #:ctx τ)] 56 [_ τ])) 57 58 (define old-eval (current-type-eval)) 59 (define (new-type-eval τ) (normalize (old-eval τ))) 60 (current-type-eval new-type-eval) 61 62 (define old-type=? (current-type=?)) 63 ;; need to also compare kinds of types 64 (define (new-type=? t1 t2) 65 (let ([k1 (kindof t1)][k2 (kindof t2)]) 66 ;; need these `not` checks bc type= does a structural stx traversal 67 ;; and may compare non-type ids (like #%plain-app) 68 (and (or (and (not k1) (not k2)) 69 (and k1 k2 ((current-kind=?) k1 k2))) 70 (old-type=? t1 t2)))) 71 (current-typecheck-relation new-type=?)) 72 73 (define-typed-syntax (Λ bvs:kind-ctx e) ≫ 74 [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e] 75 -------- 76 [⊢ e- ⇒ (∀ ([tv- :: bvs.kind] ...) τ_e)]) 77 78 ;; τ.norm invokes current-type-eval while "≫ τ-" uses only local-expand 79 ;; (via infer fn) 80 (define-typed-syntax (inst e τ:any-type ...) ≫ 81 [⊢ e ≫ e- ⇒ (~∀ tvs τ_body) (⇒ :: (~∀★ k ...))] 82 [⊢ τ ≫ τ- ⇐ :: k] ... 83 -------- 84 [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]) 85 86 ;; - see fomega2.rkt for example with no explicit tyλ and tyapp 87 (define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫ 88 [[bvs.x ≫ tv- :: bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body] 89 #:fail-unless ((current-kind?) #'k_body) ; better err, in terms of τ_body 90 (format "not a valid type: ~a\n" (type->str #'τ_body)) 91 -------- 92 [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)]) 93 94 (define-kinded-syntax (tyapp τ_fn τ_arg ...) ≫ 95 [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)] 96 #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...]) 97 (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...]) 98 [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ... 99 -------- 100 [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out])