stlc+occurrence.rkt (12385B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+sub.rkt" #:except #%datum) 3 (extends "stlc+cons.rkt" #:except + * #%datum and tup × proj ~× list) 4 (reuse tup × proj #:from "stlc+tup.rkt") 5 (require (only-in "stlc+tup.rkt" ~×)) 6 7 ;; Calculus for occurrence typing. 8 ;; - Types can be simple, or sets of simple types 9 ;; (aka "ambiguous types"; 10 ;; the run-time value will have one of a few ambiguous possible types.) 11 ;; - The ∪ constructor makes ambiguous types 12 ;; - `(test [τ ? x] e1 e2)` form will insert a run-time check to discriminate ∪ 13 ;; -- If the value at identifier x has type τ, then we continue to e1 with [x : τ] 14 ;; -- Otherwise, we move to e2 with [x : (- (typeof x) τ)]. 15 ;; i.e., [x : τ] is not possible 16 ;; - Subtyping rules: 17 ;; -- ALL : t ... <: t' => (U t ...) <: t' 18 ;; -- AMB : t <: (U ... t ...) 19 ;; -- EXT : (U t' ...) <: (U t t' ...) 20 ;; -- ONE : a<:b => (U a t' ...) <: (U b t' ...) 21 22 ;; ============================================================================= 23 24 (provide Bot Boolean Str ∪ #%datum test) 25 26 (define-base-type Bot) ;; For empty unions 27 (define-base-type Boolean) 28 (define-base-type Str) 29 30 (define-typed-syntax #%datum 31 [(_ . n:boolean) (⊢ (#%datum- . n) : Boolean)] 32 [(_ . n:str) (⊢ (#%datum- . n) : Str)] 33 [(_ . x) #'(stlc+sub:#%datum . x)]) 34 35 (define-type-constructor ∪ #:arity >= 1) 36 37 ;; ----------------------------------------------------------------------------- 38 ;; --- Union operations 39 40 ;; Occurrence type operations 41 ;; These assume that τ is a type in 'normal form' 42 (begin-for-syntax 43 (define (∪->list τ) 44 ;; Ignore type constructor & the kind 45 ;; (because there are no bound identifiers) 46 (syntax-parse τ 47 [(~∪ τ* ...) 48 (syntax->list #'(τ* ...))] 49 [_ 50 (error '∪->list (format "Given non-ambiguous type '~a'" τ))])) 51 52 (define (list->∪ τ*) 53 (if (null? τ*) 54 #'Bot 55 (τ-eval #`(∪ #,@τ*)))) 56 57 (define (∖ τ1 τ2) 58 (cond 59 [(∪? τ1) 60 (define (not-τ2? τ) 61 (not (typecheck? τ τ2))) 62 (list->∪ (filter not-τ2? (∪->list τ1)))] 63 [else ; do nothing not non-union types 64 τ1])) 65 ) 66 67 ;; ----------------------------------------------------------------------------- 68 ;; --- Normal Form 69 ;; Evaluate each type in the union, 70 ;; remove duplicates 71 ;; determinize the ordering of members 72 ;; flatten nested unions 73 74 (begin-for-syntax 75 76 (define τ-eval (current-type-eval)) 77 78 (define (τ->symbol τ) 79 (syntax-parse τ 80 [(_ κ) 81 (syntax->datum #'κ)] 82 [(_ κ (_ () _ τ* ...)) 83 (define κ-str (symbol->string (syntax->datum #'κ))) 84 (define τ-str* 85 (map (compose1 symbol->string τ->symbol) (syntax->list #'(τ* ...)))) 86 (string->symbol 87 (string-append 88 (apply string-append "(" κ-str τ-str*) 89 ")"))] 90 [_ 91 (error 'τ->symbol (~a (syntax->datum τ)))])) 92 93 (define ∪-eval 94 ;; Private helper: check that all functions have unique arities 95 ;; It's private because it assumes all τ* have been evaluated 96 (let ([assert-unique-arity-arrows 97 (lambda (τ*) 98 (for/fold ([seen '()]) 99 ([τ (in-list τ*)]) 100 (syntax-parse τ 101 [(~→ τ-dom* ... τ-cod) 102 (define arity (stx-length #'(τ-dom* ...))) 103 (when (memv arity seen) 104 (error '∪ (format "Cannot discriminate types in the union ~a. Multiple functions have arity ~a." (cons '∪ (map syntax->datum τ*)) arity))) 105 (cons arity seen)] 106 [_ seen])))]) 107 (lambda (τ-stx) 108 (syntax-parse (τ-eval τ-stx) 109 [(~∪ τ-stx* ...) 110 ;; Recursively evaluate members 111 (define τ** 112 (for/list ([τ (in-list (syntax->list #'(τ-stx* ...)))]) 113 (let ([τ+ (∪-eval τ)]) 114 (if (∪? τ+) 115 (∪->list τ+) 116 (list τ+))))) 117 ;; Remove duplicates from the union, sort members 118 (define τ* 119 (sort 120 (remove-duplicates (apply append τ**) (current-type=?)) 121 symbol<? 122 #:key τ->symbol)) 123 ;; Check for empty & singleton lists 124 (define τ 125 (cond 126 [(null? τ*) 127 (raise-user-error 'τ-eval "~a (~a:~a) empty union type ~a\n" 128 (syntax-source τ-stx) (syntax-line τ-stx) (syntax-column τ-stx) 129 (syntax->datum τ-stx))] 130 [(null? (cdr τ*)) 131 #`#,(car τ*)] 132 [else 133 (assert-unique-arity-arrows τ*) 134 #`#,(cons #'∪ τ*)])) 135 (τ-eval τ)] 136 [_ 137 (τ-eval τ-stx)])))) 138 (current-type-eval ∪-eval)) 139 140 ;; ----------------------------------------------------------------------------- 141 ;; --- Subtyping 142 143 (begin-for-syntax 144 ;; True if one ordered list (of types) is a subset of another 145 (define (subset? x* y* #:leq [cmp (current-typecheck-relation)]) 146 (let loop ([x* x*] [y* y*]) 147 (cond 148 [(null? x*) #t] 149 [(null? y*) #f] 150 [(cmp (car x*) (car y*)) 151 (loop (cdr x*) (cdr y*))] 152 [else 153 (loop x* (cdr y*))]))) 154 155 (define ∪-sub? 156 (let ([sub? (current-sub?)]) 157 (lambda (τ1-stx τ2-stx) 158 (define τ1 ((current-type-eval) τ1-stx)) 159 (define τ2 ((current-type-eval) τ2-stx)) 160 (or (Bot? τ1) (Top? τ2) 161 (match `(,(∪? τ1) ,(∪? τ2)) 162 ['(#f #t) 163 ;; AMB : a<:b => a <: (U ... b ...) 164 (for/or ([τ (in-list (∪->list τ2))]) 165 ((current-sub?) τ1 τ))] 166 ['(#t #t) 167 (define τ1* (∪->list τ1)) 168 (define τ2* (∪->list τ2)) 169 (match `(,(length τ1*) ,(length τ2*)) 170 [`(,L1 ,L2) #:when (< L1 L2) 171 ;; - EXT : (U t' ...) <: (U t t' ...) 172 (subset? τ1* τ2* #:leq (current-sub?))] 173 [`(,L1 ,L2) #:when (= L1 L2) 174 ;; - SUB : a<:b => (U a t' ...) <: (U b t' ...) 175 ;; `∪->list` guarantees same order on type members 176 ;; `sub?` is reflexive 177 (andmap (current-sub?) τ1* τ2*)] 178 [_ #f])] 179 ['(#t #f) 180 ;; - ALL : t... <: t' => (U t ...) <: t' 181 (andmap (lambda (τ) ((current-sub?) τ τ2)) (∪->list τ1))] 182 ['(#f #f) 183 ;; Fall back to OLD sub 184 (sub? τ1 τ2)]))))) 185 186 (current-sub? ∪-sub?) 187 (current-typecheck-relation (current-sub?)) 188 ) 189 190 ;; ----------------------------------------------------------------------------- 191 ;; --- Filters 192 ;; These are stored imperatively, in a function. 193 ;; Makes it easy to add a new filter & avoids duplicating this map 194 195 (begin-for-syntax 196 (define current-Π (make-parameter (lambda (x) (error 'Π)))) 197 198 (define (type->filter τ) 199 (define f ((current-Π) τ)) 200 (unless f 201 (error 'τ->filter (format "Could not express type '~a' as a filter." (syntax->datum τ)))) 202 f) 203 204 (define (type*->filter* τ*) 205 (map (current-Π) τ*)) 206 207 (define (simple-Π τ) 208 (syntax-parse (τ-eval τ) 209 [~Boolean 210 #'boolean?-] 211 [~Int 212 #'integer?-] 213 [~Str 214 #'string?-] 215 [~Num 216 #'number?-] 217 [~Nat 218 #'(lambda- (n) (and- (integer?- n) (not- (negative?- n))))] 219 [(~→ τ* ... τ) 220 (define k (stx-length #'(τ* ...))) 221 #`(lambda- (f) (and- (procedure?- f) (procedure-arity-includes?- f #,k #f)))] 222 [(~∪ τ* ...) 223 (define filter* (type*->filter* (syntax->list #'(τ* ...)))) 224 #`(lambda- (v) (for/or- ([f (in-list- (list- #,@filter*))]) (f v)))] 225 [_ 226 (error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))])) 227 (current-Π simple-Π) 228 229 ) 230 231 ;; (test (τ ? x) e1 e2) 232 ;; - drop absurd branches? 233 ;; - allow x not identifier (1. does nothing 2. latent filters) 234 (define-typed-syntax test #:datum-literals (?) 235 ;; -- THIS CASE BELONGS IN A NEW FILE 236 [(_ [τ0+:type ? (unop x-stx:id n-stx:nat)] e1 e2) 237 ;; 1. Check that we're using a known eliminator 238 #:when (free-identifier=? #'stlc+tup:proj #'unop) 239 ;; 2. Make sure we're filtering with a valid type 240 #:with f (type->filter #'τ0+) 241 ;; 3. Typecheck the eliminator call. Remember the type & apply the filter. 242 ;; (This type is PROBABLY a union -- else why bother testing!) 243 #:with (e0+ τ0) (infer+erase #'(unop x-stx n-stx)) 244 #:with τ0- (∖ #'τ0 #'τ0+) 245 ;; 4. Build the +/- types for our identifier; the thing we apply the elim. + test to 246 ;; We know that x has a pair type because (proj x n) typechecked 247 #:with (x (~× τi* ...)) (infer+erase #'x-stx) 248 #:with τ+ #`(stlc+tup:× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0+)) 249 #:with τ- #`(stlc+tup:× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0-)) 250 ;; 5. Check the branches with the refined types 251 #:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ+]) #'e1) 252 #:with [x2 e2+ τ2] (infer/ctx+erase #'([x-stx : τ-]) #'e2) 253 ;; 6. Desugar, replacing the filtered identifier 254 (⊢ (if- (f e0+) 255 ((lambda- x1 e1+) x-stx) 256 ((lambda- x2 e2+) x-stx)) 257 : (∪ τ1 τ2))] 258 ;; TODO lists 259 ;; For now, we can't express the type (List* A (U A B)), so our filters are too strong 260 ;; -- THE ORIGINAL 261 [(_ [τ0+:type ? x-stx:id] e1 e2) 262 #:with f (type->filter #'τ0+) 263 #:with (x τ0) (infer+erase #'x-stx) 264 #:with τ0- (∖ #'τ0 #'τ0+) 265 #:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ0+]) #'e1) 266 #:with [x2 e2+ τ2] (infer/ctx+erase #'([x-stx : τ0-]) #'e2) 267 ;; Expand to a conditional, using the runtime predicate 268 (⊢ (if- (f x-stx) 269 ((lambda- x1 e1+) x-stx) 270 ((lambda- x2 e2+) x-stx)) 271 : (∪ τ1 τ2))]) 272 273 ;; ============================================================================= 274 ;; === BELONGS IN A NEW FILE 275 276 ;; (extends "stlc+occurrence.rkt"); #:rename [test ot:test]) 277 ;; (extends "stlc+tup.rkt" #:except + #%datum) 278 279 (define-for-syntax (replace-at τ* n τ-new) 280 (for/list ([τ-old (in-list τ*)] 281 [i (in-naturals)]) 282 (if (= i n) 283 τ-new 284 τ-old))) 285 286 ;; Add subtyping for tuples 287 (begin-for-syntax 288 (define ×-sub? 289 (let ([sub? (current-sub?)]) 290 (lambda (τ1-stx τ2-stx) 291 (define τ1 ((current-type-eval) τ1-stx)) 292 (define τ2 ((current-type-eval) τ2-stx)) 293 (or (Bot? τ1) (Top? τ2) 294 (syntax-parse `(,τ1 ,τ2) 295 [((~× τi1* ...) 296 (~× τi2* ...)) 297 (and (stx-length=? #'(τi1* ...) 298 #'(τi2* ...)) 299 ;; Gotta use (current-sub?), because products may be recursive 300 (stx-andmap (current-sub?) #'(τi1* ...) #'(τi2* ...)))] 301 [_ 302 (sub? τ1 τ2)]))))) 303 (current-sub? ×-sub?) 304 (current-typecheck-relation (current-sub?))) 305 306 ;; --- Update Π for products 307 (begin-for-syntax 308 (define π-Π 309 (let ([Π (current-Π)]) 310 (lambda (τ) 311 (syntax-parse (τ-eval τ) 312 [(~× τ* ...) 313 (define filter* (type*->filter* (syntax->list #'(τ* ...)))) 314 #`(lambda- (v*) 315 (and- (list?- v*) 316 (for/and- ([v (in-list- v*)] 317 [f (in-list- (list- #,@filter*))]) 318 (f v))))] 319 [_ ;; Fall back 320 (Π τ)])))) 321 (current-Π π-Π)) 322 323 ;; ============================================================================= 324 ;; === Lists 325 326 ;; Subtyping for lists 327 (begin-for-syntax 328 (define list-sub? 329 (let ([sub? (current-sub?)]) 330 (lambda (τ1-stx τ2-stx) 331 (define τ1 ((current-type-eval) τ1-stx)) 332 (define τ2 ((current-type-eval) τ2-stx)) 333 (or (Bot? τ1) (Top? τ2) 334 (syntax-parse `(,τ1 ,τ2) 335 [((~List τi1) 336 (~List τi2)) 337 ((current-sub?) #'τi1 #'τi2)] 338 [_ 339 (sub? τ1 τ2)]))))) 340 (current-sub? list-sub?) 341 (current-typecheck-relation (current-sub?))) 342 343 ;; --- Update Π for lists 344 (begin-for-syntax 345 (define list-Π 346 (let ([Π (current-Π)]) 347 (lambda (τ) 348 (syntax-parse (τ-eval τ) 349 [(~List τi) 350 (define f ((current-Π) #'τi)) 351 #`(lambda- (v*) 352 (and- (list?- v*) 353 (for/and- ([v (in-list- v*)]) 354 (#,f v))))] 355 [_ ;; Fall back 356 (Π τ)])))) 357 (current-Π list-Π))