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