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