mlish-tests.rkt (27847B)
1 #lang s-exp "../mlish.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 ;; match on tups 5 (check-type 6 (match (tup 1 2) with 7 [x y -> (+ x y)]) 8 : Int -> 3) 9 10 ;; tests more or less copied from infer-tests.rkt ------------------------------ 11 (typecheck-fail (λ (x) x) #:with-msg "λ: no expected type, add annotations") 12 13 ;; top-level defines 14 (define (f [x : Int] → Int) x) 15 (typecheck-fail (f 1 2) #:with-msg "f: wrong number of arguments: expected 1, given 2") 16 (check-type f : (→ Int Int)) 17 (check-type (f 1) : Int ⇒ 1) 18 (typecheck-fail (f (λ ([x : Int]) x))) 19 20 (define (g [x : X] → X) x) 21 (check-type g : (→/test X X)) 22 23 ;; (inferred) polymorpic instantiation 24 (check-type (g 1) : Int ⇒ 1) 25 (check-type (g #f) : Bool ⇒ #f) ; different instantiation 26 (check-type (g add1) : (→ Int Int)) 27 (check-type (g +) : (→ Int Int Int)) 28 29 ;; function polymorphic in list element 30 (define-type (List X) 31 Nil 32 (Cons X (List X))) 33 34 ;; arity err 35 (typecheck-fail (Cons 1) #:with-msg "Cons: wrong number of arguments: expected 2, given 1") 36 37 ;; type err 38 (typecheck-fail (Cons 1 1) 39 #:with-msg "expected: \\(List Int\\)\n *given: Int") 40 41 (typecheck-fail 42 (match (Cons 1 Nil) with 43 [Nil -> 1]) 44 #:with-msg "match: clauses not exhaustive; missing: Cons") 45 (typecheck-fail 46 (match (Cons 1 Nil) with 47 [Cons x xs -> 1]) 48 #:with-msg "match: clauses not exhaustive; missing: Nil") 49 50 (define (g2 [lst : (List Y)] → (List Y)) lst) 51 (check-type g2 : (→/test (List Y) (List Y))) 52 (typecheck-fail (g2 1) 53 #:with-msg 54 "expected: \\(List Y\\)\n *given: Int") 55 56 ;; todo? allow polymorphic nil? 57 (check-type (g2 (Nil {Int})) : (List Int) ⇒ (Nil {Int})) 58 (check-type (g2 (Nil {Bool})) : (List Bool) ⇒ (Nil {Bool})) 59 (check-type (g2 (Nil {(List Int)})) : (List (List Int)) ⇒ (Nil {(List Int)})) 60 (check-type (g2 (Nil {(→ Int Int)})) : (List (→ Int Int)) ⇒ (Nil {(List (→ Int Int))})) 61 ;; annotations unneeded: same as tests above, but without annotations 62 (check-type (g2 Nil) : (List Int) ⇒ Nil) 63 (check-type (g2 Nil) : (List Bool) ⇒ Nil) 64 (check-type (g2 Nil) : (List (List Int)) ⇒ Nil) 65 (check-type (g2 Nil) : (List (→ Int Int)) ⇒ Nil) 66 67 (check-type (g2 (Cons 1 Nil)) : (List Int) ⇒ (Cons 1 Nil)) 68 (check-type (g2 (Cons "1" Nil)) : (List String) ⇒ (Cons "1" Nil)) 69 70 ;; mlish cant type this fn (ie, incomplete cases on variant --- what to put for Nil case?) 71 ;(define (g3 [lst : (List X)] → X) (hd lst)) 72 ;(check-type g3 : (→ {X} (List X) X)) 73 ;(check-type g3 : (→ {A} (List A) A)) 74 ;(check-not-type g3 : (→ {A B} (List A) B)) 75 ;(typecheck-fail (g3) #:with-msg "Expected.+arguments with type.+List") ; TODO: more precise err msg 76 ;(check-type (g3 (nil {Int})) : Int) ; runtime fail 77 ;(check-type (g3 (nil {Bool})) : Bool) ; runtime fail 78 ;(check-type (g3 (cons 1 nil)) : Int ⇒ 1) 79 ;(check-type (g3 (cons "1" nil)) : String ⇒ "1") 80 81 ;; recursive fn 82 (define (recf [x : Int] → Int) (recf x)) 83 (check-type recf : (→ Int Int)) 84 85 (define (countdown [x : Int] → Int) 86 (if (zero? x) 87 0 88 (countdown (sub1 x)))) 89 (check-type (countdown 0) : Int ⇒ 0) 90 (check-type (countdown 10) : Int ⇒ 0) 91 (typecheck-fail (countdown "10") #:with-msg "expected: Int\n *given: String") 92 93 ;; list fns ---------- 94 95 ; map: tests whether match and define properly propagate 'expected-type 96 (define (map [f : (→ X Y)] [lst : (List X)] → (List Y)) 97 (match lst with 98 [Nil -> Nil] 99 [Cons x xs -> (Cons (f x) (map f xs))])) 100 (check-type map : (→/test (→ X Y) (List X) (List Y))) 101 (check-type map : (→/test {Y X} (→ Y X) (List Y) (List X))) 102 (check-type map : (→/test (→ A B) (List A) (List B))) 103 (check-not-type map : (→/test (→ A B) (List B) (List A))) 104 (check-not-type map : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar 105 106 ; nil without annotation; tests fn-first, left-to-right arg inference 107 ; does work yet, need to add left-to-right inference in #%app 108 (check-type (map add1 Nil) : (List Int) ⇒ Nil) 109 (check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil)))) 110 : (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil)))) 111 (typecheck-fail (map add1 (Cons "1" Nil)) 112 #:with-msg "expected: Int\n *given: String") 113 (check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil)))) 114 : (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil)))) 115 ;; ; doesnt work yet: all lambdas need annotations 116 ;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5)) 117 118 (define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X)) 119 (match lst with 120 [Nil -> Nil] 121 [Cons x xs -> (if (p? x) 122 (Cons x (filter p? xs)) 123 (filter p? xs))])) 124 (define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X)) 125 (match lst with 126 [Nil -> Nil] 127 [Cons x xs #:when (p? x) -> (Cons x (filter p? xs))] 128 [Cons x xs -> (filter p? xs)])) 129 (check-type (filter zero? Nil) : (List Int) ⇒ Nil) 130 (check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 131 : (List Int) ⇒ Nil) 132 (check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 133 : (List Int) ⇒ (Cons 0 Nil)) 134 (check-type (filter (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil)))) 135 : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) 136 (check-type (filter/guard zero? Nil) : (List Int) ⇒ Nil) 137 (check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) 138 : (List Int) ⇒ Nil) 139 (check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) 140 : (List Int) ⇒ (Cons 0 Nil)) 141 (check-type 142 (filter/guard (λ (x) (not (zero? x))) (Cons 0 (Cons 1 (Cons 2 Nil)))) 143 : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) 144 ; doesnt work yet: all lambdas need annotations 145 ;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2)) 146 147 (define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y) 148 (match lst with 149 [Nil -> base] 150 [Cons x xs -> (f x (foldr f base xs))])) 151 (define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y) 152 (match lst with 153 [Nil -> acc] 154 [Cons x xs -> (foldr f (f x acc) xs)])) 155 156 (define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool) 157 (match lst with 158 [Nil -> #t] 159 [Cons x xs #:when (p? x) -> (all? p? xs)] 160 [Cons x xs -> #f])) 161 162 (define (tails [lst : (List X)] → (List (List X))) 163 (match lst with 164 [Nil -> (Cons Nil Nil)] 165 [Cons x xs -> (Cons lst (tails xs))])) 166 167 (define (build-list [n : Int] [f : (→ Int X)] → (List X)) 168 (if (zero? (sub1 n)) 169 (Cons (f 0) Nil) 170 (Cons (f (sub1 n)) (build-list (sub1 n) f)))) 171 (check-type (build-list 1 add1) : (List Int) ⇒ (Cons 1 Nil)) 172 (check-type (build-list 3 add1) : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil)))) 173 (check-type (build-list 5 sub1) 174 : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil)))))) 175 (check-type (build-list 5 (λ (x) (add1 (add1 x)))) 176 : (List Int) ⇒ (Cons 6 (Cons 5 (Cons 4 (Cons 3 (Cons 2 Nil)))))) 177 178 (define (build-list/comp [i : Int] [n : Int] [nf : (→ Int Int)] [f : (→ Int X)] → (List X)) 179 (if (= i n) 180 Nil 181 (Cons (f (nf i)) (build-list/comp (add1 i) n nf f)))) 182 183 (define built-list-1 (build-list/comp 0 3 (λ (x) (* 2 x)) add1)) 184 (define built-list-2 (build-list/comp 0 3 (λ (x) (* 2 x)) number->string)) 185 (check-type built-list-1 : (List Int) -> (Cons 1 (Cons 3 (Cons 5 Nil)))) 186 (check-type built-list-2 : (List String) -> (Cons "0" (Cons "2" (Cons "4" Nil)))) 187 188 (define (~>2 [a : A] [f : (→ A A)] [g : (→ A B)] → B) 189 (g (f a))) 190 191 (define ~>2-result-1 (~>2 1 (λ (x) (* 2 x)) add1)) 192 (define ~>2-result-2 (~>2 1 (λ (x) (* 2 x)) number->string)) 193 (check-type ~>2-result-1 : Int -> 3) 194 (check-type ~>2-result-2 : String -> "2") 195 196 (define (append [lst1 : (List X)] [lst2 : (List X)] → (List X)) 197 (match lst1 with 198 [Nil -> lst2] 199 [Cons x xs -> (Cons x (append xs lst2))])) 200 201 (check-type (λ (a f g) (g (f a) (+ (f 1) (f 2)))) 202 : (→/test Int (→ Int Int) (→ Int Int C) C)) 203 204 (check-type ((λ ([a : A] [f : (→ Int A)]) a) 4 (λ (x) x)) 205 : Int) 206 207 ;; end infer.rkt tests -------------------------------------------------- 208 209 ;; algebraic data types 210 (define-type IntList 211 INil 212 (ConsI Int IntList)) 213 214 ;; HO, monomorphic 215 (check-type ConsI : (→ Int IntList IntList)) 216 (define (new-cons [c : (→ Int IntList IntList)] [x : Int] [xs : IntList] 217 -> IntList) 218 (c x xs)) 219 (check-type (new-cons ConsI 1 INil) : IntList -> (ConsI 1 INil)) 220 221 ;; check that ConsI and INil are available as tyvars 222 (define (f10 [x : INil] [y : ConsI] -> ConsI) y) 223 (check-type f10 : (→/test X Y Y)) 224 225 (check-type INil : IntList) 226 (check-type (ConsI 1 INil) : IntList) 227 (check-type 228 (match INil with 229 [INil -> 1] 230 [ConsI x xs -> 2]) : Int ⇒ 1) 231 (check-type 232 (match (ConsI 1 INil) with 233 [INil -> 1] 234 [ConsI x xs -> 2]) : Int ⇒ 2) 235 (typecheck-fail (match 1 with [INil -> 1])) 236 237 (typecheck-fail (ConsI #f INil) 238 #:with-msg 239 "expected: Int\n *given: Bool") 240 241 ;; annotated 242 (check-type (Nil {Int}) : (List Int)) 243 (check-type (Cons {Int} 1 (Nil {Int})) : (List Int)) 244 (check-type (Cons {Int} 1 (Cons 2 (Nil {Int}))) : (List Int)) 245 ;; partial annotations 246 (check-type (Cons 1 (Nil {Int})) : (List Int)) 247 (check-type (Cons 1 (Cons 2 (Nil {Int}))) : (List Int)) 248 (check-type (Cons {Int} 1 Nil) : (List Int)) 249 (check-type (Cons {Int} 1 (Cons 2 Nil)) : (List Int)) 250 (check-type (Cons 1 (Cons {Int} 2 Nil)) : (List Int)) 251 ; no annotations 252 (check-type (Cons 1 Nil) : (List Int)) 253 (check-type (Cons 1 (Cons 2 Nil)) : (List Int)) 254 255 (define-type (Tree X) 256 (Leaf X) 257 (Node (Tree X) (Tree X))) 258 (check-type (Leaf 10) : (Tree Int)) 259 (check-type (Node (Leaf 10) (Leaf 11)) : (Tree Int)) 260 261 (typecheck-fail Nil #:with-msg "Nil: no expected type, add annotations") 262 (typecheck-fail (Cons 1 (Nil {Bool})) 263 #:with-msg 264 "expected: \\(List Int\\)\n *given: \\(List Bool\\)") 265 (typecheck-fail (Cons {Bool} 1 (Nil {Int})) 266 #:with-msg 267 "Cons: type mismatch: expected Bool, given Int\n *expression: 1") 268 (typecheck-fail (Cons {Bool} 1 Nil) 269 #:with-msg 270 "Cons: type mismatch: expected Bool, given Int\n *expression: 1") 271 272 (typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1]) 273 #:with-msg "Nil: no expected type, add annotations") 274 (check-type 275 (match (Nil {Int}) with 276 [Cons x xs -> 2] 277 [Nil -> 1]) 278 : Int ⇒ 1) 279 280 (check-type 281 (match (Nil {Int}) with 282 [Nil -> 1] 283 [Cons x xs -> 2]) 284 : Int ⇒ 1) 285 286 (check-type 287 (match (Cons 1 Nil) with 288 [Nil -> 3] 289 [Cons y ys -> (+ y 4)]) 290 : Int ⇒ 5) 291 292 (check-type 293 (match (Cons 1 Nil) with 294 [Cons y ys -> (+ y 5)] 295 [Nil -> 3]) 296 : Int ⇒ 6) 297 298 ;; check expected-type propagation for other match patterns 299 300 (define-type (Option A) 301 (None) 302 (Some A)) 303 304 (define (None* → (Option A)) None) 305 306 (check-type (match (tup 1 2) with [a b -> None]) : (Option Int) -> None) 307 (check-type 308 (match (list 1 2) with 309 [[] -> None] 310 [[x y] -> None]) 311 : (Option Int) -> None) 312 313 (check-type 314 (match (list 1 2) with 315 [[] -> None] 316 [x :: xs -> None]) 317 : (Option Int) -> None) 318 319 (define-type (Pairof A B) (C A B)) 320 (check-type (match (C 1 2) with [C a b -> None]) : (Option Int) -> None) 321 322 ;; type variable inference 323 324 ; F should remain valid tyvar, even though it's bound 325 (define (F [x : X] -> X) x) 326 (define (tvf1 [x : F] -> F) x) 327 (check-type tvf1 : (→/test X X)) 328 329 ; G should remain valid tyvar 330 (define-type (Type1 X) (G X)) 331 (define (tvf5 [x : G] -> G) x) 332 (check-type tvf5 : (→/test X X)) 333 334 ; TY should not be tyvar, bc it's a valid type 335 (define-type-alias TY (Pairof Int Int)) 336 (define (tvf2 [x : TY] -> TY) x) 337 (check-not-type tvf2 : (→/test X X)) 338 339 ; same with Bool 340 (define (tvf3 [x : Bool] -> Bool) x) 341 (check-not-type tvf3 : (→/test X X)) 342 343 ;; X in lam should not be a new tyvar 344 (define (tvf4 [x : X] -> (→ X X)) 345 (λ (y) x)) 346 (check-type tvf4 : (→/test X (→ X X))) 347 (check-not-type tvf4 : (→/test X (→ Y X))) 348 349 (define (tvf6 [x : X] -> (→ Y X)) 350 (λ (y) x)) 351 (check-type tvf6 : (→/test X (→ Y X))) 352 353 ;; nested lambdas 354 355 (check-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test X (→ X X))) 356 (check-not-type (λ ([x : X]) (λ ([y : X]) y)) : (→/test {X} X (→/test {Y} Y Y))) 357 (check-type (λ ([x : X]) (λ ([y : Y]) y)) : (→/test {X} X (→/test {Y} Y Y))) 358 (check-not-type (λ ([x : X]) (λ ([y : Y]) x)) : (→/test X (→ X X))) 359 360 (check-type 361 ((λ ([x : X]) (λ ([y : Y]) y)) 1) 362 : (→/test Y Y)) 363 364 ;; TODO? 365 ;; - this fails if polymorphic functions are allowed as HO args 366 ;; - do we want to allow this? 367 ;; - must explicitly instantiate before passing fn 368 (check-type 369 ((λ ([x : (→ X (→ Y Y))]) x) 370 (inst (λ ([x : X]) (inst (λ ([y : Y]) y) Int)) Int)) 371 : (→ Int (→ Int Int))) 372 373 (check-type 374 ((λ ([x : X]) (λ ([y : Y]) (λ ([z : Z]) z))) 1) 375 : (→/test {Y} Y (→/test {Z} Z Z))) 376 377 (check-type (inst Cons (→/test X X)) 378 : (→ (→/test X X) (List (→/test X X)) (List (→/test X X)))) 379 (check-type map : (→/test (→ X Y) (List X) (List Y))) 380 381 (check-type (Cons (λ ([x : X]) x) Nil) 382 : (List (→/test {X} X X))) 383 384 (define (nn [x : X] -> (→ (× X (→ Y Y)))) 385 (λ () (tup x (λ ([x : Y]) x)))) 386 (typecheck-fail (nn 1) #:with-msg "Could not infer instantiation of polymorphic function nn.") 387 (check-type (nn 1) : (→ (× Int (→ String String)))) 388 (check-type (nn 1) : (→ (× Int (→ (List Int) (List Int))))) 389 390 (define (nn2 [x : X] -> (→ (× X (→ Y Y) (List Z)))) 391 (λ () (tup x (λ ([x : Y]) x) Nil))) 392 (typecheck-fail (nn2 1) #:with-msg "Could not infer instantiation of polymorphic function nn2.") 393 (check-type (nn2 1) : (→ (× Int (→ String String) (List (List Int))))) 394 (check-type (nn2 1) : (→ (× Int (→ (List Int) (List Int)) (List String)))) 395 ;; test inst order 396 (check-type ((inst nn2 Int String (List Int)) 1) 397 : (→ (× Int (→ String String) (List (List Int))))) 398 (check-type ((inst nn2 Int (List Int) String) 1) 399 : (→ (× Int (→ (List Int) (List Int)) (List String)))) 400 401 (define (nn3 [x : X] -> (→ (× X (Option Y) (Option Z)))) 402 (λ () (tup x None None))) 403 (check-type (nn3 1) : (→/test (× Int (Option Y) (Option Z)))) 404 (check-type (nn3 1) : (→ (× Int (Option String) (Option (List Int))))) 405 (check-type ((nn3 1)) : (× Int (Option String) (Option (List Int)))) 406 (check-type ((nn3 1)) : (× Int (Option (List Int)) (Option String))) 407 ;; test inst order 408 (check-type ((inst (nn3 1) String (List Int))) : (× Int (Option String) (Option (List Int)))) 409 (check-type ((inst (nn3 1) (List Int) String)) : (× Int (Option (List Int)) (Option String))) 410 411 (define (nn4 -> (→ (Option X))) 412 (λ () (None*))) 413 (check-type (let ([x (nn4)]) 414 x) 415 : (→/test (Option X))) 416 417 (define (nn5 -> (→ (Ref (Option X)))) 418 (λ () (ref (None {X})))) 419 (typecheck-fail (let ([x (nn5)]) 420 x) 421 #:with-msg "Could not infer instantiation of polymorphic function nn5.") 422 423 (define (nn6 -> (→ (Option X))) 424 (let ([r (((inst nn5 X)))]) 425 (λ () (deref r)))) 426 (check-type (nn6) : (→/test (Option X))) 427 428 ;; A is covariant, B is invariant. 429 (define-type (Cps A B) 430 (cps (→ (→ A B) B))) 431 (define (cps* [f : (→ (→ A B) B)] → (Cps A B)) 432 (cps f)) 433 434 (define (nn7 -> (→ (Cps (Option A) B))) 435 (let ([r (((inst nn5 A)))]) 436 (λ () (cps* (λ (k) (k (deref r))))))) 437 (typecheck-fail (let ([x (nn7)]) 438 x) 439 #:with-msg "Could not infer instantiation of polymorphic function nn7.") 440 441 (define (nn8 -> (→ (Cps (Option A) Int))) 442 (nn7)) 443 (check-type (let ([x (nn8)]) 444 x) 445 : (→/test (Cps (Option A) Int))) 446 447 (define-type (Result A B) 448 (Ok A) 449 (Error B)) 450 451 (define (ok [a : A] → (Result A B)) 452 (Ok a)) 453 454 ;; Cannot infer concrete type for B in (Result A B). 455 ;; Need expected type (see (inst result-if-1 ...) example below) 456 (typecheck-fail 457 (λ ([a : Int]) (ok (Cons a Nil))) 458 #:with-msg "Could not infer instantiation of polymorphic function ok") 459 460 (define (error [b : B] → (Result A B)) 461 (Error b)) 462 463 (define (ok-fn [a : A] -> (→ (Result A B))) 464 (λ () (ok a))) 465 (define (error-fn [b : B] -> (→ (Result A B))) 466 (λ () (error b))) 467 468 (check-type (let ([x (ok-fn 1)]) 469 x) 470 : (→/test (Result Int B))) 471 (check-type (let ([x (error-fn "bad")]) 472 x) 473 : (→/test (Result A String))) 474 475 (define (nn9 [a : A] -> (→ (Result A (Ref B)))) 476 (ok-fn a)) 477 (define (nn10 [a : A] -> (→ (Result A (Ref String)))) 478 (nn9 a)) 479 (define (nn11 -> (→ (Result (Option A) (Ref String)))) 480 (nn10 (None*))) 481 482 (typecheck-fail (let ([x (nn9 1)]) 483 x) 484 #:with-msg "Could not infer instantiation of polymorphic function nn9.") 485 (check-type (let ([x (nn10 1)]) 486 x) 487 : (→ (Result Int (Ref String)))) 488 (check-type (let ([x (nn11)]) 489 x) 490 : (→/test (Result (Option A) (Ref String)))) 491 492 (check-type (if (zero? (random 2)) 493 (ok 0) 494 (error "didn't get a zero")) 495 : (Result Int String)) 496 497 (define result-if-0 498 (λ ([b : (Result A1 B1)] [succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))]) 499 (match b with 500 [Ok a -> (succeed a)] 501 [Error b -> (fail b)]))) 502 (check-type result-if-0 503 : (→/test (Result A1 B1) (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2)) 504 (Result A2 B2))) 505 506 (define (result-if-1 [b : (Result A1 B1)] 507 → (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2)) 508 (Result A2 B2))) 509 (λ ([succeed : (→ A1 (Result A2 B2))] [fail : (→ B1 (Result A2 B2))]) 510 (result-if-0 b succeed fail))) 511 (check-type result-if-1 512 : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) (→ B1 (Result A2 B2)) 513 (Result A2 B2)))) 514 (check-type ((inst result-if-1 Int String (List Int) (List String)) (Ok 1)) 515 : (→ (→ Int (Result (List Int) (List String))) 516 (→ String (Result (List Int) (List String))) 517 (Result (List Int) (List String)))) 518 (check-type ((inst result-if-1 Int String (List Int) (List String)) (Error "bad")) 519 : (→ (→ Int (Result (List Int) (List String))) 520 (→ String (Result (List Int) (List String))) 521 (Result (List Int) (List String)))) 522 523 (check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1)) 524 (λ ([a : Int]) (ok (Cons a Nil))) 525 (λ ([b : String]) (error (Cons b Nil)))) 526 : (Result (List Int) (List String))) 527 ;; same thing, but without the lambda annotations: 528 (check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1)) 529 (λ (a) (ok (Cons a Nil))) 530 (λ (b) (error (Cons b Nil)))) 531 : (Result (List Int) (List String))) 532 533 (define (result-if-2 [b : (Result A1 B1)] 534 → (→ (→ A1 (Result A2 B2)) 535 (→ (→ B1 (Result A2 B2)) 536 (Result A2 B2)))) 537 (λ ([succeed : (→ A1 (Result A2 B2))]) 538 (λ ([fail : (→ B1 (Result A2 B2))]) 539 (result-if-0 b succeed fail)))) 540 (check-type result-if-2 541 : (→/test (Result A1 B1) (→ (→ A1 (Result A2 B2)) 542 (→ (→ B1 (Result A2 B2)) 543 (Result A2 B2))))) 544 (check-type ((inst result-if-2 Int String (List Int) (List String)) (Ok 1)) 545 : (→/test (→ Int (Result (List Int) (List String))) 546 (→ (→ String (Result (List Int) (List String))) 547 (Result (List Int) (List String))))) 548 (check-type (((inst result-if-2 Int String (List Int) (List String)) (Ok 1)) 549 (λ (a) (Ok (Cons a Nil)))) 550 : (→/test (→ String (Result (List Int) (List String))) 551 (Result (List Int) (List String)))) 552 (check-type ((((inst result-if-2 Int String (List Int) (List String)) (Ok 1)) 553 (λ (a) (Ok (Cons a Nil)))) 554 (λ (b) (Error (Cons b Nil)))) 555 : (Result (List Int) (List String))) 556 557 (define (tup* [a : A] [b : B] -> (× A B)) 558 (tup a b)) 559 560 (define (nn12 -> (→ (× (Option A) (Option B)))) 561 (λ () (tup* (None*) (None*)))) 562 (check-type (let ([x (nn12)]) 563 x) 564 : (→/test (× (Option A) (Option B)))) 565 566 (define (nn13 -> (→ (× (Option A) (Option (Ref B))))) 567 (nn12)) 568 (typecheck-fail (let ([x (nn13)]) 569 x) 570 #:with-msg "Could not infer instantiation of polymorphic function nn13.") 571 572 ;; records and automatically-defined accessors and predicates 573 (define-type (RecoTest X Y) 574 (RT1 [x : X] [y : Y] [z : String]) 575 (RT2 [a : Y] [b : X] [c : (List X)]) 576 (RT3 X Y)) ; mixing records and non-records allowed 577 578 (check-type RT1-x : (→/test (RecoTest X Y) X)) 579 (check-type RT1-y : (→/test (RecoTest X Y) Y)) 580 (check-type RT1-z : (→/test (RecoTest X Y) String)) 581 (check-type RT2-a : (→/test (RecoTest X Y) Y)) 582 (check-type RT2-b : (→/test (RecoTest X Y) X)) 583 584 (check-type RT1? : (→/test (RecoTest X Y) Bool)) 585 (check-type RT2? : (→/test (RecoTest X Y) Bool)) 586 (check-type RT3? : (→/test (RecoTest X Y) Bool)) 587 588 (check-type (RT1-x (RT1 1 #t "2")) : Int -> 1) 589 (check-type (RT1-y (RT1 1 #t "2")) : Bool -> #t) 590 (check-type (RT1-z (RT1 1 #t "2")) : String -> "2") 591 592 (check-type (RT2-a (RT2 1 #f Nil)) : Int -> 1) 593 (check-type (RT2-b (RT2 1 #f Nil)) : Bool -> #f) 594 (check-type (RT2-c (RT2 1 #f Nil)) : (List Bool) -> Nil) 595 596 (check-type (RT1? (RT1 1 2 "3")) : Bool -> #t) 597 (check-type (RT1? (RT2 1 2 Nil)) : Bool -> #f) 598 (check-type (RT1? (RT3 1 "2")) : Bool -> #f) 599 (check-type (RT3? (RT3 1 2)) : Bool -> #t) 600 (check-type (RT3? (RT1 1 2 "3")) : Bool -> #f) 601 602 (typecheck-fail RT3-x #:with-msg "unbound identifier") 603 604 ;; accessors produce runtime exception if given wrong variant 605 (check-runtime-exn (RT1-x (RT2 1 #f (Cons #t Nil)))) 606 (check-runtime-exn (RT1-y (RT2 1 #f (Cons #t Nil)))) 607 (check-runtime-exn (RT1-z (RT2 1 #f (Cons #t Nil)))) 608 (check-runtime-exn (RT1-x (RT3 1 2))) 609 (check-runtime-exn (RT2-a (RT1 1 #f "2"))) 610 (check-runtime-exn (RT2-c (RT1 1 #f "2"))) 611 (check-runtime-exn (RT2-c (RT1 1 #f "2"))) 612 (check-runtime-exn (RT2-a (RT3 #f #t))) 613 614 ;; non-match version 615 (define (rt-fn [rt : (RecoTest X Y)] -> X) 616 (if (RT1? rt) 617 (RT1-x rt) 618 (if (RT2? rt) 619 (RT2-b rt) 620 (match rt with [RT3 x y -> x][RT1 x y z -> x][RT2 a b c -> b])))) 621 (check-type (rt-fn (RT1 1 #f "3")) : Int -> 1) 622 (check-type (rt-fn (RT2 #f 2 Nil)) : Int -> 2) 623 (check-type (rt-fn (RT3 10 20)) : Int -> 10) 624 625 ;; HO constructors 626 (check-type RT1 : (→/test X Y String (RecoTest X Y))) 627 (check-type RT2 : (→/test {X Y} Y X (List X) (RecoTest X Y))) 628 (check-type RT3 : (→/test X Y (RecoTest X Y))) 629 630 (typecheck-fail (for/fold ([x 1]) () "hello") 631 #:with-msg "for/fold: type mismatch: expected Int, given String\n *expression: \"hello\"") 632 633 ; ext-stlc tests -------------------------------------------------- 634 635 ; tests for stlc extensions 636 ; new literals and base types 637 (check-type "one" : String) ; literal now supported 638 (check-type #f : Bool) ; literal now supported 639 640 (check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type 641 642 ;; Unit 643 (check-type (void) : Unit) 644 (check-type void : (→ Unit)) 645 646 (typecheck-fail 647 ((λ ([x : Unit]) x) 2) 648 #:with-msg 649 "expected: Unit\n *given: Int") 650 (typecheck-fail 651 ((λ ([x : Unit]) x) void) 652 #:with-msg 653 "expected: Unit\n *given: \\(→ Unit\\)") 654 655 (check-type ((λ ([x : Unit]) x) (void)) : Unit) 656 657 ;; begin 658 (check-type (begin 1) : Int) 659 660 (typecheck-fail (begin) #:with-msg "expected more terms") 661 ;; 2016-03-06: begin terms dont need to be Unit 662 (check-type (begin 1 2 3) : Int) 663 #;(typecheck-fail 664 (begin 1 2 3) 665 #:with-msg "Expected expression 1 to have Unit type, got: Int") 666 667 (check-type (begin (void) 1) : Int ⇒ 1) 668 (check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int) 669 (check-type ((λ ([x : Int]) (begin x)) 1) : Int) 670 (check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int) 671 (check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int) 672 (check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int) 673 674 ;;ascription 675 (check-type (ann 1 : Int) : Int ⇒ 1) 676 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) 677 (typecheck-fail (ann 1 : Bool) #:with-msg "expected Bool, given Int\n *expression: 1") 678 ;ann errs 679 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier") 680 (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type") 681 (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type") 682 (typecheck-fail (ann Int : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Int") 683 684 ; let 685 (check-type (let () (+ 1 1)) : Int ⇒ 2) 686 (check-type (let ([x 10]) (+ 1 2)) : Int) 687 (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) 688 (typecheck-fail 689 (let ([x #f]) (+ x 1)) 690 #:with-msg "expected: Int\n *given: Bool") 691 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y)) 692 #:with-msg "x: unbound identifier") 693 694 (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) 695 (typecheck-fail 696 (let* ([x #t] [y (+ x 1)]) 1) 697 #:with-msg "expected: Int\n *given: Bool") 698 699 ; letrec 700 (typecheck-fail 701 (letrec ([(x : Int) #f] [(y : Int) 1]) y) 702 #:with-msg 703 "letrec: type mismatch: expected Int, given Bool\n *expression: #f") 704 (typecheck-fail 705 (letrec ([(y : Int) 1] [(x : Int) #f]) x) 706 #:with-msg 707 "letrec: type mismatch: expected Int, given Bool\n *expression: #f") 708 709 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) 710 711 ;; recursive 712 (check-type 713 (letrec ([(countdown : (→ Int String)) 714 (λ (i) 715 (if (= i 0) 716 "liftoff" 717 (countdown (- i 1))))]) 718 (countdown 10)) : String ⇒ "liftoff") 719 720 ;; mutually recursive 721 (check-type 722 (letrec ([(is-even? : (→ Int Bool)) 723 (λ (n) 724 (or (zero? n) 725 (is-odd? (sub1 n))))] 726 [(is-odd? : (→ Int Bool)) 727 (λ (n) 728 (and (not (zero? n)) 729 (is-even? (sub1 n))))]) 730 (is-odd? 11)) : Bool ⇒ #t) 731 732 ;; check some more err msgs 733 (typecheck-fail 734 (and "1" #f) 735 #:with-msg "and: type mismatch: expected Bool, given String\n *expression: \"1\"") 736 (typecheck-fail 737 (and #t "2") 738 #:with-msg 739 "and: type mismatch: expected Bool, given String\n *expression: \"2\"") 740 (typecheck-fail 741 (or "1" #f) 742 #:with-msg 743 "or: type mismatch: expected Bool, given String\n *expression: \"1\"") 744 (typecheck-fail 745 (or #t "2") 746 #:with-msg 747 "or: type mismatch: expected Bool, given String\n *expression: \"2\"") 748 ;; 2016-03-09: now ok 749 (check-type (if "true" 1 2) : Int -> 1) 750 (typecheck-fail 751 (if #t 1 "2") 752 #:with-msg 753 "branches have incompatible types: Int and String") 754 755 ;; tests from stlc+lit-tests.rkt -------------------------- 756 ; most should pass, some failing may now pass due to added types/forms 757 (check-type 1 : Int) 758 (check-not-type 1 : (→ Int Int)) 759 ;(typecheck-fail "one") ; literal now supported 760 ;(typecheck-fail #f) ; literal now supported 761 (check-type (λ (x y) x) : (→ Int Int Int)) 762 (check-not-type (λ ([x : Int]) x) : Int) 763 (check-type (λ (x) x) : (→ Int Int)) 764 (check-type (λ (f) 1) : (→ (→ Int Int) Int)) 765 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 766 767 (typecheck-fail 768 ((λ ([x : Bool]) x) 1) 769 #:with-msg "expected: Bool\n *given: Int") 770 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type 771 (typecheck-fail 772 (λ ([f : Int]) (f 1 2)) 773 #:with-msg 774 "Expected → type, got: Int") 775 776 (check-type (λ (f x y) (f x y)) 777 : (→ (→ Int Int Int) Int Int Int)) 778 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) 779 : Int ⇒ 3) 780 781 (typecheck-fail 782 (+ 1 (λ ([x : Int]) x)) 783 #:with-msg "expected: Int\n *given: \\(→ Int Int\\)") 784 (typecheck-fail 785 (λ ([x : (→ Int Int)]) (+ x x)) 786 #:with-msg "expected: Int\n *given: \\(→ Int Int\\)") 787 (typecheck-fail 788 ((λ ([x : Int] [y : Int]) y) 1) 789 #:with-msg "wrong number of arguments: expected 2, given 1\n *expected: +Int, Int\n *arguments: 1") 790 791 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 792