stlc+union.rkt (4286B)
1 #lang turnstile/lang 2 (extends "ext-stlc.rkt" 3 #:except #%app #%datum + add1 sub1 * 4 Int Int? ~Int Float Float? ~Float Bool ~Bool Bool?) 5 6 (require (for-syntax "util/filter-maximal.rkt")) 7 8 ;; Simply-Typed Lambda Calculus, plus union types 9 ;; Types: 10 ;; - types from and ext+stlc.rkt 11 ;; - Top, Num, Nat 12 ;; - U 13 ;; Type relations: 14 ;; - sub? 15 ;; - Any <: Top 16 ;; - Nat <: Int 17 ;; - Int <: Num 18 ;; - → 19 ;; Terms: 20 ;; - terms from stlc+lit.rkt, except redefined: datum and + 21 ;; - also * 22 ;; Other: sub? current-sub? 23 24 (provide (for-syntax current-sub? prune+sort) 25 define-named-type-alias 26 Int Num Nat U (type-out U*) 27 Zero NegInt PosInt Float Bool False True 28 (typed-out [+ : (→ Num Num Num)] 29 [* : (→ Num Num Num)] 30 [add1 : (→ Int Int)] 31 [sub1 : (→ Int Int)]) 32 #%datum #%app 33 (for-syntax ~PosInt ~Zero ~NegInt ~True ~False)) 34 35 (define-syntax define-named-type-alias 36 (syntax-parser 37 [(define-named-type-alias Name:id τ:any-type) 38 #'(define-syntax Name 39 (make-variable-like-transformer (add-orig #'τ #'Name)))] 40 [(define-named-type-alias (f:id x:id ...) ty) ; dont expand yet 41 #'(define-syntax (f stx) 42 (syntax-parse stx 43 [(_ x ...) (add-orig #'ty stx)]))])) 44 45 (define-base-types Zero NegInt PosInt Float False True) 46 (define-type-constructor U* #:arity >= 0) 47 48 (define-for-syntax (prune+sort tys) 49 (stx-sort 50 (filter-maximal 51 (stx->list tys) 52 typecheck?))) 53 54 (define-syntax (U stx) 55 (syntax-parse stx 56 [(_ . tys) 57 ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys 58 #:with ((~or (~U* ty1- ...) ty2-) ...) (stx-map (current-type-eval) #'tys) 59 #:with tys- (prune+sort #'(ty1- ... ... ty2- ...)) 60 (if (= 1 (stx-length #'tys-)) 61 (stx-car #'tys-) 62 (syntax/loc stx (U* . tys-)))])) 63 (define-syntax Bool 64 (make-variable-like-transformer 65 (add-orig #'(U False True) #'Bool))) 66 (define-syntax Nat 67 (make-variable-like-transformer 68 (add-orig #'(U Zero PosInt) #'Nat))) 69 (define-syntax Int 70 (make-variable-like-transformer 71 (add-orig #'(U NegInt Nat) #'Int))) 72 (define-syntax Num 73 (make-variable-like-transformer (add-orig #'(U Float Int) #'Num))) 74 75 (define-typed-syntax #%datum 76 [(_ . b:boolean) ≫ 77 #:with ty_out (if (syntax-e #'b) #'True #'False) 78 -------- 79 [⊢ [_ ≫ (#%datum- . b) ⇒ : ty_out]]] 80 [(_ . n:integer) ≫ 81 #:with ty_out (let ([m (syntax-e #'n)]) 82 (cond [(zero? m) #'Zero] 83 [(> m 0) #'PosInt] 84 [else #'NegInt])) 85 -------- 86 [⊢ [_ ≫ (#%datum- . n) ⇒ : ty_out]]] 87 [(#%datum . n:number) ≫ 88 #:when (real? (syntax-e #'n)) 89 -------- 90 [⊢ [_ ≫ (#%datum- . n) ⇒ : Float]]] 91 [(_ . x) ≫ 92 -------- 93 [_ ≻ (ext-stlc:#%datum . x)]]) 94 95 (define-typed-syntax #%app 96 [(_ e_fn e_arg ...) ≫ 97 [⊢ [e_fn ≫ e_fn- ⇒ : (~→ ~! τ_in ... τ_out)]] 98 #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) 99 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) 100 [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...] 101 -------- 102 [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]]) 103 104 (begin-for-syntax 105 (define (sub? t1 t2) 106 ; need this because recursive calls made with unexpanded types 107 ;; (define τ1 ((current-type-eval) t1)) 108 ;; (define τ2 ((current-type-eval) t2)) 109 ;; (printf "t1 = ~a\n" (syntax->datum t1)) 110 ;; (printf "t2 = ~a\n" (syntax->datum t2)) 111 (or 112 ((current-type=?) t1 t2) 113 (syntax-parse (list t1 t2) 114 ; 2 U types, subtype = subset 115 [((~U* . tys1) (~U* . tys2)) 116 (for/and ([t (stx->list #'tys1)]) 117 ((current-sub?) t t2))] 118 ; 1 U type, 1 non-U type. subtype = member 119 [(ty (~U* . tys)) 120 (for/or ([t (stx->list #'tys)]) 121 ((current-sub?) #'ty t))] 122 [((~→ s1 ... s2) (~→ t1 ... t2)) 123 (and (subs? #'(t1 ...) #'(s1 ...)) 124 ((current-sub?) #'s2 #'t2))] 125 [_ #f]))) 126 (define current-sub? (make-parameter sub?)) 127 (current-typecheck-relation sub?) 128 (define (subs? τs1 τs2) 129 (and (stx-length=? τs1 τs2) 130 (stx-andmap (current-sub?) τs1 τs2))) 131 132 (define (join t1 t2) #`(U #,t1 #,t2)) 133 (current-join join))