fomega.rkt (4798B)
1 #lang s-exp macrotypes/typecheck 2 (reuse λ #%app Int → + #:from "sysf.rkt") 3 (reuse define-type-alias String #%datum #:from "stlc+reco+var.rkt") 4 5 ;; System F_omega 6 ;; Types: 7 ;; - redefine ∀ 8 ;; - extend kind? and kind=? to include #%type 9 ;; - extend sysf with tyλ and tyapp 10 ;; Terms: 11 ;; - extend sysf with Λ inst 12 13 (provide (type-out ∀) (kind-out ★ ⇒ ∀★ ∀) Λ inst tyλ tyapp) 14 15 (define-syntax-category :: kind) 16 17 ;; want #%type to be equiv to ★ 18 ;; => extend current-kind? to recognize #%type 19 ;; <= define ★ as rename-transformer expanding to #%type 20 (begin-for-syntax 21 (current-kind? (λ (k) (or (#%type? k) (kind? k)))) 22 ;; well-formed types, ie not types with ⇒ kind 23 (current-type? (λ (t) (define k (kindof t)) 24 (and k ((current-kind?) k) (not (⇒? k))))) 25 ;; any valid type (includes ⇒-kinded types) 26 (current-any-type? (λ (t) (define k (kindof t)) 27 (and k ((current-kind?) k))))) 28 29 (begin-for-syntax 30 (define ★? #%type?) 31 (define-syntax ~★ (lambda _ (error "~★ not implemented")))) ; placeholder 32 (define-syntax ★ (make-rename-transformer #'#%type)) 33 (define-kind-constructor ⇒ #:arity >= 1) 34 (define-kind-constructor ∀★ #:arity >= 0) 35 36 (define-binding-type ∀ #:arr ∀★) 37 38 ;; alternative: normalize before type=? 39 ;; but then also need to normalize in current-promote? 40 (begin-for-syntax 41 (define (normalize τ) 42 (syntax-parse τ #:literals (#%plain-app #%plain-lambda) 43 [x:id #'x] 44 [(#%plain-app 45 (#%plain-lambda (tv ...) τ_body) τ_arg ...) 46 (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] 47 [(#%plain-lambda (x ...) . bodys) 48 #:with bodys_norm (stx-map normalize #'bodys) 49 (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)] 50 [(#%plain-app x:id . args) 51 #:with args_norm (stx-map normalize #'args) 52 (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)] 53 [(#%plain-app . args) 54 #:with args_norm (stx-map normalize #'args) 55 #:with res (normalize #'(#%plain-app . args_norm)) 56 (transfer-stx-props #'res τ #:ctx τ)] 57 [_ τ])) 58 59 (define old-eval (current-type-eval)) 60 (define (type-eval τ) (normalize (old-eval τ))) 61 (current-type-eval type-eval) 62 63 (define old-type=? (current-type=?)) 64 ; ty=? == syntax eq and syntax prop eq 65 (define (type=? t1 t2) 66 (let ([k1 (kindof t1)][k2 (kindof t2)]) 67 (and (or (and (not k1) (not k2)) 68 (and k1 k2 ((current-kind=?) k1 k2))) 69 (old-type=? t1 t2)))) 70 (current-typecheck-relation type=?)) 71 72 (define-typed-syntax Λ 73 [(_ bvs:kind-ctx e) 74 #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e) 75 (⊢ e- : (∀ ([tv- :: bvs.kind] ...) τ_e))]) 76 77 (define-typed-syntax inst 78 [(_ e τ:any-type ...) 79 #:with [e- τ_e] (infer+erase #'e) 80 #:with (~∀ (tv ...) τ_body) #'τ_e 81 #:with (~∀★ k ...) (kindof #'τ_e) 82 ; #:with ([τ- k_τ] ...) (infers+erase #'(τ ...) #:tag '::) 83 #:with (k_τ ...) (stx-map kindof #'(τ.norm ...)) 84 #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) 85 (typecheck-fail-msg/multi 86 #'(k ...) #'(k_τ ...) #'(τ ...)) 87 #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body) 88 (⊢ e- : τ_inst)]) 89 90 ;; TODO: merge with regular λ and app? 91 ;; - see fomega2.rkt 92 (define-typed-syntax tyλ 93 [(_ bvs:kind-ctx τ_body) 94 #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body #:tag '::) 95 #:fail-unless ((current-kind?) #'k_body) 96 (format "not a valid type: ~a\n" (type->str #'τ_body)) 97 (assign-kind #'(λ- tvs- τ_body-) #'(⇒ bvs.kind ... k_body))]) 98 99 (define-typed-syntax tyapp 100 [(_ τ_fn τ_arg ...) 101 ; #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒) 102 #:with [τ_fn- (~⇒ k_in ... k_out)] (infer+erase #'τ_fn #:tag '::) 103 #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...) #:tag '::) 104 #:fail-unless (kindchecks? #'(k_arg ...) #'(k_in ...)) 105 (string-append 106 (format 107 "~a (~a:~a) Arguments to function ~a have wrong kinds(s), " 108 (syntax-source stx) (syntax-line stx) (syntax-column stx) 109 (syntax->datum #'τ_fn)) 110 "or wrong number of arguments:\nGiven:\n" 111 (string-join 112 (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line 113 (syntax->datum #'(τ_arg ...)) 114 (stx-map type->str #'(k_arg ...))) 115 "\n" #:after-last "\n") 116 (format "Expected: ~a arguments with type(s): " 117 (stx-length #'(k_in ...))) 118 (string-join (stx-map type->str #'(k_in ...)) ", ")) 119 (assign-kind #'(#%app- τ_fn- τ_arg- ...) #'k_out)])