fomega2-tests.rkt (10549B)
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-kind (∀ ([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 ;; λ 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-kind Pair :: (→ ★ ★ (∀★ ★))) 90 91 (check-type (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) x)) 92 : (∀ ([X :: ★][Y :: ★]) (→ X Y X))) 93 ; parametric pair constructor 94 (check-type 95 (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) 96 : (∀ ([X :: ★][Y :: ★]) (→ X Y (Pair X Y)))) 97 ; concrete Pair Int String constructor 98 (check-type 99 (inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) 100 Int String) 101 : (→ Int String (Pair Int String))) 102 ; Pair Int String value 103 (check-type 104 ((inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) 105 Int String) 1 "1") 106 : (Pair Int String)) 107 ; fst: parametric 108 (check-type 109 (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) 110 : (∀ ([X :: ★][Y :: ★]) (→ (Pair X Y) X))) 111 ; fst: concrete Pair Int String accessor 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 : (→ (Pair Int String) Int)) 117 ; apply fst 118 (check-type 119 ((inst 120 (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p X) (λ ([x : X][y : Y]) x)))) 121 Int String) 122 ((inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) 123 Int String) 1 "1")) 124 : Int ⇒ 1) 125 ; snd 126 (check-type 127 (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) 128 : (∀ ([X :: ★][Y :: ★]) (→ (Pair X Y) Y))) 129 (check-type 130 (inst 131 (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) 132 Int String) 133 : (→ (Pair Int String) String)) 134 (check-type 135 ((inst 136 (Λ ([X :: ★][Y :: ★]) (λ ([p : (∀ ([R :: ★]) (→ (→ X Y R) R))]) ((inst p Y) (λ ([x : X][y : Y]) y)))) 137 Int String) 138 ((inst (Λ ([X :: ★] [Y :: ★]) (λ ([x : X][y : Y]) (Λ ([R :: ★]) (λ ([p : (→ X Y R)]) (p x y))))) 139 Int String) 1 "1")) 140 : String ⇒ "1") 141 142 ;;; sysf tests wont work, unless augmented with kinds 143 (check-type (Λ ([X :: ★]) (λ ([x : X]) x)) : (∀ ([X :: ★]) (→ X X))) 144 145 (check-type (Λ ([X :: ★]) (λ ([t : X] [f : X]) t)) : (∀ ([X :: ★]) (→ X X X))) ; true 146 (check-type (Λ ([X :: ★]) (λ ([t : X] [f : X]) f)) : (∀ ([X :: ★]) (→ X X X))) ; false 147 (check-type (Λ ([X :: ★]) (λ ([t : X] [f : X]) f)) : (∀ ([Y :: ★]) (→ Y Y Y))) ; false, alpha equiv 148 149 (check-type (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) 150 : (∀ ([t1 :: ★]) (∀ ([t2 :: ★]) (→ t1 (→ t2 t2))))) 151 152 (check-type (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) 153 : (∀ ([t3 :: ★]) (∀ ([t4 :: ★]) (→ t3 (→ t4 t4))))) 154 155 (check-not-type (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) (λ ([y : t2]) y)))) 156 : (∀ ([t4 :: ★]) (∀ ([t3 :: ★]) (→ t3 (→ t4 t4))))) 157 158 (check-type (inst (Λ ([t :: ★]) (λ ([x : t]) x)) Int) : (→ Int Int)) 159 (check-type (inst (Λ ([t :: ★]) 1) (→ Int Int)) : Int) 160 ; first inst should be discarded 161 (check-type (inst (inst (Λ ([t :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) (→ Int Int)) Int) : (→ Int Int)) 162 ; second inst is discarded 163 (check-type (inst (inst (Λ ([t1 :: ★]) (Λ ([t2 :: ★]) (λ ([x : t1]) x))) Int) (→ Int Int)) : (→ Int Int)) 164 165 ;; polymorphic arguments 166 (check-type (Λ ([t :: ★]) (λ ([x : t]) x)) : (∀ ([t :: ★]) (→ t t))) 167 (check-type (Λ ([t :: ★]) (λ ([x : t]) x)) : (∀ ([s :: ★]) (→ s s))) 168 (check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([s :: ★]) (∀ ([t :: ★]) (→ t t)))) 169 (check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([r :: ★]) (∀ ([t :: ★]) (→ t t)))) 170 (check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([r :: ★]) (∀ ([s :: ★]) (→ s s)))) 171 (check-type (Λ ([s :: ★]) (Λ ([t :: ★]) (λ ([x : t]) x))) : (∀ ([r :: ★]) (∀ ([u :: ★]) (→ u u)))) 172 (check-type (λ ([x : (∀ ([t :: ★]) (→ t t))]) x) : (→ (∀ ([s :: ★]) (→ s s)) (∀ ([u :: ★]) (→ u u)))) 173 (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) (λ ([x : Int]) x))) 174 (typecheck-fail ((λ ([x : (∀ (t) (→ t t))]) x) 1)) 175 (check-type ((λ ([x : (∀ ([t :: ★]) (→ t t))]) x) (Λ ([s :: ★]) (λ ([y : s]) y))) : (∀ ([u :: ★]) (→ u u))) 176 (check-type 177 (inst ((λ ([x : (∀ ([t :: ★]) (→ t t))]) x) (Λ ([s :: ★]) (λ ([y : s]) y))) Int) : (→ Int Int)) 178 (check-type 179 ((inst ((λ ([x : (∀ ([t :: ★]) (→ t t))]) x) (Λ ([s :: ★]) (λ ([y : s]) y))) Int) 10) 180 : Int ⇒ 10) 181 (check-type (λ ([x : (∀ ([t :: ★]) (→ t t))]) (inst x Int)) : (→ (∀ ([t :: ★]) (→ t t)) (→ Int Int))) 182 (check-type (λ ([x : (∀ ([t :: ★]) (→ t t))]) ((inst x Int) 10)) : (→ (∀ ([t :: ★]) (→ t t)) Int)) 183 (check-type ((λ ([x : (∀ ([t :: ★]) (→ t t))]) ((inst x Int) 10)) 184 (Λ ([s :: ★]) (λ ([y : s]) y))) 185 : Int ⇒ 10) 186 187 188 ;; previous tests ------------------------------------------------------------- 189 (check-type 1 : Int) 190 (check-not-type 1 : (→ Int Int)) 191 ;(typecheck-fail #f) ; unsupported literal 192 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 193 (check-not-type (λ ([x : Int]) x) : Int) 194 (check-type (λ ([x : Int]) x) : (→ Int Int)) 195 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 196 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 197 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type 198 (typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type 199 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 200 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 201 : (→ (→ Int Int Int) Int Int Int)) 202 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 203 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 204 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 205 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 206 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)