fomega3-tests.rkt (10257B)
1 #lang s-exp "../fomega3.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 (check-type Int : ★) 5 (check-type String : ★) 6 (typecheck-fail →) 7 (check-type (→ Int Int) : ★) 8 (typecheck-fail (→ →)) 9 (typecheck-fail (→ 1)) 10 (check-type 1 : Int) 11 12 ;(check-type (∀ ([t : ★]) (→ t t)) : ★) 13 (check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★)) 14 (check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★) 15 16 (check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X))) 17 18 (check-type ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : ★]) (λ ([x : X]) x))) 19 : (∀ ([X : ★]) (→ X X))) 20 (typecheck-fail ((λ ([x : (∀ ([X : ★]) (→ X X))]) x) (Λ ([X : (→ ★ ★)]) (λ ([x : X]) x)))) 21 22 (check-type (λ ([t : ★]) t) : (→ ★ ★)) 23 (check-type (λ ([t : ★] [s : ★]) t) : (→ ★ ★ ★)) 24 (check-type (λ ([t : ★]) (λ ([s : ★]) t)) : (→ ★ (→ ★ ★))) 25 (check-type (λ ([t : (→ ★ ★)]) t) : (→ (→ ★ ★) (→ ★ ★))) 26 (check-type (λ ([t : (→ ★ ★ ★)]) t) : (→ (→ ★ ★ ★) (→ ★ ★ ★))) 27 (check-type (λ ([arg : ★] [res : ★]) (→ arg res)) : (→ ★ ★ ★)) 28 29 (check-type ((λ ([t : ★]) t) Int) : ★) 30 (check-type (λ ([x : ((λ ([t : ★]) t) Int)]) x) : (→ Int Int)) 31 (check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) x) 1) : Int ⇒ 1) 32 (check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ x 1)) 1) : Int ⇒ 2) 33 (check-type ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) 1) : Int ⇒ 2) 34 (typecheck-fail ((λ ([x : ((λ ([t : ★]) t) Int)]) (+ 1 x)) "a-string")) 35 36 ;; partial-apply → 37 (check-type ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int) 38 : (→ ★ ★)) 39 ; f's type must have kind ★ 40 (typecheck-fail (λ ([f : ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)]) f)) 41 (check-type (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) : 42 (∀ ([tyf : (→ ★ ★)]) (→ (tyf String) (tyf String)))) 43 (check-type (inst 44 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) 45 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)) 46 : (→ (→ Int String) (→ Int String))) 47 (typecheck-fail 48 (inst (Λ ([X : ★]) (λ ([x : X]) x)) 1)) 49 ;#:with-msg "not a valid type: 1") 50 51 ;; applied f too early 52 (typecheck-fail (inst 53 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) (f 1))) 54 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int))) 55 (check-type ((inst 56 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) 57 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)) 58 (λ ([x : Int]) "int")) : (→ Int String)) 59 (check-type (((inst 60 (Λ ([tyf : (→ ★ ★)]) (λ ([f : (tyf String)]) f)) 61 ((λ ([arg : ★]) (λ ([res : ★]) (→ arg res))) Int)) 62 (λ ([x : Int]) "int")) 1) : String ⇒ "int") 63 64 ;; tapl examples, p441 65 (typecheck-fail 66 (define-type-alias tmp 1)) 67 ;#:with-msg "not a valid type: 1") 68 (define-type-alias Id (λ ([X : ★]) X)) 69 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int String) Int)) 70 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ Int (Id String)) Int)) 71 (check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int String) Int)) 72 (check-type (λ ([f : (→ Int (Id String))]) 1) : (→ (→ Int (Id String)) Int)) 73 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) (Id String)) Int)) 74 (check-type (λ ([f : (→ Int String)]) 1) : (→ (→ (Id Int) String) Int)) 75 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (→ Int String) Int)) 76 (check-type (λ ([f : (→ Int String)]) 1) : (→ (Id (→ Int String)) Int)) 77 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (→ Int String)) Int)) 78 (check-type (λ ([f : (Id (→ Int String))]) 1) : (→ (Id (Id (→ Int String))) Int)) 79 80 ;; tapl examples, p451 81 (define-type-alias Pair (λ ([A : ★] [B : ★]) (∀ ([X : ★]) (→ (→ A B X) X)))) 82 83 ;(check-type Pair : (→ ★ ★ ★)) 84 (check-type Pair : (→ ★ ★ (∀★ ★))) 85 86 (check-type (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) x)) : (∀ ([X : ★][Y : ★]) (→ X Y X))) 87 ; parametric pair constructor 88 (check-type 89 (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) 90 : (∀ ([X : ★][Y : ★]) (→ X Y (Pair X Y)))) 91 ; concrete Pair Int String constructor 92 (check-type 93 (inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) 94 Int String) 95 : (→ Int String (Pair Int String))) 96 ; Pair Int String value 97 (check-type 98 ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) 99 Int String) 1 "1") 100 : (Pair Int String)) 101 ; fst: parametric 102 (check-type 103 (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) 104 : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) X))) 105 ; fst: concrete Pair Int String accessor 106 (check-type 107 (inst 108 (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) 109 Int String) 110 : (→ (Pair Int String) Int)) 111 ; apply fst 112 (check-type 113 ((inst 114 (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) 115 Int String) 116 ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) 117 Int String) 1 "1")) 118 : Int ⇒ 1) 119 ; snd 120 (check-type 121 (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) 122 : (∀ ([X : ★][Y : ★]) (→ (Pair X Y) Y))) 123 (check-type 124 (inst 125 (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) 126 Int String) 127 : (→ (Pair Int String) String)) 128 (check-type 129 ((inst 130 (Λ ([X : ★][Y : ★]) (λ ([p : (∀ ([R : ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) 131 Int String) 132 ((inst (Λ ([X : ★] [Y : ★]) (λ ([x : X][y : Y]) (Λ ([R : ★]) (λ ([p : (→ X Y R)]) (p x y))))) 133 Int String) 1 "1")) 134 : String ⇒ "1") 135 136 ;;; sysf tests wont work, unless augmented with kinds 137 (check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X))) 138 139 (check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X : ★]) (→ X X X))) ; true 140 (check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X : ★]) (→ X X X))) ; false 141 (check-type (Λ ([X : ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y : ★]) (→ Y Y Y))) ; false, alpha equiv 142 143 (check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) 144 : (∀ ([t1 : ★]) (∀ ([t2 : ★]) (→ t1 (→ t2 t2))))) 145 146 (check-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) 147 : (∀ ([t3 : ★]) (∀ ([t4 : ★]) (→ t3 (→ t4 t4))))) 148 149 (check-not-type (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) 150 : (∀ ([t4 : ★]) (∀ ([t3 : ★]) (→ t3 (→ t4 t4))))) 151 152 (check-type (inst (Λ ([t : ★]) (λ ([x : t]) x)) Int) : (→ Int Int)) 153 (check-type (inst (Λ ([t : ★]) 1) (→ Int Int)) : Int) 154 ; first inst should be discarded 155 (check-type (inst (inst (Λ ([t : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int)) 156 ; second inst is discarded 157 (check-type (inst (inst (Λ ([t1 : ★]) (Λ ([t2 : ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int)) 158 159 ;; polymorphic arguments 160 (check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([t : ★]) (→ t t))) 161 (check-type (Λ ([t : ★]) (λ ([x : t]) x)) : (∀ ([s : ★]) (→ s s))) 162 (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([s : ★]) (∀ ([t : ★]) (→ t t)))) 163 (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([t : ★]) (→ t t)))) 164 (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([s : ★]) (→ s s)))) 165 (check-type (Λ ([s : ★]) (Λ ([t : ★]) (λ ([x : t]) x))) : (∀ ([r : ★]) (∀ ([u : ★]) (→ u u)))) 166 (check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) x) : (→ (∀ ([s : ★]) (→ s s)) (∀ ([u : ★]) (→ u u)))) 167 (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x))) 168 (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1)) 169 (check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) : (∀ ([u : ★]) (→ u u))) 170 (check-type 171 (inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) : (→ Int Int)) 172 (check-type 173 ((inst ((λ ([x : (∀ ([t : ★]) (→ t t))]) x) (Λ ([s : ★]) (λ ([y : s]) y))) Int) 10) 174 : Int ⇒ 10) 175 (check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t : ★]) (→ t t)) (→ Int Int))) 176 (check-type (λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t : ★]) (→ t t)) Int)) 177 (check-type ((λ ([x : (∀ ([t : ★]) (→ t t))]) ((inst x Int) 10)) 178 (Λ ([s : ★]) (λ ([y : s]) y))) 179 : Int ⇒ 10) 180 181 182 ;; previous tests ------------------------------------------------------------- 183 (check-type 1 : Int) 184 (check-not-type 1 : (→ Int Int)) 185 ;(typecheck-fail #f) ; unsupported literal 186 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 187 (check-not-type (λ ([x : Int]) x) : Int) 188 (check-type (λ ([x : Int]) x) : (→ Int Int)) 189 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 190 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 191 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type 192 (typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type 193 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 194 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 195 : (→ (→ Int Int Int) Int Int Int)) 196 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 197 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 198 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 199 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 200 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)