fomega-no-reuse-old.rkt (6307B)
1 #lang turnstile/lang 2 3 ;; System F_omega, without reusing rules from other languages 4 ;; - try to avoid using built-in "kind" system (ie #%type) 5 ;; - not quite there: define-primop and typed-out still use current-type? 6 ;; - use define-internal- forms instead 7 8 ;; example suggested by Alexis King 9 10 ;; this version still uses ': key for kinds 11 12 ;; tyλ and λ are separate forms 13 14 (provide define-type-alias 15 ★ ⇒ Int Bool String Float Char → ∀ tyλ tyapp 16 (typed-out [+ : (→ Int Int Int)]) 17 λ #%app #%datum Λ inst ann) 18 19 (define-syntax-category kind) 20 21 ;; redefine: 22 ;; - current-type?: well-formed types have kind ★ 23 ;; - current-any-type?: valid types have any valid kind 24 ;; - current-type-eval: reduce tylams and tyapps 25 ;; - current-type=?: must compare kind annotations as well 26 (begin-for-syntax 27 28 ;; well-formed types have kind ★ 29 ;; (need this for define-primop, which still uses type stx-class) 30 (current-type? (λ (t) (★? (kindof t)))) 31 ;; o.w., a valid type is one with any valid kind 32 (current-any-type? (λ (t) ((current-kind?) (kindof t)))) 33 34 ;; TODO: I think this can be simplified 35 (define (normalize τ) 36 (syntax-parse τ #:literals (#%plain-app #%plain-lambda) 37 [x:id #'x] 38 [(#%plain-app 39 (#%plain-lambda (tv ...) τ_body) τ_arg ...) 40 (normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))] 41 [(#%plain-lambda (x ...) . bodys) 42 #:with bodys_norm (stx-map normalize #'bodys) 43 (transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)] 44 [(#%plain-app x:id . args) 45 #:with args_norm (stx-map normalize #'args) 46 (transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)] 47 [(#%plain-app . args) 48 #:with args_norm (stx-map normalize #'args) 49 #:with res (normalize #'(#%plain-app . args_norm)) 50 (transfer-stx-props #'res τ #:ctx τ)] 51 [_ τ])) 52 (define old-eval (current-type-eval)) 53 (current-type-eval (lambda (τ) (normalize (old-eval τ)))) 54 55 (define old-type=? (current-type=?)) 56 ; ty=? == syntax eq and syntax prop eq 57 (define (type=? t1 t2) 58 (let ([k1 (kindof t1)][k2 (kindof t2)]) 59 ; the extra `and` and `or` clauses are bc type=? is a structural 60 ; traversal on stx objs, so not all sub stx objs will have a "type"-stx 61 (and (or (and (not k1) (not k2)) 62 (and k1 k2 ((current-kind=?) k1 k2))) 63 (old-type=? t1 t2)))) 64 (current-type=? type=?) 65 (current-typecheck-relation type=?)) 66 67 ;; kinds ---------------------------------------------------------------------- 68 (define-internal-kind-constructor ★) ; defines ★- 69 (define-syntax (★ stx) 70 (syntax-parse stx 71 [:id (mk-kind #'(★-))] 72 [(_ k:kind ...) (mk-kind #'(★- k.norm ...))])) 73 74 (define-kind-constructor ⇒ #:arity >= 1) 75 76 ;; types ---------------------------------------------------------------------- 77 (define-kinded-syntax (define-type-alias alias:id τ:any-type) ≫ 78 ------------------ 79 [≻ (define-syntax- alias 80 (make-variable-like-transformer #'τ.norm))]) 81 82 (define-base-type Int : ★) 83 (define-base-type Bool : ★) 84 (define-base-type String : ★) 85 (define-base-type Float : ★) 86 (define-base-type Char : ★) 87 88 (define-internal-type-constructor →) ; defines →- 89 (define-kinded-syntax (→ ty ...+) ≫ 90 [⊢ ty ≫ ty- ⇒ (~★ . _)] ... 91 -------- 92 [⊢ (→- ty- ...) ⇒ ★]) 93 94 (define-internal-binding-type ∀) ; defines ∀- 95 (define-kinded-syntax ∀ #:datum-literals (:) 96 [(_ ([tv:id : k_in:kind] ...) ty) ≫ 97 [[tv ≫ tv- : k_in.norm] ... ⊢ ty ≫ ty- ⇒ (~★ . _)] 98 ------- 99 [⊢ (∀- (tv- ...) ty-) ⇒ (★ k_in.norm ...)]]) 100 101 (define-kinded-syntax (tyλ bvs:kind-ctx τ_body) ≫ 102 [[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body] 103 #:fail-unless ((current-kind?) #'k_body) 104 (format "not a valid type: ~a\n" (type->str #'τ_body)) 105 -------- 106 [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)]) 107 108 (define-kinded-syntax (tyapp τ_fn τ_arg ...) ≫ 109 [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)] 110 #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...]) 111 (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...]) 112 [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ... 113 -------- 114 [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out]) 115 116 ;; terms ---------------------------------------------------------------------- 117 (define-typed-syntax λ #:datum-literals (:) 118 [(_ ([x:id : τ_in:type] ...) e) ≫ 119 [[x ≫ x- : τ_in.norm] ... ⊢ e ≫ e- ⇒ τ_out] 120 ------- 121 [⊢ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]] 122 [(_ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫ 123 [[x ≫ x- : τ_in] ... ⊢ e ≫ e- ⇐ τ_out] 124 --------- 125 [⊢ (λ- (x- ...) e-)]]) 126 127 (define-typed-syntax (#%app e_fn e_arg ...) ≫ 128 [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)] 129 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 130 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 131 [⊢ e_arg ≫ e_arg- ⇐ τ_in] ... 132 -------- 133 [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out]) 134 135 (define-typed-syntax (ann e (~datum :) τ:type) ≫ 136 [⊢ e ≫ e- ⇐ τ.norm] 137 -------- 138 [⊢ e- ⇒ τ.norm]) 139 140 (define-typed-syntax #%datum 141 [(_ . b:boolean) ≫ 142 -------- 143 [⊢ (#%datum- . b) ⇒ Bool]] 144 [(_ . s:str) ≫ 145 -------- 146 [⊢ (#%datum- . s) ⇒ String]] 147 [(_ . f) ≫ 148 #:when (flonum? (syntax-e #'f)) 149 -------- 150 [⊢ (#%datum- . f) ⇒ Float]] 151 [(_ . c:char) ≫ 152 -------- 153 [⊢ (#%datum- . c) ⇒ Char]] 154 [(_ . n:integer) ≫ 155 -------- 156 [⊢ (#%datum- . n) ⇒ Int]] 157 [(_ . x) ≫ 158 -------- 159 [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) 160 161 (define-typed-syntax (Λ bvs:kind-ctx e) ≫ 162 [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e] 163 -------- 164 [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)]) 165 166 (define-typed-syntax (inst e τ ...) ≫ 167 [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~★ k ...))] 168 ; [⊢ τ ≫ τ- ⇐ k] ... ; ⇐ would use typechecks? 169 [⊢ τ ≫ τ- ⇒ k_τ] ... ; so use ⇒ and kindchecks? 170 #:fail-unless (kindchecks? #'(k_τ ...) #'(k ...)) 171 (typecheck-fail-msg/multi #'(k ...) #'(k_τ ...) #'(τ ...)) 172 #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body) 173 -------- 174 [⊢ e- ⇒ τ-inst]) 175