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