typecheck.rkt (60465B)
1 #lang racket/base 2 (require 3 "postfix-in.rkt" 4 (postfix-in - racket/base) 5 (postfix-in - racket/bool) 6 (postfix-in - racket/match) 7 (postfix-in - racket/promise) 8 (for-syntax (except-in racket extends) 9 syntax/parse racket/syntax syntax/stx racket/stxparam 10 syntax/parse/define 11 (only-in racket/provide-transform 12 make-provide-pre-transformer pre-expand-export 13 make-provide-transformer expand-export) 14 "stx-utils.rkt") 15 (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx 16 "stx-utils.rkt") 17 (for-meta 3 racket/base syntax/parse racket/syntax) 18 racket/bool racket/provide racket/require racket/match racket/promise 19 syntax/parse/define) 20 (provide 21 postfix-in symbol=?- match- delay- 22 (all-defined-out) 23 (for-syntax (all-defined-out)) 24 (for-meta 2 (all-defined-out)) 25 (except-out (all-from-out racket/base) #%module-begin) 26 (all-from-out syntax/parse/define) 27 (for-syntax 28 (all-from-out racket syntax/parse racket/syntax syntax/stx 29 racket/provide-transform 30 "stx-utils.rkt")) 31 (for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)) 32 (rename-out [define-syntax-category define-stx-category])) 33 34 (module+ test 35 (require (for-syntax rackunit))) 36 37 ;; type checking functions/forms 38 39 ;; General type checking strategy: 40 ;; - Each (expanded) syntax object has a ': syntax property that is the type 41 ;; of the surface form. 42 ;; - To typecheck a surface form, it local-expands each subterm in order to get 43 ;; their types. 44 ;; - With this typechecking strategy, the typechecking implementation machinery 45 ;; is easily inserted into each #%XYZ form 46 ;; - A base type is just a Racket identifier, so type equality, even with 47 ;; aliasing, is just free-identifier=? 48 ;; - type constructors are prefix 49 ;; - use different stx prop keys for different metadata, eg ':: for kinds 50 51 ;; redefine #%module-begin to add some provides 52 (provide (rename-out [mb #%module-begin])) 53 (define-syntax (mb stx) 54 (syntax-parse stx 55 [(_ . stuff) 56 (syntax/loc this-syntax 57 (#%module-begin 58 ; auto-provide some useful racket forms 59 (provide #%module-begin #%top-interaction #%top 60 require only-in prefix-in rename-in) 61 . stuff))])) 62 63 (struct exn:fail:type:runtime exn:fail:user ()) 64 65 (begin-for-syntax 66 (define (mk-? id) (format-id id "~a?" id)) 67 (define (mk-- id) (format-id id "~a-" id)) 68 (define (mk-~ id) (format-id id "~~~a" id)) 69 (define (mk-#% id) (format-id id "#%~a" id)) 70 (define (mkx2 id) (format-id id "~a~a" id id)) 71 (define (mk-param id) (format-id id "current-~a" id)) 72 (define-for-syntax (mk-? id) (format-id id "~a?" id)) 73 (define-for-syntax (mk-~ id) (format-id id "~~~a" id)) 74 ;; drop-file-ext : String -> String 75 (define (drop-file-ext filename) 76 (car (string-split filename "."))) 77 ;; extract-filename : PathString or Symbol -> String 78 (define (extract-filename file) 79 (define f (if (string? file) file (symbol->string file))) 80 (path->string (path-replace-suffix (file-name-from-path f) ""))) 81 (define-syntax-parameter stx (syntax-rules ())) 82 83 ;; parameter is an identifier transformer 84 (define current-host-lang (make-parameter mk--))) 85 86 ;; non-Turnstile define-typed-syntax 87 ;; TODO: potentially confusing? get rid of this? 88 ;; - but it will be annoying since the `stx` stx-param is used everywhere 89 (define-syntax (define-typed-syntax stx) 90 (syntax-parse stx 91 [(_ name:id stx-parse-clause ...+) 92 #'(define-syntax (name syntx) 93 (syntax-parameterize ([stx (make-rename-transformer #'syntx)]) 94 (syntax-parse syntx stx-parse-clause ...)))])) 95 96 ;; need options for 97 ;; - pass through 98 ;; - use (generated) prefix to avoid conflicts 99 ;; - exceptions - dont pass through 100 ;; - either because id from another lang, or extending 101 ;; - use in impl 102 ;; - either as is 103 ;; - or prefixed 104 (define-syntax extends 105 (syntax-parser 106 [(_ base-lang 107 (~optional (~seq #:prefix pre)) 108 (~optional (~seq #:except (~and x:id (~not _:keyword)) ...) 109 #:defaults ([(x 1) null])) 110 (~optional (~seq #:rename [old new] ...) 111 #:defaults ([(old 1) null][(new 1) null]))) 112 #:with pre: 113 (or 114 (attribute pre) 115 (let ([pre (or (let ([dat (syntax-e #'base-lang)]) 116 (and (or (string? dat) (symbol? dat)) 117 (extract-filename dat))) 118 #'base-lang)]) 119 (format-id #'base-lang "~a:" pre))) 120 #:with internal-pre (generate-temporary) 121 #:with non-excluded-imports #'(except-in base-lang x ... old ...) 122 #:with conflicted? #'(λ (n) (member (string->symbol n) '(#%app λ #%datum begin let let* letrec if define))) 123 #:with not-conflicted? #'(λ (n) (and (not (conflicted? n)) n)) 124 #`(begin 125 #,(quasisyntax/loc this-syntax 126 (require #,(syntax/loc this-syntax 127 (prefix-in pre: base-lang)))) ; prefixed 128 #,(quasisyntax/loc this-syntax 129 (require #,(syntax/loc this-syntax 130 (rename-in (only-in base-lang old ...) [old new] ...)))) 131 #,(quasisyntax/loc this-syntax 132 (require #,(syntax/loc this-syntax 133 (filtered-in not-conflicted? non-excluded-imports)))) 134 #,(quasisyntax/loc this-syntax 135 (require 136 #,(syntax/loc this-syntax 137 (filtered-in ; conflicted names, with (internal) prefix 138 (let ([conflicted-pre (symbol->string (syntax->datum #'internal-pre))]) 139 (λ (name) (and (conflicted? name) 140 (string-append conflicted-pre name)))) 141 non-excluded-imports)))) 142 #,(quasisyntax/loc this-syntax 143 (provide (filtered-out 144 (let* ([pre-str #,(string-append (extract-filename (syntax-e #'base-lang)) ":")] 145 [int-pre-str #,(symbol->string (syntax->datum #'internal-pre))] 146 [pre-str-len (string-length pre-str)] 147 [int-pre-str-len (string-length int-pre-str)] 148 [drop-pre (λ (s) (substring s pre-str-len))] 149 [drop-int-pre (λ (s) (substring s int-pre-str-len))] 150 [excluded (map symbol->string (syntax->datum #'(x ... new ...)))]) 151 (λ (name) 152 (define out-name 153 (or (and (string-prefix? name pre-str) 154 (drop-pre name)) 155 (and (string-prefix? name int-pre-str) 156 (drop-int-pre name)) 157 name)) 158 (and (not (member out-name excluded)) out-name))) 159 (all-from-out base-lang)) 160 )))])) 161 (define-syntax reuse 162 (syntax-parser 163 [(_ (~or x:id [old:id new:id]) ... #:from base-lang) 164 #:with pre: 165 (let ([pre (or (let ([dat (syntax-e #'base-lang)]) 166 (and (or (string? dat) (symbol? dat)) 167 (extract-filename dat))) 168 #'base-lang)]) 169 (format-id #'base-lang "~a:" pre)) 170 #`(begin 171 #,(syntax/loc this-syntax 172 (require (rename-in (only-in base-lang old ...) [old new] ...))) 173 #,(syntax/loc this-syntax 174 (require (prefix-in pre: (only-in base-lang x ...)))) 175 #,(quasisyntax/loc this-syntax 176 (provide (filtered-out 177 (let* ([pre-str #,(string-append (extract-filename (syntax-e #'base-lang)) ":")] 178 [pre-str-len (string-length pre-str)] 179 [drop-pre (λ (s) (substring s pre-str-len))] 180 ; [excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))] 181 [origs (map symbol->string (syntax->datum #'(x ... new ...)))]) 182 (λ (name) 183 (define out-name 184 (or (and (string-prefix? name pre-str) 185 (drop-pre name)) 186 name)) 187 (and #;(not (member out-name excluded)) 188 (member out-name origs) 189 out-name))) 190 (all-from-out base-lang)))))])) 191 192 (define-syntax add-expected 193 (syntax-parser 194 [(_ e τ) (add-orig (add-expected-ty #'e #'τ) (get-orig #'e))])) 195 (define-syntax pass-expected 196 (syntax-parser 197 [(_ e stx) (add-expected-ty #'e (get-expected-type #'stx))])) 198 (define-for-syntax (add-expected-ty e ty) 199 (if (and (syntax? ty) (syntax-e ty)) 200 (set-stx-prop/preserved e 'expected-type ((current-type-eval) ty)) 201 e)) 202 203 (begin-for-syntax 204 ;; Helper functions for attaching/detaching types, kinds, etc. 205 206 ;; A Tag is a Symbol serving as a stx prop key for some kind of metadata. 207 ;; e.g., ': for types, ':: for kinds, etc. 208 ;; Define new metadata via `define-syntax-category` 209 210 ;; attach : Stx Tag Val -> Stx 211 ;; Adds Tag+Val to Stx as stx prop, returns new Stx. 212 ;; e.g., Stx = expression, Tag = ':, Val = Type stx 213 (define (attach stx tag v) 214 (set-stx-prop/preserved stx tag v)) 215 (define (attachs stx tags vs #:ev [ev (λ (x) x)]) 216 (for/fold ([stx stx]) ([t (in-list tags)] [v (in-stx-list vs)]) 217 (attach stx t (ev v)))) 218 ;; detach : Stx Tag -> Val 219 ;; Retrieves Val at Tag stx prop on Stx. 220 ;; If Val is a non-empty list, return first element, otherwise return Val. 221 ;; e.g., Stx = expression, Tag = ':, Val = Type stx 222 (define (detach stx tag) 223 (get-stx-prop/ca*r stx tag))) 224 225 ;; ---------------------------------------------------------------------------- 226 ;; ---------------------------------------------------------------------------- 227 ;; define-syntax-category ----------------------------------------------------- 228 ;; ---------------------------------------------------------------------------- 229 ;; ---------------------------------------------------------------------------- 230 231 ;; This is a huge macro. 232 ;; Defines a new type of metadata on syntax, e.g. types, and functions 233 ;; and macros for manipulating the metadata, e.g. define-base-type, type=?, etc 234 235 ;; A syntax category requires a name and two keys, 236 ;; - one to use when attaching values of this category (eg ': for types) 237 ;; - another for attaching "types" to these values (eg ':: for kinds on types) 238 ;; If key1 is unspecified, the default is ': 239 ;; If key2 is unspecified, the default is "twice" key1 (ie '::) 240 ;; 241 ;; example uses: 242 ;; (define-syntax-category type) 243 ;; (define-syntax-category : type) 244 ;; (define-syntax-category : type ::) 245 ;; (define-syntax-category :: kind :::) 246 ;; 247 ;; CODE NOTE: 248 ;; To make this large macros-defining macro easier to read, 249 ;; I use a `type` pat var corresponding to the category name, 250 ;; and a `kind` pat var for its "type". 251 ;; But `name` could correspond to any kind of metadata, 252 ;; e.g., kinds, src locs, polymorphic bounds 253 (define-syntax (define-syntax-category stx) 254 (syntax-parse stx 255 [(_ name:id) ; default key1 = ': for types 256 #'(define-syntax-category : name)] 257 [(_ key:id name:id) ; default key2 = ':: for kinds 258 #`(define-syntax-category key name #,(mkx2 #'key))] 259 [(_ key1:id name:id key2:id) 260 ;; syntax classes 261 #:with type #'name ; dangerous? check `type` not used in binding pos below 262 #:with any-type (format-id #'name "any-~a" #'name) 263 #:with type-ctx (format-id #'name "~a-ctx" #'name) 264 #:with type-bind (format-id #'name "~a-bind" #'name) 265 #:with type-ann (format-id #'name "~a-ann" #'name) 266 ;; type well-formedness 267 #:with #%tag (mk-#% #'name) ; default "type" for this metadata, e.g. #%type 268 #:with #%tag? (mk-? #'#%tag) 269 #:with mk-type (format-id #'name "mk-~a" #'name) 270 #:with type? (mk-? #'name) 271 #:with any-type? (mk-? #'any-type) 272 #:with current-type? (mk-param #'type?) 273 #:with current-any-type? (mk-param #'any-type?) 274 ;; assigning and retrieving types 275 #:with type-key1 (format-id #'name "~a-key1" #'name) 276 #:with type-key2 (format-id #'name "~a-key2" #'name) 277 #:with assign-type (format-id #'name "assign-~a" #'name) 278 #:with fast-assign-type (format-id #'name "fast-assign-~a" #'name) 279 #:with typeof (format-id #'name "~aof" #'name) 280 #:with tagoftype (format-id #'name "tagof~a" #'name) 281 ;; type checking 282 #:with current-typecheck-relation (format-id #'name "current-~acheck-relation" #'name) 283 #:with typecheck? (format-id #'name "~acheck?" #'name) 284 #:with typechecks? (format-id #'name "~achecks?" #'name) 285 #:with type=? (format-id #'name "~a=?" #'name) 286 #:with types=? (format-id #'name "~as=?" #'name) 287 #:with current-type=? (mk-param #'type=?) 288 #:with same-types? (format-id #'name "same-~as?" #'name) 289 #:with current-type-eval (format-id #'name "current-~a-eval" #'name) 290 #:with default-type-eval (format-id #'name "default-~a-eval" #'name) 291 #:with type-evals (format-id #'name "~a-evals" #'name) 292 ;; defining types 293 #:with define-base-type (format-id #'name "define-base-~a" #'name) 294 #:with define-base-types (format-id #'name "define-base-~as" #'name) 295 #:with define-internal-type-constructor (format-id #'name "define-internal-~a-constructor" #'name) 296 #:with define-type-constructor (format-id #'name "define-~a-constructor" #'name) 297 #:with define-internal-binding-type (format-id #'name "define-internal-binding-~a" #'name) 298 #:with define-binding-type (format-id #'name "define-binding-~a" #'name) 299 #:with type-out (format-id #'name "~a-out" #'name) 300 #'(begin 301 (define #%tag void) ; TODO: cache expanded #%tag? 302 (begin-for-syntax 303 ;; type-wellformedness --------------------------------------------- 304 (define (#%tag? t) (and (id? t) (free-id=? t #'#%tag))) 305 (define (mk-type t) (attach t 'key2 #'#%tag)) 306 ;; type? corresponds to "well-formed" types 307 (define (type? t) (#%tag? (tagoftype t))) 308 (define current-type? (make-parameter type?)) 309 ;; any-type? corresponds to any type, defaults to type? 310 (define (any-type? t) (type? t)) 311 (define current-any-type? (make-parameter any-type?)) 312 ;; assigning and retrieving types ---------------------------------- 313 (define (type-key1) 'key1) 314 (define (type-key2) 'key2) 315 (define (typeof stx) (detach stx 'key1)) 316 (define (tagoftype stx) (detach stx 'key2)) ; = kindof if kind stx-cat defined 317 (define (fast-assign-type e τ) ; TODO: does this actually help? 318 (attach e 'key1 (syntax-local-introduce τ))) 319 (define (assign-type e τ) 320 (fast-assign-type e ((current-type-eval) τ))) 321 ;; helper stx classes ---------------------------------------------- 322 (define-syntax-class type ;; e.g., well-formed types 323 #:attributes (norm) 324 (pattern τ 325 #:with norm ((current-type-eval) #'τ) 326 #:fail-unless ((current-type?) #'norm) 327 (format "~a (~a:~a) not a well-formed ~a: ~a" 328 (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) 329 'name (type->str #'τ)))) 330 (define-syntax-class any-type ;; e.g., any valid type 331 #:attributes (norm) 332 (pattern τ 333 #:with norm ((current-type-eval) #'τ) 334 #:fail-unless ((current-any-type?) #'norm) 335 (format "~a (~a:~a) not a valid ~a: ~a" 336 (syntax-source #'τ) (syntax-line #'τ) (syntax-column #'τ) 337 'name (type->str #'τ)))) 338 (define-syntax-class type-bind #:datum-literals (key1) 339 #:attributes (x type) 340 (pattern [x:id key1 ~! (~var ty type)] 341 #:attr type #'ty.norm) 342 (pattern any 343 #:fail-when #t 344 (format 345 (string-append 346 "Improperly formatted ~a annotation: ~a; should have shape [x ~a τ], " 347 "where τ is a valid ~a.") 348 'name (type->str #'any) 'key1 'name) 349 #:attr x #f #:attr type #f)) 350 (define-syntax-class type-ctx 351 #:attributes ((x 1) (type 1)) 352 (pattern ((~var || type-bind) (... ...)))) 353 (define-syntax-class type-ann ; type instantiation 354 #:attributes (norm) 355 (pattern (~and (_) 356 (~fail #:unless (brace? this-syntax)) 357 ((~var t type) ~!)) 358 #:attr norm (delay #'t.norm)) 359 (pattern any 360 #:fail-when #t 361 (format 362 (string-append 363 "Improperly formatted ~a annotation: ~a; should have shape {τ}, " 364 "where τ is a valid ~a.") 365 'name (type->str #'any) 'name) 366 #:attr norm #f)) 367 ;; checking types 368 (define (type=? t1 t2) 369 ;; (printf "(τ=) t1 = ~a\n" #;τ1 (stx->datum t1)) 370 ;; (printf "(τ=) t2 = ~a\n" #;τ2 (stx->datum t2)) 371 (or (and (id? t1) (id? t2) (free-id=? t1 t2)) 372 (and (stx-null? t1) (stx-null? t2)) 373 (and (not (stx-pair? t1)) (not (id? t1)) 374 (not (stx-pair? t2)) (not (id? t1)) ; datums 375 (equal? (stx->datum t1) (stx->datum t2))) 376 (syntax-parse (list t1 t2) ; handle binding types 377 [(((~literal #%plain-lambda) (~and (_:id (... ...)) xs) . ts1) 378 ((~literal #%plain-lambda) (~and (_:id (... ...)) ys) . ts2)) 379 (and (stx-length=? #'xs #'ys) 380 (stx-length=? #'ts1 #'ts2) 381 (stx-andmap 382 (λ (ty1 ty2) 383 ((current-type=?) (substs #'ys #'xs ty1) ty2)) 384 #'ts1 #'ts2))] 385 [_ (and (stx-pair? t1) (stx-pair? t2) 386 (types=? t1 t2))]))) 387 (define current-type=? (make-parameter type=?)) 388 (define (types=? τs1 τs2) 389 (and (stx-length=? τs1 τs2) 390 (stx-andmap (current-type=?) τs1 τs2))) 391 ; extra indirection, enables easily overriding type=? with eg sub? 392 ; to add subtyping, without changing any other definitions 393 (define current-typecheck-relation (make-parameter type=?)) 394 ;; convenience fns for current-typecheck-relation 395 (define (typecheck? t1 t2) 396 ((current-typecheck-relation) t1 t2)) 397 (define (typechecks? τs1 τs2) 398 (and (= (stx-length τs1) (stx-length τs2)) 399 (stx-andmap typecheck? τs1 τs2))) 400 (define (same-types? τs) 401 (define τs-lst (syntax->list τs)) 402 (or (null? τs-lst) 403 (andmap (λ (τ) ((current-type=?) (car τs-lst) τ)) (cdr τs-lst)))) 404 ;; type eval 405 ;; - default-type-eval == full expansion == canonical type representation 406 ;; - must expand because: 407 ;; - checks for unbound identifiers (ie, undefined types) 408 ;; - checks for valid types, ow can't distinguish types and terms 409 ;; - could parse types but separate parser leads to duplicate code 410 ;; - later, expanding enables reuse of same mechanisms for kind checking 411 ;; and type application 412 (define (default-type-eval τ) 413 ; TODO: optimization: don't expand if expanded 414 ; - but this causes problems when combining unexpanded and 415 ; expanded types to create new types 416 ; - alternative: use syntax-local-expand-expression? 417 (add-orig (expand/df τ) τ)) 418 (define current-type-eval (make-parameter default-type-eval)) 419 (define (type-evals τs) #`#,(stx-map (current-type-eval) τs))) 420 ;; defining types ---------------------------------------------------- 421 (define-syntax type-out ;; helps with providing defined types 422 (make-provide-transformer 423 (lambda (stx modes) 424 (syntax-parse stx 425 ;; cannot write ty:type bc provides might precede type def 426 [(_ . ts) 427 #:with t-expanders (stx-map mk-~ #'ts) 428 #:with t?s (stx-map mk-? #'ts) 429 #:with t-s (filter identifier-binding (stx-map mk-- #'ts)) 430 (expand-export 431 (syntax/loc stx (combine-out 432 (combine-out . ts) (combine-out . t-s) 433 (for-syntax (combine-out . t-expanders) . t?s))) 434 modes)])))) 435 ;; base types -------------------------------------------------------- 436 (define-syntax define-base-type 437 (syntax-parser ; default = 'key2 + #%tag 438 [(_ (~var τ id)) #'(define-base-type τ key2 #%tag)] 439 [(_ (~var τ id) new-key2 new-#%tag) 440 #:with τ? (mk-? #'τ) 441 #:with τ-expander (mk-~ #'τ) 442 #:with τ-internal (generate-temporary #'τ) 443 #`(begin 444 (begin-for-syntax 445 (define (τ? t) 446 (syntax-parse t 447 [((~literal #%plain-app) (~literal τ-internal)) #t] 448 [_ #f])) 449 (define-syntax τ-expander 450 (pattern-expander 451 (syntax-parser 452 [(~var _ id) 453 #'((~literal #%plain-app) (~literal τ-internal))] 454 ; - this case used by ⇑, TODO: remove this case? 455 ; - but it's also needed when matching a list of types, 456 ; e.g., in stlc+sub (~Nat τ) 457 [(_ . rst) 458 #'(((~literal #%plain-app) (~literal τ-internal)) . rst)])))) 459 (define τ-internal 460 (λ () (raise (exn:fail:type:runtime 461 (format "~a: Cannot use ~a at run time" 'τ 'tag) 462 (current-continuation-marks))))) 463 (define-syntax τ 464 (syntax-parser 465 [(~var _ id) 466 (add-orig 467 (attach 468 (syntax/loc this-syntax (τ-internal)) 469 'new-key2 (expand/df #'new-#%tag)) 470 #'τ)])))])) 471 (define-syntax define-base-types 472 (syntax-parser 473 [(_ (~var x id) (... ...)) 474 #'(begin (define-base-type x) (... ...))])) 475 ;; type constructors ------------------------------------------------- 476 ;; internal-type-constructor defines: 477 ;; - internal id identifying the constructor 478 ;; - predicate recognizing the internal id 479 ;; - expanded shape of type 480 ;; - pattern expander recognizing the shape 481 ;; - internal contructor τ- 482 ;; internal-type-constructor does no checks: 483 ;; - does not check arity 484 ;; - does not check that inputs are valid types 485 ;; - does not attach a kind to itself 486 (define-syntax define-internal-type-constructor 487 (syntax-parser 488 [(_ (~var τ id) 489 (~or 490 (~optional ; variances 491 (~seq #:arg-variances arg-variances-stx:expr) 492 #:name "#:arg-variances keyword" 493 #:defaults 494 ([arg-variances-stx 495 #`(λ (stx-id) 496 (for/list ([_ (in-stx-list (stx-cdr stx-id))]) 497 invariant))])) 498 (~optional ; extra-info 499 (~seq #:extra-info extra-info) 500 #:name "#:extra-info keyword" 501 #:defaults ([extra-info #'void]))) (... ...)) 502 #:with τ? (mk-? #'τ) 503 #:with τ- (mk-- #'τ) 504 #:with τ-expander (mk-~ #'τ) 505 #:with τ-internal (generate-temporary #'τ) 506 #`(begin 507 (begin-for-syntax 508 (define (τ? t) 509 (syntax-parse t 510 [(~Any (~literal τ-internal) . _) #t] 511 [_ #f])) 512 (define-syntax τ-expander 513 (pattern-expander 514 (syntax-parser 515 [(_ . pat) 516 #:with expanded-τ (generate-temporary) 517 #'(~and expanded-τ 518 (~Any 519 (~literal/else τ-internal 520 (format "Expected ~a ~a, got: ~a" 521 'τ 'name (type->str #'expanded-τ)) 522 #'expanded-τ) 523 . pat))]))) 524 (define arg-vars arg-variances-stx)) 525 (define τ-internal 526 (λ _ (raise (exn:fail:type:runtime 527 (format "~a: Cannot use ~a at run time" 'τ 'name) 528 (current-continuation-marks))))) 529 ; τ- is an internal constructor: 530 ; It does not validate inputs and does not attach a kind, 531 ; ie, it won't be recognized as a valid type, the programmer 532 ; must implement their own kind system on top 533 (define-syntax (τ- stx) 534 (syntax-parse stx 535 [(_ . args) 536 #:with τ* (add-arg-variances #'τ-internal (arg-vars stx)) 537 (syntax/loc stx 538 (τ* (λ () (#%expression extra-info) . args)))])))])) 539 (define-syntax define-type-constructor 540 (syntax-parser 541 [(_ (~var τ id) 542 ;; TODO: allow any order of kws between τ and τ- 543 (~optional ; arity 544 (~seq #:arity op n:exact-nonnegative-integer) 545 #:defaults ([op #'=] [n #'1])) 546 . (~and other-options (~not (#:arity . _)))) 547 #:with τ- (mk-- #'τ) 548 #'(begin 549 (define-internal-type-constructor τ . other-options) 550 (define-syntax (τ stx) 551 (syntax-parse stx 552 [(_ . args) 553 #:fail-unless (op (stx-length #'args) n) 554 (format 555 "wrong number of arguments, expected ~a ~a" 556 'op 'n) 557 #:with ([arg- _] (... (... ...))) (infers+erase #'args #:tag 'key2) 558 ;; args are validated on the next line rather than above 559 ;; to ensure enough stx-parse progress for proper err msg, 560 ;; ie, "invalid type" instead of "improper tycon usage" 561 #:with (~! (~var _ type) (... (... ...))) #'(arg- (... (... ...))) 562 (add-orig (mk-type (syntax/loc stx (τ- arg- (... (... ...))))) stx)] 563 [_ ;; else fail with err msg 564 (type-error #:src stx 565 #:msg 566 (string-append 567 "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments") 568 #'τ stx #'op #'n)])))])) 569 (define-syntax define-internal-binding-type 570 (syntax-parser 571 [(_ (~var τ id) 572 (~or 573 (~optional ; variances 574 (~seq #:arg-variances arg-variances-stx:expr) 575 #:name "#:arg-variances keyword" 576 #:defaults 577 ([arg-variances-stx 578 #`(λ (stx-id) 579 (for/list ([arg (in-stx-list (stx-cddr stx-id))]) 580 invariant))])) 581 (~optional ; extra-info 582 (~seq #:extra-info extra-info) 583 #:name "#:extra-info keyword" 584 #:defaults ([extra-info #'void]))) (... ...)) 585 #:with τ? (mk-? #'τ) 586 #:with τ- (mk-- #'τ) 587 #:with τ-expander (mk-~ #'τ) 588 #:with τ-internal (generate-temporary #'τ) 589 #`(begin 590 (begin-for-syntax 591 (define (τ? t) 592 (syntax-parse t 593 [(~Any/bvs (~literal τ-internal) _ . _) 594 #t] 595 [_ #f])) 596 ;; cannot deal with annotations bc τ- has no knowledge of 597 ;; its kind 598 (define-syntax τ-expander 599 (pattern-expander 600 (syntax-parser 601 ; this case used by ⇑, TODO: remove this case? 602 ;; if has-annotations? 603 ;; - type has surface shape: 604 ;; (τ ([tv : k] ...) body ...) 605 ;; - and parses to pattern: 606 ;; [([tv k] ...) (body ...)] 607 ;; if not has-annotations? 608 ;; - type has surface shape: 609 ;; (τ (tv ...) body ...) 610 ;; - and parses to pattern: 611 ;; [(tv ...) (body ...)] 612 [(_ . pat:id) 613 #:with expanded-τ (generate-temporary) 614 ; #:with kindcon-expander (mk-~ #'kindcon) 615 #'(~and expanded-τ 616 (~Any/bvs 617 (~literal/else τ-internal 618 (format "Expected ~a type, got: ~a" 619 'τ (type->str #'expanded-τ)) 620 #'expanded-τ) 621 (~and bvs (tv (... (... (... ...))))) 622 . rst) 623 ;; #,(if (attribute has-annotations?) 624 ;; #'(~and 625 ;; (~parse (kindcon-expander k (... (... ...))) 626 ;; (detach #'expanded-τ)) 627 ;; (~parse pat 628 ;; #'[([tv k] (... (... ...))) rst])) 629 (~parse pat #'[bvs rst]))] 630 ;; TODO: fix this to handle has-annotations? 631 ;; the difference with the first case is that here 632 ;; the body is ungrouped, ie, 633 ;; parses to pattern[(tv ...) . (body ...)] 634 [(_ bvs-pat . pat) 635 #:with expanded-τ (generate-temporary) 636 #'(~and expanded-τ 637 (~Any/bvs 638 (~literal/else τ-internal 639 (format "Expected ~a ~a, got: ~a" 640 'τ 'name (type->str #'expanded-τ)) 641 #'expanded-τ) 642 bvs-pat . pat))]))) 643 (define arg-vars arg-variances-stx)) 644 (define τ-internal 645 (λ _ (raise (exn:fail:type:runtime 646 (format "~a: Cannot use ~a at run time" 'τ 'name) 647 (current-continuation-marks))))) 648 ; τ- is an internal constructor: 649 ; It does not validate inputs and does not attach a kind, 650 ; ie, it won't be recognized as a valid type, the programmer 651 ; must implement their own kind system 652 (define-syntax (τ- stx) 653 (syntax-parse stx 654 [(_ bvs . args) 655 #:with τ* (add-arg-variances #'τ-internal (arg-vars stx)) 656 (syntax/loc stx 657 (τ* (λ bvs (#%expression extra-info) . args)))])))])) 658 (define-syntax define-binding-type 659 (syntax-parser 660 [(_ (~var τ id) 661 (~or ;; TODO: allow any order of kws between τ and τ- 662 (~optional ; arity, ie body exprs 663 (~seq #:arity op n:exact-nonnegative-integer) 664 #:name "#:arity keyword" 665 #:defaults ([op #'=] [n #'1])) 666 (~optional ; bvs, ie num bindings tyvars 667 (~seq #:bvs bvs-op bvs-n:exact-nonnegative-integer) 668 #:name "#:bvs keyword" 669 #:defaults ([bvs-op #'>=][bvs-n #'0])) 670 (~optional ; arr, ie constructor for kind annotations 671 (~seq #:arr (~and kindcon (~parse has-annotations? #'#t))) 672 #:name "#:arr keyword" 673 #:defaults ([kindcon #'void]))) ; dont use kindcon default 674 (... ...) 675 . (~and other-options 676 (~not ((~or #:arity #:bvs #:arr) . _)))) 677 #:with τ- (mk-- #'τ) 678 #`(begin 679 (define-internal-binding-type τ . other-options) 680 (define-syntax (τ stx) 681 (syntax-parse stx 682 [(_ (~and bvs 683 (~or (bv:id (... (... ...))) 684 (~and (~fail #:unless #,(attribute has-annotations?)) 685 ([_ (~datum key2) _] (... (... ...))) 686 bvs+ann))) 687 . args) 688 #:fail-unless (bvs-op (stx-length #'bvs) bvs-n) 689 (format "wrong number of type vars, expected ~a ~a" 690 'bvs-op 'bvs-n) 691 #:fail-unless (op (stx-length #'args) n) 692 (format "wrong number of arguments, expected ~a ~a" 693 'op 'n) 694 #:with bvs+ks (if #,(attribute has-annotations?) 695 #'bvs+ann 696 #'([bv key2 #%tag] (... (... ...)))) 697 #:with (bvs- τs- _) (infers/ctx+erase #'bvs+ks #'args #:tag 'key2) 698 ;; args are validated on the next line rather than above 699 ;; to ensure enough stx-parse progress for proper err msg, 700 ;; ie, "invalid type" instead of "improper tycon usage" 701 #:with (~! (~var _ type) (... (... ...))) #'τs- 702 #:with ([tv (~datum key2) k_arg] (... (... ...))) #'bvs+ks 703 #:with k_result (if #,(attribute has-annotations?) 704 #'(kindcon k_arg (... (... ...))) 705 #'#%tag) 706 (add-orig 707 (attach #'(τ- bvs- . τs-) 'key2 (default-type-eval #'k_result)) 708 stx)] 709 [_ 710 (type-error #:src stx 711 #:msg 712 (string-append 713 "Improper usage of type constructor ~a: ~a, expected ~a ~a arguments") 714 #'τ stx #'op #'n)])))])))])) 715 716 ;; ---------------------------------------------------------------------------- 717 ;; ---------------------------------------------------------------------------- 718 ;; end of define-syntax-category ---------------------------------------------- 719 ;; ---------------------------------------------------------------------------- 720 ;; ---------------------------------------------------------------------------- 721 722 ;; pre-declare all type-related functions and forms 723 (define-syntax-category type) 724 725 ;; TODO: move these into define-syntax-category? 726 (define-syntax typed-out 727 (make-provide-pre-transformer 728 (lambda (stx modes) 729 (syntax-parse stx #:datum-literals (:) 730 ;; cannot write ty:type bc provides might precede type def 731 [(_ (~and (~or (~and [out-x:id (~optional :) ty] (~parse x ((current-host-lang)#'out-x))) 732 [[x:id (~optional :) ty] out-x:id])) ...) 733 #:with (x/tc ...) (generate-temporaries #'(x ...)) 734 #:when (stx-map 735 syntax-local-lift-module-end-declaration 736 ;; use define-primop to validate type 737 #'((define-primop x/tc x ty) ...)) 738 (pre-expand-export (syntax/loc stx (rename-out [x/tc out-x] ...)) 739 modes)])))) 740 741 ;; colon is optional to make it easier to use define-primop in macros 742 (define-syntax define-primop 743 (syntax-parser #:datum-literals (:) 744 [(define-primop op:id (~optional :) τ) 745 #:with op- ((current-host-lang) #'op) 746 #'(define-primop op op- τ)] 747 [(define-primop op/tc:id (~optional #:as) op:id (~optional :) τ:type) 748 ; rename-transformer doesnt seem to expand at the right time 749 ; - op still has no type in #%app 750 #'(define-syntax op/tc 751 (make-variable-like-transformer (assign-type #'op #'τ)))])) 752 753 ;; generic, type-agnostic parameters 754 ;; Use in code that is generic over types and kinds, e.g., in #lang Turnstile 755 (begin-for-syntax 756 (define current=? (make-parameter (current-type=?))) 757 (define (=s? xs1 xs2) ; map current=? pairwise over lists 758 (and (stx-length=? xs1 xs2) (stx-andmap (current=?) xs1 xs2))) 759 (define (sames? stx) ; check list contains same types 760 (define xs (stx->list stx)) 761 (or (null? xs) (andmap (λ (x) ((current=?) (car xs) x)) (cdr xs)))) 762 (define current-check-relation (make-parameter (current-typecheck-relation))) 763 (define (check? x1 x2) ((current-check-relation) x1 x2)) 764 (define (checks? xs1 xs2) ; map current-check-relation pairwise of lists 765 (and (stx-length=? xs1 xs2) (stx-andmap check? xs1 xs2))) 766 (define current-ev (make-parameter (current-type-eval))) 767 (define current-tag (make-parameter (type-key1)))) 768 769 ;; type assignment utilities -------------------------------------------------- 770 (define-simple-macro (with-ctx ([x x- ty] ...) e ...) 771 (let-syntax 772 ([x (make-variable-like-transformer (assign-type #'x- #'ty))] ...) 773 e ...)) 774 775 (define-syntax (let*-syntax stx) 776 (syntax-parse stx 777 [(_ () . body) #'(let-syntax () . body)] 778 [(_ (b . bs) . es) #'(let-syntax (b) (let*-syntax bs . es))])) 779 780 (define-syntax (⊢m stx) 781 (syntax-parse stx #:datum-literals (:) 782 [(_ e : τ) (assign-type #`e #`τ)] 783 [(_ e τ) (assign-type #`e #`τ)])) 784 785 (begin-for-syntax 786 ;; var-assign : 787 ;; Id (Listof Sym) (StxListof TypeStx) -> Stx 788 (define (var-assign x seps τs) 789 (attachs x seps τs #:ev (current-type-eval))) 790 791 ;; macro-var-assign : Id -> (Id (Listof Sym) (StxListof TypeStx) -> Stx) 792 ;; generate a function for current-var-assign that expands 793 ;; to an invocation of the macro by the given identifier 794 ;; e.g. 795 ;; > (current-var-assign (macro-var-assign #'foo)) 796 ;; > ((current-var-assign) #'x '(:) #'(τ)) 797 ;; #'(foo x : τ) 798 (define ((macro-var-assign mac-id) x seps τs) 799 (datum->syntax x `(,mac-id ,x . ,(stx-appendmap list seps τs)))) 800 801 ;; current-var-assign : 802 ;; (Parameterof [Id (Listof Sym) (StxListof TypeStx) -> Stx]) 803 (define current-var-assign 804 (make-parameter var-assign)) 805 806 ;; Type assignment macro (ie assign-type) for nicer syntax 807 (define-syntax (⊢ stx) 808 (syntax-parse stx 809 [(_ e tag τ) #'(assign-type #`e #`τ)] 810 [(_ e τ) #'(⊢ e : τ)])) 811 (define-syntax (⊢/no-teval stx) 812 (syntax-parse stx 813 [(_ e tag τ) #'(fast-assign-type #`e #`τ)] 814 [(_ e τ) #'(⊢/no-teval e : τ)])) 815 816 ;; functions for manipulating "expected type" 817 (define (add-expected-type e τ) 818 (if (and (syntax? τ) (syntax-e τ)) 819 (set-stx-prop/preserved e 'expected-type τ) ; dont type-eval?, ie expand? 820 e)) 821 (define (get-expected-type e) 822 (get-stx-prop/cd*r e 'expected-type)) 823 824 ;; TODO: remove? only used by macrotypes/examples/infer.rkt 825 (define (add-env e env) (set-stx-prop/preserved e 'env env)) 826 (define (get-env e) (syntax-property e 'env)) 827 828 (define (mk-tyvar X) (attach X 'tyvar #t)) 829 (define (tyvar? X) (syntax-property X 'tyvar)) 830 831 (define type-pat "[A-Za-z]+") 832 833 ;; TODO: remove this? only benefit is single control point for current-promote 834 ;; - infers type of e 835 ;; - checks that type of e matches the specified type 836 ;; - erases types in e 837 ;; - returns e- and its type 838 ;; - does not return type if it's base type 839 (define-syntax (⇑ stx) 840 (syntax-parse stx #:datum-literals (as) 841 [(_ e as tycon) 842 #:with τ? (mk-? #'tycon) 843 #:with τ-get (format-id #'tycon "~a-get" #'tycon) 844 #:with τ-expander (mk-~ #'tycon) 845 #'(syntax-parse 846 ;; when type error, prefer outer err msg 847 (with-handlers ([exn:fail? 848 (λ (ex) 849 (define matched-ty 850 (regexp-match 851 (pregexp 852 (string-append "got\\:\\s(" type-pat ")")) 853 (exn-message ex))) 854 (unless matched-ty 855 (raise ex (current-continuation-marks))) 856 (define t-in-msg 857 (datum->syntax #'here 858 (string->symbol 859 (cadr matched-ty)))) 860 (list #'e t-in-msg))]) 861 (infer+erase #'e)) 862 #:context #'e 863 [(e- τ_e_) 864 #:with τ_e ((current-promote) #'τ_e_) 865 #:fail-unless (τ? #'τ_e) 866 (format 867 "~a (~a:~a): Expected expression ~s to have ~a type, got: ~a" 868 (syntax-source #'e) (syntax-line #'e) (syntax-column #'e) 869 (if (has-orig? #'e-) 870 (syntax->datum (get-orig #'e-)) 871 (syntax->datum #'e)) 872 'tycon (type->str #'τ_e)) 873 (syntax-parse #'τ_e 874 [(τ-expander . args) #'(e- args)] 875 [_ #'e-])])])) 876 (define-syntax (⇑s stx) 877 (syntax-parse stx #:datum-literals (as) 878 [(_ es as tycon) 879 #:with τ? (mk-? #'tycon) 880 #:with τ-get (format-id #'tycon "~a-get" #'tycon) 881 #:with τ-expander (mk-~ #'tycon) 882 #'(syntax-parse (stx-map infer+erase #'es) #:context #'es 883 [((e- τ_e_) (... ...)) 884 #:with (τ_e (... ...)) (stx-map (current-promote) #'(τ_e_ (... ...))) 885 #:when (stx-andmap 886 (λ (e t) 887 (or (τ? t) 888 (type-error #:src e 889 #:msg 890 (string-append 891 (format "Expected expression ~s" (syntax->datum e)) 892 " to have ~a type, got: ~a") 893 (quote-syntax tycon) t))) 894 #'es 895 #'(τ_e (... ...))) 896 #:with res 897 (stx-map (λ (e t) 898 (syntax-parse t 899 [(τ-expander . args) #`(#,e args)] 900 [_ e])) 901 #'(e- (... ...)) 902 #'(τ_e (... ...))) 903 #'res])])) 904 905 ;; -------------------------------------------------------------------------- 906 ;; "infer" function for expanding/computing type of an expression 907 908 ;; matches arbitrary number of nexted (expanded) let-stxs 909 (define-syntax ~let*-syntax 910 (pattern-expander 911 (syntax-parser 912 [(_ . pat) 913 #:with the-stx (generate-temporary) 914 #'(~and the-stx 915 (~parse pat (let L ([stxs #'(the-stx)]) 916 (syntax-parse stxs 917 [(((~literal let-values) () 918 ((~literal let-values) () 919 . rst))) 920 (L #'rst)] 921 [es #'es]))))]))) 922 923 ;; basic infer function with no context: 924 ;; infers the type and erases types in an expression 925 (define (infer+erase e #:tag [tag (current-tag)] #:expa [expa expand/df]) 926 (define e+ (expa e)) 927 (list e+ (detach e+ tag))) 928 ;; infers the types and erases types in multiple expressions 929 (define (infers+erase es #:tag [tag (current-tag)] #:expa [expa expand/df]) 930 (stx-map (λ (e) (infer+erase e #:tag tag #:expa expa)) es)) 931 932 ;; This is the main "infer" function. Most others are defined in terms of this. 933 ;; It should be named infer+erase but leaving it for now for backward compat. 934 ;; ctx = vars and their types (or or any props, denoted with any "sep") 935 ;; - each x in ctx is in scope for subsequent xs 936 ;; - ie, dont need separate ctx and tvctx 937 ;; - keep tvctx bc it's often useful to separate the returned Xs- 938 ;; TODO: infer currently tries to be generic over types and kinds 939 ;; but I'm not sure it properly generalizes 940 ;; eg, what if I need separate type-eval and kind-eval fns? 941 ;; - should infer be moved into define-syntax-category? 942 (define (infer es #:ctx [ctx null] #:tvctx [tvctx null] 943 #:tag [tag (current-tag)] ; the "type" to return from es 944 #:expa [expa expand/df] ; used to expand e 945 #:key [kev #'(current-type-eval)]) ; kind-eval (tvk in tvctx) 946 (syntax-parse ctx 947 [((~or X:id [x:id (~seq sep:id τ) ...]) ...) ; dont expand; τ may reference to tv 948 #:with (~or (~and (tv:id ...) 949 (~parse ([(tvsep ...) (tvk ...)] ...) 950 (stx-map (λ _ #'[(::) (#%type)]) #'(tv ...)))) 951 ([tv (~seq tvsep:id tvk) ...] ...)) 952 tvctx 953 #:with (e ...) es 954 #:with ((~literal #%plain-lambda) tvs+ 955 (~let*-syntax 956 ((~literal #%expression) 957 ((~literal #%plain-lambda) xs+ 958 (~let*-syntax 959 ((~literal #%expression) e+) ... (~literal void)))))) 960 (expa 961 #`(λ (tv ...) 962 (let*-syntax ([tv (make-rename-transformer 963 (mk-tyvar 964 (attachs #'tv '(tvsep ...) #'(tvk ...) 965 #:ev #,kev)))] ...) 966 (λ (X ... x ...) 967 (let*-syntax ([X (make-variable-like-transformer 968 (mk-tyvar (attach #'X ':: (#,kev #'#%type))))] ... 969 [x (make-variable-like-transformer 970 ((current-var-assign) 971 #'x 972 '(sep ...) 973 #'(τ ...)))] ...) 974 (#%expression e) ... void))))) 975 (list #'tvs+ #'xs+ 976 #'(e+ ...) 977 (stx-map (λ (e) (detach e tag)) #'(e+ ...)))] 978 [([x τ] ...) (infer es #:ctx #`([x #,tag τ] ...) #:tvctx tvctx #:tag tag)])) 979 980 ;; fns derived from infer --------------------------------------------------- 981 ;; some are syntactic shortcuts, some are for backwards compat 982 983 ;; shorter names 984 ; ctx = type env for bound vars in term e, etc 985 ; can also use for bound tyvars in type e 986 (define (infer/ctx+erase ctx e #:tag [tag (current-tag)]) 987 (syntax-parse (infer (list e) #:ctx ctx #:tag tag) 988 [(_ xs (e+) (τ)) (list #'xs #'e+ #'τ)])) 989 (define (infers/ctx+erase ctx es #:tag [tag (current-tag)]) 990 (stx-cdr (infer es #:ctx ctx #:tag tag))) 991 ; tyctx = kind env for bound type vars in term e 992 (define (infer/tyctx+erase ctx e #:tag [tag (current-tag)]) 993 (syntax-parse (infer (list e) #:tvctx ctx #:tag tag) 994 [(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)])) 995 (define (infers/tyctx+erase ctx es #:tag [tag (current-tag)]) 996 (syntax-parse (infer es #:tvctx ctx #:tag tag) 997 [(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)])) 998 (define infer/tyctx infer/tyctx+erase) 999 (define infer/ctx infer/ctx+erase) 1000 1001 (define current-promote (make-parameter (λ (t) t))) 1002 1003 ;; term expansion 1004 ;; expand/df : Syntax -> Syntax 1005 ;; Local expands the given syntax object. 1006 ;; The result always has a type (ie, a ': stx-prop). 1007 ;; Note: 1008 ;; local-expand must expand all the way down, ie stop-ids == null 1009 ;; If stop-ids is #f, then subexpressions won't get expanded and thus won't 1010 ;; get assigned a type. 1011 (define (expand/df e) 1012 (local-expand e 'expression null)) 1013 1014 ;; TODO: move these into define-syntax-category? 1015 ;; typecheck-fail-msg/1 : Type Type Stx -> String 1016 (define (typecheck-fail-msg/1 τ_expected τ_given expression) 1017 (format "type mismatch: expected ~a, given ~a\n expression: ~s" 1018 (type->str τ_expected) 1019 (or (and (syntax-e τ_given) (type->str τ_given)) 1020 "an invalid expression") 1021 (syntax->datum (get-orig expression)))) 1022 1023 ;; typecheck-fail-msg/1/no-expr : Type Type Stx -> String 1024 (define (typecheck-fail-msg/1/no-expr τ_expected τ_given) 1025 (format "type mismatch: expected ~a, given ~a" 1026 (type->str τ_expected) 1027 (type->str τ_given))) 1028 1029 ;; typecheck-fail-msg/multi : (Stx-Listof Type) (Stx-Listof Type) (Stx-Listof Stx) -> String 1030 (define (typecheck-fail-msg/multi τs_expected τs_given expressions) 1031 (format (string-append "type mismatch\n" 1032 " expected: ~a\n" 1033 " given: ~a\n" 1034 " expressions: ~a") 1035 (string-join (stx-map type->str τs_expected) ", ") 1036 (string-join (stx-map type->str τs_given) ", ") 1037 (string-join (map ~s (stx-map syntax->datum expressions)) ", "))) 1038 1039 ;; typecheck-fail-msg/multi/no-exprs : (Stx-Listof Type) (Stx-Listof Type) -> String 1040 (define (typecheck-fail-msg/multi/no-exprs τs_expected τs_given) 1041 (format (string-append "type mismatch\n" 1042 " expected: ~a\n" 1043 " given: ~a") 1044 (string-join (stx-map type->str τs_expected) ", ") 1045 (string-join (stx-map type->str τs_given) ", "))) 1046 1047 ;; no-expected-type-fail-msg : -> String 1048 (define (no-expected-type-fail-msg) 1049 "no expected type, add annotations") 1050 1051 ;; num-args-fail-msg : Stx (Stx-Listof Type) (Stx-Listof Stx) -> String 1052 (define (num-args-fail-msg fn τs_expected arguments) 1053 (format (string-append "~s: wrong number of arguments: expected ~a, given ~a\n" 1054 " expected: ~a\n" 1055 " arguments: ~a") 1056 (syntax->datum (get-orig fn)) 1057 (stx-length τs_expected) (stx-length arguments) 1058 (string-join (stx-map type->str τs_expected) ", ") 1059 (string-join (map ~s (map syntax->datum (stx-map get-orig arguments))) ", "))) 1060 1061 (struct exn:fail:type:check exn:fail:user ()) 1062 (struct exn:fail:type:infer exn:fail:user ()) 1063 1064 ;; TODO: deprecate this? can we rely on stx-parse instead? 1065 ;; type-error #:src Syntax #:msg String Syntax ... 1066 ;; usage: 1067 ;; type-error #:src src-stx 1068 ;; #:msg msg-string msg-args ... 1069 (define-simple-macro (type-error #:src stx-src #:msg msg args ...) 1070 #:with contmarks (syntax/loc this-syntax (current-continuation-marks)) 1071 (raise 1072 (exn:fail:type:check 1073 (format (string-append "TYPE-ERROR: ~a (~a:~a): " msg) 1074 (syntax-source stx-src) (syntax-line stx-src) (syntax-column stx-src) 1075 (type->str args) ...) 1076 contmarks)))) 1077 1078 (begin-for-syntax 1079 ; surface type syntax is saved as the value of the 'orig property 1080 ; used to report error msgs 1081 (define (add-orig stx orig) 1082 (define origs (or (syntax-property orig 'orig) null)) 1083 (set-stx-prop/preserved stx 'orig (cons orig origs))) 1084 (define (get-orig τ) 1085 (car (reverse (or (syntax-property τ 'orig) (list τ))))) 1086 (define (pass-orig stx orig) 1087 (add-orig stx (get-orig orig))) 1088 (define (has-orig? stx) 1089 (and (syntax-property stx 'orig) #true)) 1090 (define (type->str ty) 1091 (define τ (get-orig ty)) 1092 (cond 1093 [(identifier? τ) (symbol->string (syntax->datum τ))] 1094 [(stx-list? τ) (string-join (stx-map type->str τ) 1095 #:before-first "(" 1096 #:after-last ")")] 1097 [else (format "~s" (syntax->datum τ))])) 1098 (define (types->str tys #:sep [sep ", "]) 1099 (string-join (stx-map type->str tys) sep))) 1100 1101 (begin-for-syntax 1102 (define (brace? stx) 1103 (define paren-shape/#f (syntax-property stx 'paren-shape)) 1104 (and paren-shape/#f (char=? paren-shape/#f #\{))) 1105 (define (brack? stx) 1106 (define paren-shape/#f (syntax-property stx 'paren-shape)) 1107 (and paren-shape/#f (char=? paren-shape/#f #\[))) 1108 1109 (define (iff b1 b2) 1110 (boolean=? b1 b2)) 1111 1112 ;; Variance is (variance Boolean Boolean) 1113 (struct variance (covariant? contravariant?) #:prefab) 1114 (define irrelevant (variance #true #true)) 1115 (define covariant (variance #true #false)) 1116 (define contravariant (variance #false #true)) 1117 (define invariant (variance #false #false)) 1118 ;; variance-irrelevant? : Variance -> Boolean 1119 (define (variance-irrelevant? v) 1120 (and (variance-covariant? v) (variance-contravariant? v))) 1121 ;; variance-invariant? : Variance -> Boolean 1122 (define (variance-invariant? v) 1123 (and (not (variance-covariant? v)) (not (variance-contravariant? v)))) 1124 ;; variance-join : Variance Variance -> Variance 1125 (define (variance-join v1 v2) 1126 (variance (and (variance-covariant? v1) 1127 (variance-covariant? v2)) 1128 (and (variance-contravariant? v1) 1129 (variance-contravariant? v2)))) 1130 ;; variance-compose : Variance Variance -> Variance 1131 (define (variance-compose v1 v2) 1132 (variance (or (variance-irrelevant? v1) 1133 (variance-irrelevant? v2) 1134 (and (variance-covariant? v1) (variance-covariant? v2)) 1135 (and (variance-contravariant? v1) (variance-contravariant? v2))) 1136 (or (variance-irrelevant? v1) 1137 (variance-irrelevant? v2) 1138 (and (variance-covariant? v1) (variance-contravariant? v2)) 1139 (and (variance-contravariant? v1) (variance-covariant? v2))))) 1140 1141 ;; add-arg-variances : Id (Listof Variance) -> Id 1142 ;; Takes a type constructor id and adds variance information about the arguments. 1143 (define (add-arg-variances id arg-variances) 1144 (set-stx-prop/preserved id 'arg-variances arg-variances)) 1145 ;; get-arg-variances : Id -> (U False (Listof Variance)) 1146 ;; Takes a type constructor id and gets the argument variance information. 1147 (define (get-arg-variances id) 1148 (syntax-property id 'arg-variances)) 1149 1150 ;; todo: abstract out the common shape of a type constructor, 1151 ;; i.e., the repeated pattern code in the functions below 1152 (define (get-extra-info t) 1153 (syntax-parse t 1154 [((~literal #%plain-app) internal-id 1155 ((~literal #%plain-lambda) bvs 1156 ((~literal #%expression) ((~literal quote) extra-info-macro)) . tys)) 1157 (expand/df #'(extra-info-macro . tys))] 1158 [_ #f])) 1159 ;; gets the internal id in a type representation 1160 (define (get-type-tag t) 1161 (syntax-parse t 1162 [((~literal #%plain-app) tycons . _) #'tycons] 1163 [X:id #'X] 1164 [_ (type-error #:src t #:msg "Can't get internal id: ~a" t)])) 1165 (define (get-type-tags ts) 1166 (stx-map get-type-tag ts))) 1167 1168 ; substitution 1169 (begin-for-syntax 1170 (define-syntax ~Any/bvs ; matches any tycon 1171 (pattern-expander 1172 (syntax-parser 1173 [(_ tycons bvs . rst) 1174 #'(~and ty 1175 (~parse 1176 ((~literal #%plain-app) tycons 1177 ((~literal #%plain-lambda) bvs 1178 skipped-extra-info . rst)) 1179 ((current-promote) #'ty)))]))) 1180 (define-syntax ~Any 1181 (pattern-expander 1182 (syntax-parser 1183 [(_ tycons . rst) 1184 #'(~Any/bvs tycons _ . rst)]))) 1185 (define-syntax ~literal/else 1186 (pattern-expander 1187 (syntax-parser 1188 [(_ lit:id fail-msg:expr stx) 1189 #'(~and actual 1190 (~parse 1191 (~fail #:unless (and (identifier? #'actual) 1192 (free-identifier=? #'actual #'lit)) 1193 fail-msg) 1194 stx))]))) 1195 (define (merge-type-tags stx) ;; TODO: merge other tags? 1196 (define t (syntax-property stx ':)) 1197 (or (and (pair? t) 1198 (identifier? (car t)) (identifier? (cdr t)) 1199 (free-identifier=? (car t) (cdr t)) 1200 (set-stx-prop/preserved stx ': (car t))) 1201 stx)) 1202 ; subst τ for y in e, if (bound-id=? x y) 1203 (define (subst τ x e [cmp bound-identifier=?]) 1204 (syntax-parse e 1205 [y:id 1206 #:when (cmp e x) 1207 (transfer-stx-props τ (merge-type-tags (syntax-track-origin τ e e)))] 1208 [(esub ...) 1209 #:with res (stx-map (λ (e1) (subst τ x e1 cmp)) #'(esub ...)) 1210 (transfer-stx-props #'res e #:ctx e)] 1211 [_ e])) 1212 1213 (define (substs τs xs e [cmp bound-identifier=?]) 1214 (stx-fold (lambda (ty x res) (subst ty x res cmp)) e τs xs))) 1215 1216 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1217 1218 (module+ test 1219 (begin-for-syntax 1220 (test-case "variance-join" 1221 (test-case "joining with irrelevant doesn't change it" 1222 (check-equal? (variance-join irrelevant irrelevant) irrelevant) 1223 (check-equal? (variance-join irrelevant covariant) covariant) 1224 (check-equal? (variance-join irrelevant contravariant) contravariant) 1225 (check-equal? (variance-join irrelevant invariant) invariant)) 1226 (test-case "joining with invariant results in invariant" 1227 (check-equal? (variance-join invariant irrelevant) invariant) 1228 (check-equal? (variance-join invariant covariant) invariant) 1229 (check-equal? (variance-join invariant contravariant) invariant) 1230 (check-equal? (variance-join invariant invariant) invariant)) 1231 (test-case "joining a with a results in a" 1232 (check-equal? (variance-join irrelevant irrelevant) irrelevant) 1233 (check-equal? (variance-join covariant covariant) covariant) 1234 (check-equal? (variance-join contravariant contravariant) contravariant) 1235 (check-equal? (variance-join invariant invariant) invariant)) 1236 (test-case "joining covariant with contravariant results in invariant" 1237 (check-equal? (variance-join covariant contravariant) invariant) 1238 (check-equal? (variance-join contravariant covariant) invariant))) 1239 (test-case "variance-compose" 1240 (test-case "composing with covariant doesn't change it" 1241 (check-equal? (variance-compose covariant irrelevant) irrelevant) 1242 (check-equal? (variance-compose covariant covariant) covariant) 1243 (check-equal? (variance-compose covariant contravariant) contravariant) 1244 (check-equal? (variance-compose covariant invariant) invariant)) 1245 (test-case "composing with irrelevant results in irrelevant" 1246 (check-equal? (variance-compose irrelevant irrelevant) irrelevant) 1247 (check-equal? (variance-compose irrelevant covariant) irrelevant) 1248 (check-equal? (variance-compose irrelevant contravariant) irrelevant) 1249 (check-equal? (variance-compose irrelevant invariant) irrelevant)) 1250 (test-case "otherwise composing with invariant results in invariant" 1251 (check-equal? (variance-compose invariant covariant) invariant) 1252 (check-equal? (variance-compose invariant contravariant) invariant) 1253 (check-equal? (variance-compose invariant invariant) invariant)) 1254 (test-case "composing with with contravariant flips covariant and contravariant" 1255 (check-equal? (variance-compose contravariant covariant) contravariant) 1256 (check-equal? (variance-compose contravariant contravariant) covariant) 1257 (check-equal? (variance-compose contravariant irrelevant) irrelevant) 1258 (check-equal? (variance-compose contravariant invariant) invariant))) 1259 ))