tlb-infer-tests.rkt (4239B)
1 #lang s-exp "../infer.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 (check-type (λ (x) 5) : (∀ (X) (→ X Int))) 5 (check-type (λ (x) x) : (∀ (X) (→ X X))) 6 (check-type ((λ (x) x) 5) : Int) 7 (check-type ((λ (x) x) (λ (y) y)) : (∀ (Y) (→ Y Y))) 8 9 (check-type (λ (x) (λ (y) 6)) : (∀ (X) (→ X (∀ (Y) (→ Y Int))))) 10 (check-type (λ (x) (λ (y) x)) : (∀ (X) (→ X (∀ (Y) (→ Y X))))) 11 (check-type (λ (x) (λ (y) y)) : (∀ (X) (→ X (∀ (Y) (→ Y Y))))) 12 13 (check-type (λ (x) (λ (y) (λ (z) 7))) : (∀ (X) (→ X (∀ (Y) (→ Y (∀ (Z) (→ Z Int))))))) 14 (check-type (λ (x) (λ (y) (λ (z) x))) : (∀ (X) (→ X (∀ (Y) (→ Y (∀ (Z) (→ Z X))))))) 15 (check-type (λ (x) (λ (y) (λ (z) y))) : (∀ (X) (→ X (∀ (Y) (→ Y (∀ (Z) (→ Z Y))))))) 16 (check-type (λ (x) (λ (y) (λ (z) z))) : (∀ (X) (→ X (∀ (Y) (→ Y (∀ (Z) (→ Z Z))))))) 17 18 (check-type (+ 1 2) : Int) 19 (check-type (λ (x) (+ x 2)) : (→ Int Int)) 20 (check-type (λ (x y) (+ 1 2)) : (∀ (X Y) (→ X Y Int))) 21 (check-type (λ (x y) (+ x 2)) : (∀ (Y) (→ Int Y Int))) 22 (check-type (λ (x y) (+ 1 y)) : (∀ (X) (→ X Int Int))) 23 (check-type (λ (x y) (+ x y)) : (→ Int Int Int)) 24 25 (check-type (λ (x) (λ (y) (+ 1 2))) : (∀ (X) (→ X (∀ (Y) (→ Y Int))))) 26 (check-type (λ (x) (λ (y) (+ x 2))) : (→ Int (∀ (Y) (→ Y Int)))) 27 (check-type (λ (x) (λ (y) (+ 1 y))) : (∀ (X) (→ X (→ Int Int)))) 28 (check-type (λ (x) (λ (y) (+ x y))) : (→ Int (→ Int Int))) 29 30 (check-type (λ (x) (λ (y) (λ (z) (+ 1 2)))) : (∀ (X) (→ X (∀ (Y) (→ Y (∀ (Z) (→ Z Int))))))) 31 (check-type (λ (x) (λ (y) (λ (z) (+ x 2)))) : (→ Int (∀ (Y) (→ Y (∀ (Z) (→ Z Int)))))) 32 (check-type (λ (x) (λ (y) (λ (z) (+ y 2)))) : (∀ (X) (→ X (→ Int (∀ (Z) (→ Z Int)))))) 33 (check-type (λ (x) (λ (y) (λ (z) (+ z 2)))) : (∀ (X) (→ X (∀ (Y) (→ Y (→ Int Int)))))) 34 (check-type (λ (x) (λ (y) (λ (z) (+ x y)))) : (→ Int (→ Int (∀ (Z) (→ Z Int))))) 35 (check-type (λ (x) (λ (y) (λ (z) (+ x z)))) : (→ Int (∀ (Y) (→ Y (→ Int Int))))) 36 (check-type (λ (x) (λ (y) (λ (z) (+ y z)))) : (∀ (X) (→ X (→ Int (→ Int Int))))) 37 (check-type (λ (x) (λ (y) (λ (z) (+ (+ x y) z)))) : (→ Int (→ Int (→ Int Int)))) 38 39 (check-type (λ (f a) (f a)) : (∀ (A B) (→ (→ A B) A B))) 40 41 (check-type (λ (a f g) (g (f a))) 42 : (∀ (A C B) (→ A (→ A B) (→ B C) C))) 43 (check-type (λ (a f g) (g (f a) (+ (f 1) (f 2)))) 44 : (∀ (C) (→ Int (→ Int Int) (→ Int Int C) C))) 45 (check-type (λ (a f g) (g (λ () (f a)) (+ (f 1) (f 2)))) 46 : (∀ (C) (→ Int (→ Int Int) (→ (→ Int) Int C) C))) 47 48 (typecheck-fail 49 (λ (f) (f f)) 50 #:with-msg "couldn't unify f[0-9]+ and \\(→ f[0-9]+ result[0-9]+\\) because one contains the other") 51 52 (typecheck-fail 53 (λ (f) 54 ((λ (g) (f (λ (x) ((g g) x)))) 55 (λ (g) (f (λ (x) ((g g) x)))))) 56 #:with-msg "couldn't unify g[0-9]+ and \\(→ g[0-9]+ result[0-9]+\\) because one contains the other") 57 58 (define fact-builder 59 (λ (fact) 60 (λ (n) 61 (if (= 0 n) 62 1 63 (* n (fact (sub1 n))))))) 64 65 (check-type fact-builder : (→ (→ Int Int) (→ Int Int))) 66 67 (define fact~ (fact-builder (fact-builder (fact-builder (fact-builder (fact-builder (λ (n) 1))))))) 68 (check-type fact~ : (→ Int Int)) 69 (check-type (fact~ 0) : Int -> 1) 70 (check-type (fact~ 1) : Int -> 1) 71 (check-type (fact~ 2) : Int -> 2) 72 (check-type (fact~ 3) : Int -> 6) 73 (check-type (fact~ 4) : Int -> 24) 74 (check-type (fact~ 5) : Int -> 120) 75 (check-type (fact~ 6) : Int -> 720) 76 ;(check-type (fact~ 7) : Int -> 5040) ; fails, produces 2520 77 ;(check-type (fact~ 8) : Int -> 40320) ; fails, produces 6720 78 79 (define/rec Y : (∀ (A B) (→ (→ (→ A B) (→ A B)) (→ A B))) 80 (λ (f) 81 (f (λ (x) ((Y f) x))))) 82 (check-type Y : (∀ (A B) (→ (→ (→ A B) (→ A B)) (→ A B)))) 83 84 (define fact (Y fact-builder)) 85 (check-type fact : (→ Int Int)) 86 (check-type (fact 0) : Int -> 1) 87 (check-type (fact 1) : Int -> 1) 88 (check-type (fact 2) : Int -> 2) 89 (check-type (fact 3) : Int -> 6) 90 (check-type (fact 4) : Int -> 24) 91 (check-type (fact 5) : Int -> 120) 92 (check-type (fact 6) : Int -> 720) 93 (check-type (fact 7) : Int -> 5040) 94 (check-type (fact 8) : Int -> 40320)