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