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