mlish.rkt (59031B)
1 #lang s-exp macrotypes/typecheck 2 (require 3 (postfix-in - racket/fixnum) 4 (postfix-in - racket/flonum) 5 (for-syntax macrotypes/type-constraints macrotypes/variance-constraints)) 6 7 (extends 8 "ext-stlc.rkt" 9 #:except → define #%app λ #%datum begin 10 + - * void = zero? sub1 add1 not let let* and 11 #:rename [~→ ~ext-stlc:→]) 12 (reuse inst #:from "sysf.rkt") 13 (require (only-in "ext-stlc.rkt" → →?)) 14 (require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ)) 15 (reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt") 16 (require (only-in "stlc+rec-iso.rkt" ~× ×?)) 17 (provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum])) 18 (reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt") 19 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil))) 20 (require (only-in "stlc+cons.rkt" ~List List? List)) 21 (reuse ref deref := Ref #:from "stlc+box.rkt") 22 (require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×) 23 [tup rec] [proj get] [× ××])) 24 (provide rec get ××) 25 ;; for pattern matching 26 (require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list))) 27 (require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup))) 28 29 ;; ML-like language 30 ;; - top level recursive functions 31 ;; - user-definable algebraic datatypes 32 ;; - pattern matching 33 ;; - (local) type inference 34 35 (module+ test 36 (require (for-syntax rackunit))) 37 38 (provide define-type 39 → →/test 40 ; redefine these to use lifted → 41 (typed-out [+ : (→ Int Int Int)] 42 [- : (→ Int Int Int)] 43 [* : (→ Int Int Int)] 44 [max : (→ Int Int Int)] 45 [min : (→ Int Int Int)] 46 [void : (→ Unit)] 47 [= : (→ Int Int Bool)] 48 [<= : (→ Int Int Bool)] 49 [< : (→ Int Int Bool)] 50 [> : (→ Int Int Bool)] 51 [modulo : (→ Int Int Int)] 52 [zero? : (→ Int Bool)] 53 [sub1 : (→ Int Int)] 54 [add1 : (→ Int Int)] 55 [not : (→ Bool Bool)] 56 [abs : (→ Int Int)] 57 [even? : (→ Int Bool)] 58 [odd? : (→ Int Bool)]) 59 define match match2 λ 60 (rename-out [mlish:#%app #%app]) 61 cond when unless 62 Channel make-channel channel-get channel-put 63 Thread thread 64 List Vector 65 vector make-vector vector-length vector-ref vector-set! vector-copy! 66 Sequence in-range in-naturals in-vector in-list in-lines 67 for for* 68 for/list for/vector for*/vector for*/list for/fold for/hash for/sum 69 printf format display displayln list->vector 70 let let* begin 71 Hash in-hash hash hash-set! hash-ref hash-has-key? hash-count 72 String-Port Input-Port 73 write-string string-length string-copy! 74 quotient+remainder 75 set! 76 provide-type 77 (rename-out [mlish-provide provide]) 78 require-typed 79 Regexp 80 equal? 81 read) 82 83 ;; creating possibly polymorphic types 84 ;; ?∀ only wraps a type in a forall if there's at least one type variable 85 (define-syntax ?∀ 86 (lambda (stx) 87 (syntax-case stx () 88 [(?∀ () body) 89 #'body] 90 [(?∀ (X ...) body) 91 #'(∀ (X ...) body)]))) 92 93 ;; ?Λ only wraps an expression in a Λ if there's at least one type variable 94 (define-syntax ?Λ 95 (lambda (stx) 96 (syntax-case stx () 97 [(?Λ () body) 98 #'body] 99 [(?Λ (X ...) body) 100 #'(Λ (X ...) body)]))) 101 102 (begin-for-syntax 103 ;; matching possibly polymorphic types 104 (define-syntax ~?∀ 105 (pattern-expander 106 (lambda (stx) 107 (syntax-case stx () 108 [(?∀ vars-pat body-pat) 109 #'(~or (~∀ vars-pat body-pat) 110 (~and (~not (~∀ _ _)) 111 (~parse vars-pat #'()) 112 body-pat))])))) 113 114 ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id) 115 ;; finds the free Xs in the type 116 (define (find-free-Xs Xs ty) 117 (for/list ([X (in-list (stx->list Xs))] 118 #:when (stx-contains-id? ty X)) 119 X)) 120 121 ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args 122 ;; stx = the application stx = (#%app e_fn e_arg ...) 123 ;; tyXs = input and output types from fn type 124 ;; ie (typeof e_fn) = (-> . tyXs) 125 ;; It infers the types of arguments from left-to-right, 126 ;; and it expands and returns all of the arguments. 127 ;; It returns list of 3 values if successful, else throws a type error 128 ;; - a list of all the arguments, expanded 129 ;; - a list of all the type variables 130 ;; - the constraints for substituting the types 131 (define (solve Xs tyXs stx) 132 (syntax-parse tyXs 133 [(τ_inX ... τ_outX) 134 ;; generate initial constraints with expected type and τ_outX 135 #:with (~?∀ Vs expected-ty) (and (get-expected-type stx) 136 ((current-type-eval) (get-expected-type stx))) 137 (define initial-cs 138 (if (and (syntax-e #'expected-ty) (stx-null? #'Vs)) 139 (add-constraints Xs '() (list (list #'expected-ty #'τ_outX))) 140 '())) 141 (syntax-parse stx 142 [(_ e_fn . args) 143 (define-values (as- cs) 144 (for/fold ([as- null] [cs initial-cs]) 145 ([a (in-list (syntax->list #'args))] 146 [tyXin (in-list (syntax->list #'(τ_inX ...)))]) 147 (define ty_in (inst-type/cs Xs cs tyXin)) 148 (define/with-syntax [a- ty_a] 149 (infer+erase (if (empty? (find-free-Xs Xs ty_in)) 150 (add-expected-ty a ty_in) 151 a))) 152 (values 153 (cons #'a- as-) 154 (add-constraints Xs cs (list (list ty_in #'ty_a)) 155 (list (list (inst-type/cs/orig 156 Xs cs ty_in 157 (λ (id1 id2) 158 (equal? (syntax->datum id1) 159 (syntax->datum id2)))) 160 #'ty_a)))))) 161 162 (list (reverse as-) Xs cs)])])) 163 164 (define (raise-app-poly-infer-error stx expected-tys given-tys e_fn) 165 (type-error #:src stx 166 #:msg (format 167 (string-append 168 "Could not infer instantiation of polymorphic function ~s.\n" 169 " expected: ~a\n" 170 " given: ~a") 171 (syntax->datum (get-orig e_fn)) 172 (string-join (stx-map type->str expected-tys) ", ") 173 (string-join (stx-map type->str given-tys) ", ")))) 174 175 ;; covariant-Xs? : Type -> Bool 176 ;; Takes a possibly polymorphic type, and returns true if all of the 177 ;; type variables are in covariant positions within the type, false 178 ;; otherwise. 179 (define (covariant-Xs? ty) 180 (syntax-parse ((current-type-eval) ty) 181 [(~?∀ Xs ty) 182 (for/and ([X (in-list (syntax->list #'Xs))]) 183 (covariant-X? X #'ty))])) 184 185 ;; find-X-variance : Id Type [Variance] -> Variance 186 ;; Returns the variance of X within the type ty 187 (define (find-X-variance X ty [ctxt-variance covariant]) 188 (match (find-variances (list X) ty ctxt-variance) 189 [(list variance) variance])) 190 191 ;; covariant-X? : Id Type -> Bool 192 ;; Returns true if every place X appears in ty is a covariant position, false otherwise. 193 (define (covariant-X? X ty) 194 (variance-covariant? (find-X-variance X ty covariant))) 195 196 ;; contravariant-X? : Id Type -> Bool 197 ;; Returns true if every place X appears in ty is a contravariant position, false otherwise. 198 (define (contravariant-X? X ty) 199 (variance-contravariant? (find-X-variance X ty covariant))) 200 201 ;; find-variances : (Listof Id) Type [Variance] -> (Listof Variance) 202 ;; Returns the variances of each of the Xs within the type ty, 203 ;; where it's already within a context represented by ctxt-variance. 204 (define (find-variances Xs ty [ctxt-variance covariant]) 205 (syntax-parse ty 206 [A:id 207 (for/list ([X (in-list Xs)]) 208 (cond [(free-identifier=? X #'A) ctxt-variance] 209 [else irrelevant]))] 210 [(~Any tycons) 211 (make-list (length Xs) irrelevant)] 212 [(~?∀ () (~Any tycons τ ...)) 213 #:when (get-arg-variances #'tycons) 214 #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons)) 215 (define τ-ctxt-variances 216 (for/list ([arg-variance (in-list (get-arg-variances #'tycons))]) 217 (variance-compose ctxt-variance arg-variance))) 218 (for/fold ([acc (make-list (length Xs) irrelevant)]) 219 ([τ (in-list (syntax->list #'[τ ...]))] 220 [τ-ctxt-variance (in-list τ-ctxt-variances)]) 221 (map variance-join 222 acc 223 (find-variances Xs τ τ-ctxt-variance)))] 224 [ty 225 #:when (not (for/or ([X (in-list Xs)]) 226 (stx-contains-id? #'ty X))) 227 (make-list (length Xs) irrelevant)] 228 [_ (make-list (length Xs) invariant)])) 229 230 ;; find-variances/exprs : (Listof Id) Type [Variance-Expr] -> (Listof Variance-Expr) 231 ;; Like find-variances, but works with Variance-Exprs instead of 232 ;; concrete variance values. 233 (define (find-variances/exprs Xs ty [ctxt-variance covariant]) 234 (syntax-parse ty 235 [A:id 236 (for/list ([X (in-list Xs)]) 237 (cond [(free-identifier=? X #'A) ctxt-variance] 238 [else irrelevant]))] 239 [(~Any tycons) 240 (make-list (length Xs) irrelevant)] 241 [(~?∀ () (~Any tycons τ ...)) 242 #:when (get-arg-variances #'tycons) 243 #:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons)) 244 (define τ-ctxt-variances 245 (for/list ([arg-variance (in-list (get-arg-variances #'tycons))]) 246 (variance-compose/expr ctxt-variance arg-variance))) 247 (for/fold ([acc (make-list (length Xs) irrelevant)]) 248 ([τ (in-list (syntax->list #'[τ ...]))] 249 [τ-ctxt-variance (in-list τ-ctxt-variances)]) 250 (map variance-join/expr 251 acc 252 (find-variances/exprs Xs τ τ-ctxt-variance)))] 253 [ty 254 #:when (not (for/or ([X (in-list Xs)]) 255 (stx-contains-id? #'ty X))) 256 (make-list (length Xs) irrelevant)] 257 [_ (make-list (length Xs) invariant)])) 258 259 ;; current-variance-constraints : (U False (Mutable-Setof Variance-Constraint)) 260 ;; If this is false, that means that infer-variances should return concrete Variance values. 261 ;; If it's a mutable set, that means that infer-variances should mutate it and return false, 262 ;; and type constructors should return the list of variance vars. 263 (define current-variance-constraints (make-parameter #false)) 264 265 ;; infer-variances : 266 ;; ((-> Stx) -> Stx) (Listof Variance-Var) (Listof Id) (Listof Type-Stx) 267 ;; -> (U False (Listof Variance)) 268 (define (infer-variances with-variance-vars-okay variance-vars Xs τs) 269 (cond 270 [(current-variance-constraints) 271 (define variance-constraints (current-variance-constraints)) 272 (define variance-exprs 273 (for/fold ([exprs (make-list (length variance-vars) irrelevant)]) 274 ([τ (in-list τs)]) 275 (define/syntax-parse (~?∀ Xs* τ*) 276 ;; This can mutate variance-constraints! 277 ;; This avoids causing an infinite loop by having the type 278 ;; constructors provide with-variance-vars-okay so that within 279 ;; this call they declare variance-vars for their variances. 280 (with-variance-vars-okay 281 (λ () ((current-type-eval) #`(∀ #,Xs #,τ))))) 282 (map variance-join/expr 283 exprs 284 (find-variances/exprs (syntax->list #'Xs*) #'τ* covariant)))) 285 (for ([var (in-list variance-vars)] 286 [expr (in-list variance-exprs)]) 287 (set-add! variance-constraints (variance= var expr))) 288 #f] 289 [else 290 (define variance-constraints (mutable-set)) 291 ;; This will mutate variance-constraints! 292 (parameterize ([current-variance-constraints variance-constraints]) 293 (infer-variances with-variance-vars-okay variance-vars Xs τs)) 294 (define mapping 295 (solve-variance-constraints variance-vars 296 (set->list variance-constraints) 297 (variance-mapping))) 298 (for/list ([var (in-list variance-vars)]) 299 (variance-mapping-ref mapping var))])) 300 301 ;; make-arg-variances-proc : 302 ;; (Listof Variance-Var) (Listof Id) (Listof Type-Stx) -> (Stx -> (U (Listof Variance) 303 ;; (Listof Variance-Var))) 304 (define (make-arg-variances-proc arg-variance-vars Xs τs) 305 ;; variance-vars-okay? : (Parameterof Boolean) 306 ;; A parameter that determines whether or not it's okay for 307 ;; this type constructor to return a list of Variance-Vars 308 ;; for the variances. 309 (define variance-vars-okay? (make-parameter #false)) 310 ;; with-variance-vars-okay : (-> A) -> A 311 (define (with-variance-vars-okay f) 312 (parameterize ([variance-vars-okay? #true]) 313 (f))) 314 ;; arg-variances : (Boxof (U False (List Variance ...))) 315 ;; If false, means that the arg variances have not been 316 ;; computed yet. Otherwise, stores the complete computed 317 ;; variances for the arguments to this type constructor. 318 (define arg-variances (box #f)) 319 ;; arg-variances-proc : Stx -> (U (Listof Variance) (Listof Variance-Var)) 320 (define (arg-variance-proc stx) 321 (or (unbox arg-variances) 322 (cond 323 [(variance-vars-okay?) 324 arg-variance-vars] 325 [else 326 (define inferred-variances 327 (infer-variances 328 with-variance-vars-okay 329 arg-variance-vars 330 Xs 331 τs)) 332 (cond [inferred-variances 333 (set-box! arg-variances inferred-variances) 334 inferred-variances] 335 [else 336 arg-variance-vars])]))) 337 arg-variance-proc) 338 339 ;; compute unbound tyvars in one unexpanded type ty 340 (define (compute-tyvar1 ty) 341 (syntax-parse ty 342 [X:id #'(X)] 343 [() #'()] 344 [(C t ...) (stx-appendmap compute-tyvar1 #'(t ...))])) 345 ;; computes unbound ids in (unexpanded) tys, to be used as tyvars 346 (define (compute-tyvars tys) 347 (define Xs (stx-appendmap compute-tyvar1 tys)) 348 (filter 349 (lambda (X) 350 (with-handlers 351 ([exn:fail:syntax:unbound? (lambda (e) #t)] 352 [exn:fail:type:infer? (lambda (e) #t)]) 353 (let ([X+ ((current-type-eval) X)]) 354 (not (or (tyvar? X+) (type? X+)))))) 355 (stx-remove-dups Xs)))) 356 357 ;; define -------------------------------------------------- 358 ;; for function defs, define infers type variables 359 ;; - since the order of the inferred type variables depends on expansion order, 360 ;; which is not known to programmers, to make the result slightly more 361 ;; intuitive, we arbitrarily sort the inferred tyvars lexicographically 362 (define-typed-syntax define 363 [(_ x:id e) 364 #:with (e- τ) (infer+erase #'e) 365 #:with y (generate-temporary) 366 #'(begin- 367 (define-syntax x (make-rename-transformer (⊢ y : τ))) 368 (define- y e-))] 369 ; explicit "forall" 370 [(_ Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) 371 e_body ... e) 372 #:when (brace? #'Ys) 373 ;; TODO; remove this code duplication 374 #:with g (add-orig (generate-temporary #'f) #'f) 375 #:with e_ann #'(add-expected e τ_out) 376 #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out)) 377 ;; TODO: check that specified return type is correct 378 ;; - currently cannot do it here; to do the check here, need all types of 379 ;; top-lvl fns, since they can call each other 380 #:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected))) 381 ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...))) 382 #`(begin- 383 (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected))) 384 (define- g 385 (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))] 386 ;; alternate type sig syntax, after parameter names 387 [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b) 388 #'(define (f [x : ty] ... -> ty_out) . b)] 389 [(_ (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) 390 e_body ... e) 391 #:with Ys (compute-tyvars #'(τ ... τ_out)) 392 #:with g (add-orig (generate-temporary #'f) #'f) 393 #:with e_ann #'(add-expected e τ_out) ; must be macro bc t_out may have unbound tvs 394 #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out)) 395 ;; TODO: check that specified return type is correct 396 ;; - currently cannot do it here; to do the check here, need all types of 397 ;; top-lvl fns, since they can call each other 398 #:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected))) 399 (set-stx-prop/preserved 400 ((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...))) 401 'orig 402 (list #'(→ τ+orig ...))) 403 #`(begin- 404 (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected))) 405 (define- g 406 (?Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]) 407 408 ;; define-type ----------------------------------------------- 409 ;; TODO: should validate τ as part of define-type definition (before it's used) 410 ;; - not completely possible, since some constructors may not be defined yet, 411 ;; ie, mutually recursive datatypes 412 ;; for now, validate types but punt if encountering unbound ids 413 (define-syntax (define-type stx) 414 (syntax-parse stx 415 [(define-type Name:id . rst) 416 #:with NewName (generate-temporary #'Name) 417 #:with Name2 (add-orig #'(NewName) #'Name) 418 #`(begin- 419 (define-type Name2 . #,(subst #'Name2 #'Name #'rst)) 420 (stlc+rec-iso:define-type-alias Name Name2))] 421 [(define-type (Name:id X:id ...) 422 ;; constructors must have the form (Cons τ ...) 423 ;; but the first ~or clause accepts 0-arg constructors as ids; 424 ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email) 425 (~and (~or (~and IdCons:id 426 (~parse (Cons [fld (~datum :) τ] ...) #'(IdCons))) 427 (Cons [fld (~datum :) τ] ...) 428 (~and (Cons τ ...) 429 (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...) 430 ;; validate tys 431 #:with (ty_flat ...) (stx-flatten #'((τ ...) ...)) 432 #:with (_ _ (_ _ (_ _ (_ _ ty+ ...)))) 433 (with-handlers 434 ([exn:fail:syntax:unbound? 435 (λ (e) 436 (define X (stx-car (exn:fail:syntax-exprs e))) 437 #`(lambda () (let-syntax () (let-syntax () (#%app void unbound)))))]) 438 (expand/df 439 #`(lambda (X ...) 440 (let-syntax 441 ([Name 442 (syntax-parser 443 [(_ X ...) (mk-type #'void)] 444 [stx 445 (type-error 446 #:src #'stx 447 #:msg 448 (format "Improper use of constructor ~a; expected ~a args, got ~a" 449 (syntax->datum #'Name) (stx-length #'(X ...)) 450 (stx-length (stx-cdr #'stx))))])] 451 [X (make-rename-transformer (mk-type #'X))] ...) 452 (void ty_flat ...))))) 453 #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...))) 454 (stx-map 455 (lambda (t+ t) (unless (type? t+) 456 (type-error #:src t 457 #:msg "~a is not a valid type" t))) 458 #'(ty+ ...) #'(ty_flat ...))) 459 #:with NameExpander (format-id #'Name "~~~a" #'Name) 460 #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name) 461 #:with (StructName ...) (generate-temporaries #'(Cons ...)) 462 #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) 463 #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) 464 #:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...)) 465 #:with ((exposed-acc ...) ...) 466 (stx-map 467 (λ (C fs) (stx-map (λ (f) (format-id C "~a-~a" C f)) fs)) 468 #'(Cons ...) #'((fld ...) ...)) 469 #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs)) 470 #'(StructName ...) #'((fld ...) ...)) 471 #:with (Cons? ...) (stx-map mk-? #'(StructName ...)) 472 #:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...)) 473 #`(begin- 474 (define-syntax (NameExtraInfo stx) 475 (syntax-parse stx 476 [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)])) 477 (begin-for-syntax 478 ;; arg-variance-vars : (List Variance-Var ...) 479 (define arg-variance-vars 480 (list (variance-var (syntax-e (generate-temporary 'X))) ...))) 481 (define-type-constructor Name 482 #:arity = #,(stx-length #'(X ...)) 483 #:arg-variances (make-arg-variances-proc arg-variance-vars 484 (list #'X ...) 485 (list #'τ ... ...)) 486 #:extra-info 'NameExtraInfo) 487 (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ... 488 (define-syntax (exposed-acc stx) ; accessor for records 489 (syntax-parse stx 490 [_:id (⊢ acc (?∀ (X ...) (ext-stlc:→ (Name X ...) τ)))] 491 [(o . rst) ; handle if used in fn position 492 #:with app (datum->syntax #'o '#%app) 493 #`(app 494 #,(assign-type #'acc #'(?∀ (X ...) (ext-stlc:→ (Name X ...) τ))) 495 . rst)])) ... ... 496 (define-syntax (exposed-Cons? stx) ; predicates for each variant 497 (syntax-parse stx 498 [_:id (⊢ Cons? (?∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))] 499 [(o . rst) ; handle if used in fn position 500 #:with app (datum->syntax #'o '#%app) 501 #`(app 502 #,(assign-type #'Cons? #'(?∀ (X ...) (ext-stlc:→ (Name X ...) Bool))) 503 . rst)])) ... 504 (define-syntax (Cons stx) 505 (syntax-parse stx 506 ; no args and not polymorphic 507 [C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)] 508 ; no args but polymorphic, check inferred type 509 [C:id 510 #:when (stx-null? #'(τ ...)) 511 #:with τ-expected (syntax-property #'C 'expected-type) 512 #:fail-unless (syntax-e #'τ-expected) 513 (raise 514 (exn:fail:type:infer 515 (format "~a (~a:~a): ~a: ~a" 516 (syntax-source stx) (syntax-line stx) (syntax-column stx) 517 (syntax-e #'C) 518 (no-expected-type-fail-msg)) 519 (current-continuation-marks))) 520 #:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected) 521 #'(C {τ-expected-arg (... ...)})] 522 [_:id (⊢ StructName (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))] ; HO fn 523 [(C τs e_arg ...) 524 #:when (brace? #'τs) ; commit to this clause 525 #:with {~! τ_X:type (... ...)} #'τs 526 #:with (τ_in:type (... ...)) ; instantiated types 527 (stx-map 528 (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t)) 529 #'(τ ...)) 530 #:with ([e_arg- τ_arg] ...) 531 (stx-map 532 (λ (e τ_e) 533 (infer+erase (set-stx-prop/preserved e 'expected-type τ_e))) 534 #'(e_arg ...) #'(τ_in.norm (... ...))) 535 #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...))) 536 (typecheck-fail-msg/multi #'(τ_in.norm (... ...)) #'(τ_arg ...) #'(e_arg ...)) 537 (⊢ (StructName e_arg- ...) : (Name τ_X (... ...)))] 538 [(C . args) ; no type annotations, must infer instantiation 539 #:with StructName/ty 540 (set-stx-prop/preserved 541 (⊢ StructName : (?∀ (X ...) (ext-stlc:→ τ ... (Name X ...)))) 542 'orig 543 (list #'C)) 544 ; stx/loc transfers expected-type 545 (syntax/loc stx (mlish:#%app StructName/ty . args))])) 546 ...)])) 547 548 ;; match -------------------------------------------------- 549 (begin-for-syntax 550 (define (get-ctx pat ty) 551 (unify-pat+ty (list pat ty))) 552 (define (unify-pat+ty pat+ty) 553 (syntax-parse pat+ty 554 [(pat ty) #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens) 555 (syntax-parse #'pat 556 [{(~datum _)} #'()] 557 [{(~literal stlc+cons:nil)} #'()] 558 [{A:id} ; disambiguate 0-arity constructors (that don't need parens) 559 #:when (get-extra-info #'ty) 560 #'()] 561 ;; comma tup syntax always has parens 562 [{(~and ps (p1 (unq p) ...))} 563 #:when (not (stx-null? #'(p ...))) 564 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 565 (unify-pat+ty #'(ps ty))] 566 [{p ...} 567 (unify-pat+ty #'((p ...) ty))])] ; pair 568 [((~datum _) ty) #'()] 569 [((~or (~literal stlc+cons:nil)) ty) #'()] 570 [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens) 571 #:with (_ (_ (_ C) . _) ...) (get-extra-info #'ty) 572 #:when (member (syntax->datum #'A) (syntax->datum #'(C ...))) 573 #'()] 574 [(x:id ty) #'((x ty))] 575 [((p1 (unq p) ...) ty) ; comma tup stx 576 #:when (not (stx-null? #'(p ...))) 577 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 578 #:with (~× t ...) #'ty 579 #:with (pp ...) #'(p1 p ...) 580 (unifys #'([pp t] ...))] 581 [(((~literal stlc+tup:tup) p ...) ty) ; tup 582 #:with (~× t ...) #'ty 583 (unifys #'([p t] ...))] 584 [(((~literal stlc+cons:list) p ...) ty) ; known length list 585 #:with (~List t) #'ty 586 (unifys #'([p t] ...))] 587 [(((~seq p (~datum ::)) ... rst) ty) ; nicer cons stx 588 #:with (~List t) #'ty 589 (unifys #'([p t] ... [rst ty]))] 590 [(((~literal stlc+cons:cons) p ps) ty) ; arb length list 591 #:with (~List t) #'ty 592 (unifys #'([p t] [ps ty]))] 593 [((Name p ...) ty) 594 #:with (_ (_ Cons) _ _ [_ _ τ] ...) 595 (stx-findf 596 (syntax-parser 597 [(_ 'C . rst) 598 (equal? (syntax->datum #'Name) (syntax->datum #'C))]) 599 (stx-cdr (get-extra-info #'ty))) 600 (unifys #'([p τ] ...))] 601 [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t)) 602 #'()])) 603 (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys)) 604 605 (define (compile-pat p ty) 606 (syntax-parse p 607 [pat #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens) 608 (syntax-parse #'pat 609 [{(~datum _)} #'_] 610 [{(~literal stlc+cons:nil)} (syntax/loc p (list))] 611 [{A:id} ; disambiguate 0-arity constructors (that don't need parens) 612 #:when (get-extra-info ty) 613 (compile-pat #'(A) ty)] 614 ;; comma tup stx always has parens 615 [{(~and ps (p1 (unq p) ...))} 616 #:when (not (stx-null? #'(p ...))) 617 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 618 (compile-pat #'ps ty)] 619 [{pat ...} (compile-pat (syntax/loc p (pat ...)) ty)])] 620 [(~datum _) #'_] 621 [(~literal stlc+cons:nil) ; nil 622 #'(list)] 623 [A:id ; disambiguate 0-arity constructors (that don't need parens) 624 #:with (_ (_ (_ C) . _) ...) (get-extra-info ty) 625 #:when (member (syntax->datum #'A) (syntax->datum #'(C ...))) 626 (compile-pat #'(A) ty)] 627 [x:id p] 628 [(p1 (unq p) ...) ; comma tup stx 629 #:when (not (stx-null? #'(p ...))) 630 #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...))) 631 #:with (~× t ...) ty 632 #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'(p1 p ...) #'(t ...)) 633 #'(list p- ...)] 634 [((~literal stlc+tup:tup) . pats) 635 #:with (~× . tys) ty 636 #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'pats #'tys) 637 (syntax/loc p (list p- ...))] 638 [((~literal stlc+cons:list) . ps) 639 #:with (~List t) ty 640 #:with (p- ...) (stx-map (lambda (p) (compile-pat p #'t)) #'ps) 641 (syntax/loc p (list p- ...))] 642 [((~seq pat (~datum ::)) ... last) ; nicer cons stx 643 #:with (~List t) ty 644 #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(pat ...)) 645 #:with last- (compile-pat #'last ty) 646 (syntax/loc p (list-rest p- ... last-))] 647 [((~literal stlc+cons:cons) p ps) 648 #:with (~List t) ty 649 #:with p- (compile-pat #'p #'t) 650 #:with ps- (compile-pat #'ps ty) 651 #'(cons p- ps-)] 652 [(Name . pats) 653 #:with (_ (_ Cons) (_ StructName) _ [_ _ τ] ...) 654 (stx-findf 655 (syntax-parser 656 [(_ 'C . rst) 657 (equal? (syntax->datum #'Name) (syntax->datum #'C))]) 658 (stx-cdr (get-extra-info ty))) 659 #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...)) 660 (syntax/loc p (StructName p- ...))])) 661 662 ;; pats = compiled pats = racket pats 663 (define (check-exhaust pats ty) 664 (define (else-pat? p) 665 (syntax-parse p [(~literal _) #t] [_ #f])) 666 (define (nil-pat? p) 667 (syntax-parse p 668 [((~literal list)) #t] 669 [_ #f])) 670 (define (non-nil-pat? p) 671 (syntax-parse p 672 [((~literal list-rest) . rst) #t] 673 [((~literal cons) . rst) #t] 674 [_ #f])) 675 (define (tup-pat? p) 676 (syntax-parse p 677 [((~literal list) . _) #t] [_ #f])) 678 (cond 679 [(or (stx-ormap else-pat? pats) (stx-ormap identifier? pats)) #t] 680 [(List? ty) ; lists 681 (unless (stx-ormap nil-pat? pats) 682 (error 'match2 (let ([last (car (stx-rev pats))]) 683 (format "(~a:~a) missing nil clause for list expression" 684 (syntax-line last) (syntax-column last))))) 685 (unless (stx-ormap non-nil-pat? pats) 686 (error 'match2 (let ([last (car (stx-rev pats))]) 687 (format "(~a:~a) missing clause for non-empty, arbitrary length list" 688 (syntax-line last) (syntax-column last))))) 689 #t] 690 [(×? ty) ; tuples 691 (unless (stx-ormap tup-pat? pats) 692 (error 'match2 (let ([last (car (stx-rev pats))]) 693 (format "(~a:~a) missing pattern for tuple expression" 694 (syntax-line last) (syntax-column last))))) 695 (syntax-parse pats 696 [((_ p ...) ...) 697 (syntax-parse ty 698 [(~× t ...) 699 (apply stx-andmap 700 (lambda (t . ps) (check-exhaust ps t)) 701 #'(t ...) 702 (syntax->list #'((p ...) ...)))])])] 703 [else ; algebraic datatypes 704 (syntax-parse (get-extra-info ty) 705 [(_ (_ (_ C) (_ Cstruct) . rst) ...) 706 (syntax-parse pats 707 [((Cpat _ ...) ...) 708 (define Cs (syntax->datum #'(C ...))) 709 (define Cstructs (syntax->datum #'(Cstruct ...))) 710 (define Cpats (syntax->datum #'(Cpat ...))) 711 (unless (set=? Cstructs Cpats) 712 (error 'match2 713 (let ([last (car (stx-rev pats))]) 714 (format "(~a:~a) clauses not exhaustive; missing: ~a" 715 (syntax-line last) (syntax-column last) 716 (string-join 717 (for/list ([C Cs][Cstr Cstructs] #:unless (member Cstr Cpats)) 718 (symbol->string C)) 719 ", "))))) 720 #t])] 721 [_ #t])])) 722 723 ;; TODO: do get-ctx and compile-pat in one pass 724 (define (compile-pats pats ty) 725 (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats)) 726 ) 727 728 (define-syntax (match2 stx) 729 (syntax-parse stx #:datum-literals (with) 730 [(_ e with . clauses) 731 #:fail-when (null? (syntax->list #'clauses)) "no clauses" 732 #:with [e- τ_e] (infer+erase #'e) 733 (syntax-parse #'clauses #:datum-literals (->) 734 [([(~seq p ...) -> e_body] ...) 735 #:with (pat ...) (stx-map ; use brace to indicate root pattern 736 (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})])) 737 #'((p ...) ...)) 738 #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e) 739 #:with ty-expected (get-expected-type stx) 740 #:with ([(x- ...) e_body- ty_body] ...) 741 (stx-map 742 infer/ctx+erase 743 #'(ctx ...) #'((add-expected e_body ty-expected) ...)) 744 #:when (check-exhaust #'(pat- ...) #'τ_e) 745 (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : (⊔ ty_body ...)) 746 ])])) 747 748 (define-typed-syntax match #:datum-literals (with) 749 [(_ e with . clauses) 750 #:fail-when (null? (syntax->list #'clauses)) "no clauses" 751 #:with [e- τ_e] (infer+erase #'e) 752 #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type 753 (cond 754 [(×? #'τ_e) ;; e is tuple 755 (syntax-parse #'clauses #:datum-literals (->) 756 [([x ... -> e_body]) 757 #:with (~× ty ...) #'τ_e 758 #:fail-unless (stx-length=? #'(ty ...) #'(x ...)) 759 "match clause pattern not compatible with given tuple" 760 #:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...) 761 #'(add-expected e_body t_expect)) 762 #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))]) 763 #`(lambda- (s) (list-ref- s #,(datum->syntax #'here i)))) 764 #:with z (generate-temporary) 765 (⊢ (let- ([z e-]) 766 (let- ([x- (acc z)] ...) e_body-)) 767 : ty_body)])] 768 [(List? #'τ_e) ;; e is List 769 (syntax-parse #'clauses #:datum-literals (-> ::) 770 [([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary))) 771 (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'()))) 772 -> e_body] ...+) 773 #:fail-unless (stx-ormap 774 (lambda (xx) (and (brack? xx) (zero? (stx-length xx)))) 775 #'(xs ...)) 776 "match: missing empty list case" 777 #:fail-when (and (stx-andmap brack? #'(xs ...)) 778 (= 1 (stx-length #'(xs ...)))) 779 "match: missing non-empty list case" 780 #:with (~List ty) #'τ_e 781 #:with ([(x- ... rst-) e_body- ty_body] ...) 782 (stx-map (lambda (ctx e) (infer/ctx+erase ctx e)) 783 #'(([x ty] ... [rst (List ty)]) ...) #'((add-expected e_body t_expect) ...)) 784 #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...)) 785 #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...)) 786 #:with (pred? ...) (stx-map 787 (lambda (l lo) #`(λ- (lst) (#,lo (length- lst) #,l))) 788 #'(len ...) #'(lenop ...)) 789 #:with ((acc1 ...) ...) (stx-map 790 (lambda (xs) 791 (for/list ([(x i) (in-indexed (syntax->list xs))]) 792 #`(lambda- (lst) (list-ref- lst #,(datum->syntax #'here i))))) 793 #'((x ...) ...)) 794 #:with (acc2 ...) (stx-map (lambda (l) #`(lambda- (lst) (list-tail- lst #,l))) #'(len ...)) 795 (⊢ (let- ([z e-]) 796 (cond- 797 [(pred? z) 798 (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...)) 799 : (⊔ ty_body ...))])] 800 [else ;; e is variant 801 (syntax-parse #'clauses #:datum-literals (->) 802 [([Clause:id x:id ... 803 (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)])) 804 -> e_c_un] ...+) ; un = unannotated with expected ty 805 ;; length #'clauses may be > length #'info, due to guards 806 #:with info-body (get-extra-info #'τ_e) 807 #:with (_ (_ (_ ConsAll) . _) ...) #'info-body 808 #:fail-unless (set=? (syntax->datum #'(Clause ...)) 809 (syntax->datum #'(ConsAll ...))) 810 (type-error #:src stx 811 #:msg (string-append 812 "match: clauses not exhaustive; missing: " 813 (string-join 814 (map symbol->string 815 (set-subtract 816 (syntax->datum #'(ConsAll ...)) 817 (syntax->datum #'(Clause ...)))) 818 ", "))) 819 #:with ((_ _ _ Cons? [_ acc τ] ...) ...) 820 (map ; ok to compare symbols since clause names can't be rebound 821 (lambda (Cl) 822 (stx-findf 823 (syntax-parser 824 [(_ 'C . rst) (equal? Cl (syntax->datum #'C))]) 825 (stx-cdr #'info-body))) ; drop leading #%app 826 (syntax->datum #'(Clause ...))) 827 ;; this commented block experiments with expanding to unsafe ops 828 ;; #:with ((acc ...) ...) (stx-map 829 ;; (lambda (accs) 830 ;; (for/list ([(a i) (in-indexed (syntax->list accs))]) 831 ;; #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i))))) 832 ;; #'((acc-fn ...) ...)) 833 #:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...)) 834 #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...) 835 (stx-map 836 (λ (bs eg+ec) (infers/ctx+erase bs eg+ec)) 837 #'(([x : τ] ...) ...) #'((e_guard e_c) ...)) 838 #:fail-unless (and (same-types? #'(τ_guard ...)) 839 (Bool? (stx-car #'(τ_guard ...)))) 840 "guard expression(s) must have type bool" 841 #:with z (generate-temporary) ; dont duplicate eval of test expr 842 (⊢ (let- ([z e-]) 843 (cond- 844 [(and- (Cons? z) 845 (let- ([x- (acc z)] ...) e_guard-)) 846 (let- ([x- (acc z)] ...) e_c-)] ...)) 847 : (⊔ τ_ec ...))])])]) 848 849 ; special arrow that computes free vars; for use with tests 850 ; (because we can't write explicit forall 851 (define-syntax →/test 852 (syntax-parser 853 [(→/test (~and Xs (X:id ...)) . rst) 854 #:when (brace? #'Xs) 855 #'(?∀ (X ...) (ext-stlc:→ . rst))] 856 [(→/test . rst) 857 #:with Xs (compute-tyvars #'rst) 858 #'(?∀ Xs (ext-stlc:→ . rst))])) 859 860 ; all λs have type (?∀ (X ...) (→ τ_in ... τ_out)) 861 (define-typed-syntax λ 862 [(_ (x:id ...) body) 863 #:with (~?∀ Xs expected) (get-expected-type stx) 864 #:fail-unless (→? #'expected) 865 (no-expected-type-fail-msg) 866 #:with (~ext-stlc:→ arg-ty ... body-ty) #'expected 867 #:fail-unless (stx-length=? #'[x ...] #'[arg-ty ...]) 868 (format "expected a function of ~a arguments, got one with ~a arguments" 869 (stx-length #'[arg-ty ...]) (stx-length #'[x ...])) 870 #`(?Λ Xs (ext-stlc:λ ([x : arg-ty] ...) (add-expected body body-ty)))] 871 [(_ (~and args ([_ (~datum :) ty] ...)) body) 872 #:with (~?∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx) 873 #`(?Λ () (ext-stlc:λ args (add-expected body body-ty)))] 874 [(_ (~and x+tys ([_ (~datum :) ty] ...)) . body) 875 #:with Xs (compute-tyvars #'(ty ...)) 876 ;; TODO is there a way to have λs that refer to ids defined after them? 877 #'(?Λ Xs (ext-stlc:λ x+tys . body))]) 878 879 880 ;; #%app -------------------------------------------------- 881 (define-typed-syntax mlish:#%app 882 [(_ e_fn . e_args) 883 ;; compute fn type (ie ∀ and →) 884 #:with [e_fn- (~?∀ Xs (~ext-stlc:→ . tyX_args))] (infer+erase #'e_fn) 885 ;; solve for type variables Xs 886 #:with [(e_arg- ...) Xs* cs] (solve #'Xs #'tyX_args stx) 887 ;; instantiate polymorphic function type 888 #:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args) 889 #:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out) 890 ;; arity check 891 #:fail-unless (stx-length=? #'(τ_in ...) #'e_args) 892 (num-args-fail-msg #'e_fn #'(τ_in ...) #'e_args) 893 ;; compute argument types 894 #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...)) 895 ;; typecheck args 896 #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) 897 (typecheck-fail-msg/multi #'(τ_in ...) #'(τ_arg ...) #'e_args) 898 #:with τ_out* (if (stx-null? #'(unsolved-X ...)) 899 #'τ_out 900 (syntax-parse #'τ_out 901 [(~?∀ (Y ...) τ_out) 902 (unless (→? #'τ_out) 903 (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)) 904 (for ([X (in-list (syntax->list #'(unsolved-X ...)))]) 905 (unless (covariant-X? X #'τ_out) 906 (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))) 907 #'(∀ (unsolved-X ... Y ...) τ_out)])) 908 (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)]) 909 910 911 ;; cond and other conditionals 912 (define-typed-syntax cond 913 [(_ [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t))) 914 test) 915 b ... body] ...+) 916 #:with (test- ...) (⇑s (test ...) as Bool) 917 #:with ty-expected (get-expected-type stx) 918 #:with ([body- ty_body] ...) (infers+erase #'((add-expected body ty-expected) ...)) 919 #:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...)) 920 (⊢ (cond- [test- b- ... body-] ...) : (⊔ ty_body ...))]) 921 (define-typed-syntax when 922 [(_ test body ...) 923 ; #:with test- (⇑ test as Bool) 924 #:with [test- _] (infer+erase #'test) 925 #:with [(body- _) ...] (infers+erase #'(body ...)) 926 (⊢ (when- test- body- ... (void-)) : Unit)]) 927 (define-typed-syntax unless 928 [(_ test body ...) 929 ; #:with test- (⇑ test as Bool) 930 #:with [test- _] (infer+erase #'test) 931 #:with [(body- _) ...] (infers+erase #'(body ...)) 932 (⊢ (unless- test- body- ... (void-)) : Unit)]) 933 934 ;; sync channels and threads 935 (define-type-constructor Channel) 936 937 (define-typed-syntax make-channel 938 [(_ (~and tys {ty})) 939 #:when (brace? #'tys) 940 (⊢ (make-channel-) : (Channel ty))]) 941 (define-typed-syntax channel-get 942 [(_ c) 943 #:with [c- (~Channel ty)] (infer+erase #'c) 944 (⊢ (channel-get- c-) : ty)]) 945 (define-typed-syntax channel-put 946 [(_ c v) 947 #:with [c- (~Channel ty)] (infer+erase #'c) 948 #:with [v- ty_v] (infer+erase #'v) 949 #:fail-unless (typechecks? #'ty_v #'ty) 950 (typecheck-fail-msg/1 #'ty #'ty_v #'v) 951 (⊢ (channel-put- c- v-) : Unit)]) 952 953 (define-base-type Thread) 954 955 ;; threads 956 (define-typed-syntax thread 957 [(_ th) 958 #:with (th- (~?∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th) 959 (⊢ (thread- th-) : Thread)]) 960 961 (provide (typed-out [random : (→ Int Int)] 962 [integer->char : (→ Int Char)] 963 [string->list : (→ String (List Char))] 964 [string->number : (→ String Int)])) 965 (define-typed-syntax number->string 966 [f:id (assign-type #'number->string- #'(→ Int String))] 967 [(_ n) 968 #'(number->string n (ext-stlc:#%datum . 10))] 969 [(_ n rad) 970 #:with args- (⇑s (n rad) as Int) 971 (⊢ (number->string- . args-) : String)]) 972 (provide number->string string-append 973 (typed-out [string : (→ Char String)] 974 [sleep : (→ Int Unit)] 975 [string=? : (→ String String Bool)] 976 [string<=? : (→ String String Bool)])) 977 978 (define-typed-syntax string-append 979 [(_ . strs) 980 #:with strs- (⇑s strs as String) 981 (⊢ (string-append- . strs-) : String)]) 982 983 ;; vectors 984 (define-type-constructor Vector) 985 986 (define-typed-syntax vector 987 [(_ (~and tys {ty})) 988 #:when (brace? #'tys) 989 (⊢ (vector-) : (Vector ty))] 990 [(_ v ...) 991 #:with ([v- ty] ...) (infers+erase #'(v ...)) 992 #:when (same-types? #'(ty ...)) 993 #:with one-ty (stx-car #'(ty ...)) 994 (⊢ (vector- v- ...) : (Vector one-ty))]) 995 (define-typed-syntax make-vector 996 [(_ n) #'(make-vector n (ext-stlc:#%datum . 0))] 997 [(_ n e) 998 #:with n- (⇑ n as Int) 999 #:with [e- ty] (infer+erase #'e) 1000 (⊢ (make-vector- n- e-) : (Vector ty))]) 1001 (define-typed-syntax vector-length 1002 [(_ e) 1003 #:with [e- _] (⇑ e as Vector) 1004 (⊢ (vector-length- e-) : Int)]) 1005 (define-typed-syntax vector-ref 1006 [(_ e n) 1007 #:with n- (⇑ n as Int) 1008 #:with [e- (ty)] (⇑ e as Vector) 1009 (⊢ (vector-ref- e- n-) : ty)]) 1010 (define-typed-syntax vector-set! 1011 [(_ e n v) 1012 #:with n- (⇑ n as Int) 1013 #:with [e- (~Vector ty)] (infer+erase #'e) 1014 #:with [v- ty_v] (infer+erase #'v) 1015 #:fail-unless (typecheck? #'ty_v #'ty) 1016 (typecheck-fail-msg/1 #'ty #'ty_v #'v) 1017 (⊢ (vector-set!- e- n- v-) : Unit)]) 1018 (define-typed-syntax vector-copy! 1019 [(_ dest start src) 1020 #:with start- (⇑ start as Int) 1021 #:with [dest- (~Vector ty_dest)] (infer+erase #'dest) 1022 #:with [src- (~Vector ty_src)] (infer+erase #'src) 1023 #:fail-unless (typecheck? #'ty_dest #'ty_src) 1024 (typecheck-fail-msg/1 1025 #'(Vector ty_src) #'(Vector ty_dest) #'dest) 1026 (⊢ (vector-copy!- dest- start- src-) : Unit)]) 1027 1028 1029 ;; sequences and for loops 1030 1031 (define-type-constructor Sequence) 1032 1033 (define-typed-syntax in-range 1034 [(_ end) 1035 #'(in-range (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))] 1036 [(_ start end) 1037 #'(in-range start end (ext-stlc:#%datum . 1))] 1038 [(_ start end step) 1039 #:with (e- ...) (⇑s (start end step) as Int) 1040 (⊢ (in-range- e- ...) : (Sequence Int))]) 1041 1042 (define-typed-syntax in-naturals 1043 [(in-naturals) #'(in-naturals (ext-stlc:#%datum . 0))] 1044 [(in-naturals start) 1045 #:with start- (⇑ start as Int) 1046 (⊢ (in-naturals- start-) : (Sequence Int))]) 1047 1048 1049 (define-typed-syntax in-vector 1050 [(in-vector e) 1051 #:with [e- (ty)] (⇑ e as Vector) 1052 (⊢ (in-vector- e-) : (Sequence ty))]) 1053 1054 (define-typed-syntax in-list 1055 [(in-list e) 1056 #:with [e- (ty)] (⇑ e as List) 1057 (⊢ (in-list- e-) : (Sequence ty))]) 1058 1059 (define-typed-syntax in-lines 1060 [(in-lines e) 1061 #:with e- (⇑ e as String) 1062 (⊢ (in-lines- (open-input-string e-)) : (Sequence String))]) 1063 1064 (define-typed-syntax for 1065 [(for ([x:id e]...) b ... body) 1066 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1067 #:with [(x- ...) (b- ... body-) (ty_b ... ty_body)] 1068 (infers/ctx+erase #'([x : ty] ...) #'(b ... body)) 1069 (⊢ (for- ([x- e-] ...) b- ... body-) : Unit)]) 1070 (define-typed-syntax for* 1071 [(for* ([x:id e]...) body) 1072 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1073 #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) 1074 (⊢ (for*- ([x- e-] ...) body-) : Unit)]) 1075 1076 (define-typed-syntax for/list 1077 [(for/list ([x:id e]...) body) 1078 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1079 #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) 1080 (⊢ (for/list- ([x- e-] ...) body-) : (List ty_body))]) 1081 (define-typed-syntax for/vector 1082 [(for/vector ([x:id e]...) body) 1083 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1084 #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) 1085 (⊢ (for/vector- ([x- e-] ...) body-) : (Vector ty_body))]) 1086 (define-typed-syntax for*/vector 1087 [(for*/vector ([x:id e]...) body) 1088 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1089 #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) 1090 (⊢ (for*/vector- ([x- e-] ...) body-) : (Vector ty_body))]) 1091 (define-typed-syntax for*/list 1092 [(for*/list ([x:id e]...) body) 1093 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1094 #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body) 1095 (⊢ (for*/list- ([x- e-] ...) body-) : (List ty_body))]) 1096 (define-typed-syntax for/fold 1097 [(for/fold ([acc init]) ([x:id e] ...) body) 1098 #:with [init- ty_init] (infer+erase #`(pass-expected init #,stx)) 1099 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1100 #:with [(acc- x- ...) body- ty_body] 1101 (infer/ctx+erase #'([acc : ty_init][x : ty] ...) #'body) 1102 #:fail-unless (typecheck? #'ty_body #'ty_init) 1103 (typecheck-fail-msg/1 #'ty_init #'ty_body #'body) 1104 (⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-) : ty_body)]) 1105 1106 (define-typed-syntax for/hash 1107 [(for/hash ([x:id e]...) body) 1108 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1109 #:with [(x- ...) body- (~× ty_k ty_v)] 1110 (infer/ctx+erase #'([x : ty] ...) #'body) 1111 (⊢ (for/hash- ([x- e-] ...) 1112 (let- ([t body-]) 1113 (values- (car- t) (cadr- t)))) 1114 : (Hash ty_k ty_v))]) 1115 1116 (define-typed-syntax for/sum 1117 [(for/sum ([x:id e]... 1118 (~optional (~seq #:when guard) #:defaults ([guard #'#t]))) 1119 body) 1120 #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence) 1121 #:with [(x- ...) (guard- body-) (_ ty_body)] 1122 (infers/ctx+erase #'([x : ty] ...) #'(guard body)) 1123 #:when (Int? #'ty_body) 1124 (⊢ (for/sum- ([x- e-] ... #:when guard-) body-) : Int)]) 1125 1126 ; printing and displaying 1127 (define-typed-syntax printf 1128 [(printf str e ...) 1129 #:with s- (⇑ str as String) 1130 #:with ([e- ty] ...) (infers+erase #'(e ...)) 1131 (⊢ (printf- s- e- ...) : Unit)]) 1132 (define-typed-syntax format 1133 [(format str e ...) 1134 #:with s- (⇑ str as String) 1135 #:with ([e- ty] ...) (infers+erase #'(e ...)) 1136 (⊢ (format- s- e- ...) : String)]) 1137 (define-typed-syntax display 1138 [(display e) 1139 #:with [e- _] (infer+erase #'e) 1140 (⊢ (display- e-) : Unit)]) 1141 (define-typed-syntax displayln 1142 [(displayln e) 1143 #:with [e- _] (infer+erase #'e) 1144 (⊢ (displayln- e-) : Unit)]) 1145 (provide (typed-out [newline : (→ Unit)])) 1146 1147 (define-typed-syntax list->vector 1148 [(list->vector e) 1149 #:with [e- (ty)] (⇑ e as List) 1150 (⊢ (list->vector- e-) : (Vector ty))]) 1151 1152 (define-typed-syntax let 1153 [(let name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body) 1154 #:with ([e- ty_e] ...) (infers+erase #'(e ...)) 1155 #:with [(name- . xs-) (body- ...) (_ ... ty_body)] 1156 (infers/ctx+erase #'([name : (→ ty_e ... ty.norm)][x : ty_e] ...) 1157 #'(b ... body)) 1158 #:fail-unless (typecheck? #'ty_body #'ty.norm) 1159 (format "type of let body ~a does not match expected typed ~a" 1160 (type->str #'ty_body) (type->str #'ty)) 1161 (⊢ (letrec- ([name- (λ- xs- body- ...)]) 1162 (name- e- ...)) 1163 : ty_body)] 1164 [(let ([x:id e] ...) body ...) 1165 #'(ext-stlc:let ([x e] ...) (begin body ...))]) 1166 (define-typed-syntax let* 1167 [(let* ([x:id e] ...) body ...) 1168 #'(ext-stlc:let* ([x e] ...) (begin body ...))]) 1169 1170 (define-typed-syntax begin 1171 [(begin body ... b) 1172 #:with expected (get-expected-type stx) 1173 #:with b_ann #'(add-expected b expected) 1174 #'(ext-stlc:begin body ... b_ann)]) 1175 1176 ;; hash 1177 (define-type-constructor Hash #:arity = 2) 1178 1179 (define-typed-syntax in-hash 1180 [(in-hash e) 1181 #:with [e- (ty_k ty_v)] (⇑ e as Hash) 1182 (⊢ (hash-map- e- list-) 1183 : (Sequence (stlc+rec-iso:× ty_k ty_v)))]) 1184 1185 ; mutable hashes 1186 (define-typed-syntax hash 1187 [(hash (~and tys {ty_key ty_val})) 1188 #:when (brace? #'tys) 1189 (⊢ (make-hash-) : (Hash ty_key ty_val))] 1190 [(hash (~seq k v) ...) 1191 #:with ([k- ty_k] ...) (infers+erase #'(k ...)) 1192 #:with ([v- ty_v] ...) (infers+erase #'(v ...)) 1193 #:when (same-types? #'(ty_k ...)) 1194 #:when (same-types? #'(ty_v ...)) 1195 #:with ty_key (stx-car #'(ty_k ...)) 1196 #:with ty_val (stx-car #'(ty_v ...)) 1197 (⊢ (make-hash- (list- (cons- k- v-) ...)) : (Hash ty_key ty_val))]) 1198 (define-typed-syntax hash-set! 1199 [(hash-set! h k v) 1200 #:with [h- (~Hash ty_key ty_val)] (infer+erase #'h) 1201 #:with [k- ty_k] (infer+erase #'k) 1202 #:with [v- ty_v] (infer+erase #'v) 1203 #:fail-unless (typecheck? #'ty_k #'ty_key) (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) 1204 #:fail-unless (typecheck? #'ty_v #'ty_val) (typecheck-fail-msg/1 #'ty_val #'ty_v #'v) 1205 (⊢ (hash-set!- h- k- v-) : Unit)]) 1206 (define-typed-syntax hash-ref 1207 [(hash-ref h k) 1208 #:with [h- (~Hash ty_key ty_val)] (infer+erase #'h) 1209 #:with [k- ty_k] (infer+erase #'k) 1210 #:fail-unless (typecheck? #'ty_k #'ty_key) 1211 (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) 1212 (⊢ (hash-ref- h- k-) : ty_val)] 1213 [(hash-ref h k fail) 1214 #:with [h- (~Hash ty_key ty_val)] (infer+erase #'h) 1215 #:with [k- ty_k] (infer+erase #'k) 1216 #:fail-unless (typecheck? #'ty_k #'ty_key) 1217 (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) 1218 #:with [fail- (~?∀ () (~ext-stlc:→ ty_fail))] (infer+erase #'fail) 1219 #:fail-unless (typecheck? #'ty_fail #'ty_val) 1220 (typecheck-fail-msg/1 #'(→ ty_val) #'(→ ty_fail) #'fail) 1221 (⊢ (hash-ref- h- k- fail-) : ty_val)]) 1222 (define-typed-syntax hash-has-key? 1223 [(hash-has-key? h k) 1224 #:with [h- (~Hash ty_key _)] (infer+erase #'h) 1225 #:with [k- ty_k] (infer+erase #'k) 1226 #:fail-unless (typecheck? #'ty_k #'ty_key) 1227 (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) 1228 (⊢ (hash-has-key?- h- k-) : Bool)]) 1229 1230 (define-typed-syntax hash-count 1231 [(hash-count h) 1232 #:with [h- _] (⇑ h as Hash) 1233 (⊢ (hash-count- h-) : Int)]) 1234 1235 (define-base-type String-Port) 1236 (define-base-type Input-Port) 1237 (provide (typed-out [open-output-string : (→ String-Port)] 1238 [get-output-string : (→ String-Port String)] 1239 [string-upcase : (→ String String)])) 1240 1241 (define-typed-syntax write-string 1242 [(write-string str out) 1243 #'(write-string str out (ext-stlc:#%datum . 0) (string-length str))] 1244 [(write-string str out start end) 1245 #:with str- (⇑ str as String) 1246 #:with out- (⇑ out as String-Port) 1247 #:with start- (⇑ start as Int) 1248 #:with end- (⇑ end as Int) 1249 (⊢ (begin- (write-string- str- out- start- end-) (void-)) : Unit)]) 1250 1251 (define-typed-syntax string-length 1252 [(string-length str) 1253 #:with str- (⇑ str as String) 1254 (⊢ (string-length- str-) : Int)]) 1255 (provide (typed-out [make-string : (→ Int String)] 1256 [string-set! : (→ String Int Char Unit)] 1257 [string-ref : (→ String Int Char)])) 1258 (define-typed-syntax string-copy! 1259 [(string-copy! dest dest-start src) 1260 #'(string-copy! 1261 dest dest-start src (ext-stlc:#%datum . 0) (string-length src))] 1262 [(string-copy! dest dest-start src src-start src-end) 1263 #:with dest- (⇑ dest as String) 1264 #:with src- (⇑ src as String) 1265 #:with dest-start- (⇑ dest-start as Int) 1266 #:with src-start- (⇑ src-start as Int) 1267 #:with src-end- (⇑ src-end as Int) 1268 (⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) : Unit)]) 1269 1270 (provide (typed-out [fl+ : (→ Float Float Float)] 1271 [fl- : (→ Float Float Float)] 1272 [fl* : (→ Float Float Float)] 1273 [fl/ : (→ Float Float Float)] 1274 [flsqrt : (→ Float Float)] 1275 [flceiling : (→ Float Float)] 1276 [inexact->exact : (→ Float Int)] 1277 [exact->inexact : (→ Int Float)] 1278 [char->integer : (→ Char Int)] 1279 [real->decimal-string : (→ Float Int String)] 1280 [fx->fl : (→ Int Float)])) 1281 (define-typed-syntax quotient+remainder 1282 [(quotient+remainder x y) 1283 #:with x- (⇑ x as Int) 1284 #:with y- (⇑ y as Int) 1285 (⊢ (let-values- ([[a b] (quotient/remainder- x- y-)]) 1286 (list- a b)) 1287 : (stlc+rec-iso:× Int Int))]) 1288 (provide (typed-out [quotient : (→ Int Int Int)])) 1289 1290 (define-typed-syntax set! 1291 [(set! x:id e) 1292 #:with [x- ty_x] (infer+erase #'x) 1293 #:with [e- ty_e] (infer+erase #'e) 1294 #:fail-unless (typecheck? #'ty_e #'ty_x) 1295 (typecheck-fail-msg/1 #'ty_x #'ty_e #'e) 1296 (⊢ (set!- x e-) : Unit)]) 1297 1298 (define-typed-syntax provide-type [(provide-type ty ...) #'(provide- ty ...)]) 1299 1300 (define-typed-syntax mlish-provide 1301 [(provide x:id ...) 1302 #:with ([x- ty_x] ...) (infers+erase #'(x ...)) 1303 ; TODO: use hash-code to generate this tmp 1304 #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...)) 1305 #'(begin- 1306 (provide- x ...) 1307 (stlc+rec-iso:define-type-alias x-ty ty_x) ... 1308 (provide- x-ty ...))]) 1309 (define-typed-syntax require-typed 1310 [(require-typed x:id ... #:from mod) 1311 #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...)) 1312 #:with (y ...) (generate-temporaries #'(x ...)) 1313 #'(begin- 1314 (require- (rename-in- (only-in- mod x ... x-ty ...) [x y] ...)) 1315 (define-syntax x (make-rename-transformer (assign-type #'y #'x-ty))) ...)]) 1316 1317 (define-base-type Regexp) 1318 (provide (typed-out [regexp-match : (→ Regexp String (List String))] 1319 [regexp : (→ String Regexp)])) 1320 1321 (define-typed-syntax equal? 1322 [(equal? e1 e2) 1323 #:with [e1- ty1] (infer+erase #'e1) 1324 #:with [e2- ty2] (infer+erase #'(add-expected e2 ty1)) 1325 #:fail-unless (typecheck? #'ty1 #'ty2) "arguments to equal? have different types" 1326 (⊢ (equal?- e1- e2-) : Bool)]) 1327 1328 (define-typed-syntax read 1329 [(read) 1330 (⊢ (let- ([x (read-)]) 1331 (cond- [(eof-object?- x) ""] 1332 [(number?- x) (number->string- x)] 1333 [(symbol?- x) (symbol->string- x)])) : String)]) 1334 1335 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1336 1337 (module+ test 1338 (begin-for-syntax 1339 (check-true (covariant-Xs? #'Int)) 1340 (check-true (covariant-Xs? #'(stlc+box:Ref Int))) 1341 (check-true (covariant-Xs? #'(→ Int Int))) 1342 (check-true (covariant-Xs? #'(∀ (X) X))) 1343 (check-false (covariant-Xs? #'(∀ (X) (stlc+box:Ref X)))) 1344 (check-false (covariant-Xs? #'(∀ (X) (→ X X)))) 1345 (check-false (covariant-Xs? #'(∀ (X) (→ X Int)))) 1346 (check-true (covariant-Xs? #'(∀ (X) (→ Int X)))) 1347 (check-true (covariant-Xs? #'(∀ (X) (→ (→ X Int) X)))) 1348 (check-false (covariant-Xs? #'(∀ (X) (→ (→ (→ X Int) Int) X)))) 1349 (check-false (covariant-Xs? #'(∀ (X) (→ (stlc+box:Ref X) Int)))) 1350 (check-false (covariant-Xs? #'(∀ (X Y) (→ X Y)))) 1351 (check-true (covariant-Xs? #'(∀ (X Y) (→ (→ X Int) Y)))) 1352 (check-false (covariant-Xs? #'(∀ (X Y) (→ (→ X Int) (→ Y Int))))) 1353 (check-true (covariant-Xs? #'(∀ (X Y) (→ (→ X Int) (→ Int Y))))) 1354 (check-false (covariant-Xs? #'(∀ (A B) (→ (→ Int (stlc+rec-iso:× A B)) 1355 (→ String (stlc+rec-iso:× A B)) 1356 (stlc+rec-iso:× A B))))) 1357 (check-true (covariant-Xs? #'(∀ (A B) (→ (→ (stlc+rec-iso:× A B) Int) 1358 (→ (stlc+rec-iso:× A B) String) 1359 (stlc+rec-iso:× A B))))) 1360 ))