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