generic.mlish (17106B)
1 #lang s-exp "../../mlish+adhoc.rkt" 2 (require "../rackunit-typechecking.rkt") 3 4 (define-typeclass (Eq X) 5 [== : (→ X X Bool)]) 6 7 (define-instance (Eq Int) 8 [== =]) 9 10 (define-instance (Eq Float) 11 [== fl=]) 12 13 (define (id-fn1 [x : X] #:where (Eq X) -> X) x) 14 (typecheck-fail (id-fn1 #f) #:with-msg "\\(Eq Bool\\) instance undefined") 15 (check-type (id-fn1 1) : Int -> 1) 16 17 (check-type (== 1 2) : Bool -> (= 1 2)) 18 (check-type (== 1 2) : Bool -> #f) 19 (check-type (== 2 2) : Bool -> (= 2 2)) 20 (check-type (== 2 2) : Bool -> #t) 21 (typecheck-fail (== "1" "1") 22 #:with-msg "== operation undefined for input types: String, String") 23 24 (define-instance (Eq String) ; test use of lambda on rhs 25 [== (λ ([x : String] [y : String]) 26 (string=? x y))]) 27 28 (check-type (== "1" "2") : Bool -> (string=? "1" "2")) 29 (check-type (== "1" "2") : Bool -> #f) 30 (check-type (== "2" "2") : Bool -> (string=? "2" "2")) 31 (check-type (== "2" "2") : Bool -> #t) 32 33 (define-instance (Eq Char) 34 [== char=?]) 35 36 (check-type (λ ([x : X] #:where (Eq X)) 37 (== x x)) 38 : (=>/test (Eq X) (→ X Bool))) 39 40 (check-type ((λ ([x : X] #:where (Eq X)) (== x x)) 1) : Bool -> #t) 41 (check-type ((λ ([x : X] #:where (Eq X)) (== x x)) "1") : Bool -> #t) 42 (typecheck-fail ((λ ([x : X] #:where (Eq X)) (== x x)) #f) 43 #:with-msg 44 "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool") 45 46 (define (member? [x : X] [lst : (List X)] #:where (Eq X) -> Bool) 47 (match lst with 48 [[] -> #f] 49 [y :: ys -> (or (== x y) (member? x ys))])) 50 51 (check-type (member? 1 nil) : Bool -> #f) 52 (check-type (member? 1 (list 2)) : Bool -> #f) 53 (check-type (member? 1 (list 2 1)) : Bool -> #t) 54 (typecheck-fail (member? "1" (list 1))) ; TODO: fix err msg 55 (check-type (member? "1" nil) : Bool -> #f) 56 (check-type (member? "1" (list "2")) : Bool -> #f) 57 (check-type (member? "1" (list "2" "1")) : Bool -> #t) 58 59 ;; TODO?: fix name clash of generic op and concrete op 60 (define-typeclass (Ord X) 61 [lt : (→ X X Bool)] 62 [lte : (→ X X Bool)] 63 [gt : (→ X X Bool)] 64 [gte : (→ X X Bool)]) 65 66 (define-instance (Ord Int) 67 [lt <] [lte <=] [gt >] [gte >=]) 68 69 ;; missing typeclass constraint 70 (typecheck-fail (λ ([x : X]) (== x x)) 71 #:with-msg "== operation undefined for input types: X, X") 72 (typecheck-fail (λ ([x : X]) (lte x x)) 73 #:with-msg "lte operation undefined for input types: X, X") 74 ;; wrong typeclass constraint 75 (typecheck-fail (λ ([x : Y] #:where (Ord Y)) (== x x)) 76 #:with-msg "== operation undefined for input types: Y, Y") 77 (typecheck-fail (λ ([x : Y] #:where (Eq Y)) (gt x x)) 78 #:with-msg "gt operation undefined for input types: Y, Y") 79 80 (check-type (λ ([x : Y] #:where (Ord Y)) (lte x x)) 81 : (=>/test (Ord Y) (→ Y Bool))) 82 (check-type (λ ([x : Y] #:where (Ord Y)) (lt x x)) 83 : (=>/test (Ord Y) (→ Y Bool))) 84 (check-type (λ ([x : Y] #:where (Ord Y)) (gte x x)) 85 : (=>/test (Ord Y) (→ Y Bool))) 86 (check-type (λ ([x : Y] #:where (Ord Y)) (gt x x)) 87 : (=>/test (Ord Y) (→ Y Bool))) 88 89 (check-type (λ ([x : Y] [y : Y] #:where (Ord Y)) (lt x x)) 90 : (=>/test (Ord Y) (→ Y Y Bool))) 91 (check-type (λ ([x : Y] [y : Y] #:where (Ord Y)) (lt x y)) 92 : (=>/test (Ord Y) (→ Y Y Bool))) 93 (check-type (λ ([x : Y] #:where (Ord Y) (Eq Y)) 94 (lt x x)) 95 : (=>/test (Ord Y) (Eq Y) (→ Y Bool))) 96 (check-type (λ ([x : Y] #:where (Ord Y) (Eq Y)) 97 (== x x)) 98 : (=>/test (Ord Y) (Eq Y) (→ Y Bool))) 99 100 (check-type (λ ([x : Y] #:where (Ord Y) (Eq Y)) 101 (and (== x x) (lte x x))) 102 : (=>/test (Ord Y) (Eq Y) (→ Y Bool))) 103 104 ;; todo: not working; results in dup ids 105 #;(check-type (λ ([x : X] [y : Y] #:where (Ord X) (Ord Y)) (< x y)) 106 : (=>/test (Ord Y) (→ Y Y Bool))) 107 108 (define (f [x : X] #:where (Eq X) -> Bool) 109 (== x x)) 110 (check-type (f 1) : Bool -> #t) 111 (check-type (f "1") : Bool -> #t) 112 (typecheck-fail (f #f) 113 #:with-msg 114 "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool") 115 116 (define-instance (Ord String) 117 [lt string<?] [lte string<=?] [gt string>?] [gte string>=?]) 118 (check-type (lt "1" "2") : Bool -> #t) 119 (define (f2 [x : X] [y : X] #:where (Ord X) -> Bool) 120 (lte x y)) 121 (check-type (f2 1 2) : Bool -> #t) 122 (check-type (f2 "1" "2") : Bool -> #t) 123 (typecheck-fail (f2 1 "2")) 124 125 (define-typeclass (Num X) 126 [add : (→ X X X)] 127 [sub : (→ X X X)] 128 [mul : (→ X X X)]) 129 130 (typecheck-fail 131 (define-instance (Num Int) 132 [add +] [sub -] [mul fl*]) 133 #:with-msg 134 "define\\-instance\\: type mismatch\\: expected \\(→ Int Int Int\\), given \\(→ Float Float Float\\).*at.*fl\\*") 135 136 (define-instance (Num Int) 137 [add +] [sub -] [mul *]) 138 (define-instance (Num Float) 139 [add fl+] [sub fl-] [mul fl*]) 140 141 (define (square [x : X] #:where (Num X) -> X) 142 (mul x x)) 143 (check-type (square 5) : Int -> 25) 144 (check-type (square 2.5) : Float -> 6.25) 145 ;; "propagation" of typeclass constraints to other constrained fns 146 ;; (memsq tests the same thing?) 147 (define (square2 [x : X] #:where (Num X) -> X) 148 (square x)) 149 (check-type (square2 5) : Int -> 25) 150 (check-type (square2 2.5) : Float -> 6.25) 151 (define (squares [xyz : (× X Y Z)] #:where (Num X) (Num Y) (Num Z)-> (× X Y Z)) 152 (match2 xyz with 153 [(x,y,z) -> (tup (square x) (square y) (square z))])) 154 (check-type (squares (tup 5 5 5)) : (× Int Int Int) -> (tup 25 25 25)) 155 (check-type (squares (tup 2.5 5 5)) : (× Float Int Int) -> (tup 6.25 25 25)) 156 (check-type (squares (tup 5 2.5 5)) : (× Int Float Int) -> (tup 25 6.25 25)) 157 (check-type (squares (tup 5 5 2.5)) : (× Int Int Float) -> (tup 25 25 6.25)) 158 (check-type (squares (tup 2.5 2.5 2.5)) : (× Float Float Float) -> (tup 6.25 6.25 6.25)) 159 (typecheck-fail (squares (tup 5 5 #f)) #:with-msg "\\(Num Bool\\) instance undefined") 160 (typecheck-fail (squares (tup 5 #f 5)) #:with-msg "\\(Num Bool\\) instance undefined") 161 (typecheck-fail (squares (tup #f 5 5)) #:with-msg "\\(Num Bool\\) instance undefined") 162 163 ;; -------------------------------------------------- 164 165 (define-type (TypeA X) (A [x : X] [y : X])) 166 167 ;; constraint of nested tyvar 168 (define (test-a1 [a : (TypeA X)] #:where (Eq X) -> Bool) 169 (== (A-x a) (A-y a))) 170 (check-type (test-a1 (A 1 2)) : Bool -> #f) 171 (check-type (test-a1 (A "1" "2")) : Bool -> #f) 172 (typecheck-fail (test-a1 (A #t #f)) 173 #:with-msg 174 "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool") 175 176 (define (test-a2 [a : (TypeA X)] [fa : (→ (TypeA X) X)] #:where (Eq X) -> Bool) 177 (== (fa a) (fa a))) 178 179 (check-type (test-a2 (A 1 2) (inst A-x Int)) : Bool -> #t) 180 (check-type (test-a2 (A "1" "2") (inst A-x String)) : Bool -> #t) 181 182 (define-type (Heap X) 183 Emp 184 (H X)) 185 186 (define (hf [h : (Heap X)] #:where (Ord X) -> Bool) 187 (match h with 188 [Emp -> #f] 189 [H x -> (lte x x)])) 190 191 (check-type (hf (H 1)) : Bool -> #t) 192 (typecheck-fail (hf (H #f)) 193 #:with-msg 194 "Ord Bool.*instance undefined.*Cannot instantiate function with constraints.*Ord X.*with.*X : Bool") 195 196 ;; type classes for non-base types 197 (define-instance (Eq X) => (Eq (List X)) 198 [== (λ ([l1 : (List X)] [l2 : (List X)]) 199 (match2 (tup l1 l2) with 200 [(nil,nil) -> #t] 201 [((x :: xs),(y :: ys)) -> (and (== x y) (== xs ys))] 202 [_ -> #f]))]) 203 204 ;; nil and nil 205 (check-type (== (nil {Int}) (nil {Int})) : Bool -> #t) 206 ;; TODO: better err msg? 207 ;; as of 2016-04-04: "== operation undefined for input types: Int, Bool" 208 ;; should somehow indicate that the two values are not equal because types differ? 209 (typecheck-fail (== (nil {Int}) (nil {Bool}))) 210 ;; nil and non-nil 211 (check-type (== (nil {Int}) (list 1)) : Bool -> #f) 212 (check-type (== (nil {Int}) (cons 1 nil)) : Bool -> #f) 213 (check-type (== (nil {Int}) (cons 1 (cons 2 nil))) : Bool -> #f) 214 ;; non-nil and nil 215 (check-type (== (list 1) (nil {Int})) : Bool -> #f) 216 (check-type (== (cons 1 nil) (nil {Int})) : Bool -> #f) 217 (check-type (== (cons 1 (cons 2 nil)) (nil {Int})) : Bool -> #f) 218 ;; non-nil and non-nil 219 (check-type (== (list 1) (list 1)) : Bool -> #t) 220 (check-type (== (cons 1 nil) (list 1)) : Bool -> #t) 221 (check-type (== (list 1) (cons 1 nil)) : Bool -> #t) 222 (check-type (== (list 1) (list 1 2)) : Bool -> #f) 223 (check-type (== (list 1 2) (list 1)) : Bool -> #f) 224 (check-type (== (list 1 2) (list 1 2)) : Bool -> #t) 225 (check-type (== (list 1 2) (list 1 3)) : Bool -> #f) 226 (check-type (== (list 1 3) (list 1 2)) : Bool -> #f) 227 228 (define (list-eq1 [l1 : (List X)] [l2 : (List X)] #:where (Eq X) -> Bool) 229 (== l1 l2)) 230 231 (check-type (list-eq1 (nil {Int}) (nil {Int})) : Bool -> #t) 232 (check-type (list-eq1 (nil {Int}) (list 1)) : Bool -> #f) 233 (check-type (list-eq1 (list 1) (nil {Int})) : Bool -> #f) 234 (check-type (list-eq1 (list 1) (list 1)) : Bool -> #t) 235 (check-type (list-eq1 (list 1) (list 2)) : Bool -> #f) 236 (check-type (list-eq1 (list 1) (list 1 2)) : Bool -> #f) 237 238 (check-type (member? (list 1) (list (list 1))) : Bool -> #t) 239 (check-type (member? (list 1) (list (list 2))) : Bool -> #f) 240 (check-type (member? (list 1) (list (list 2) (list 1))) : Bool -> #t) 241 242 (define (id-fn2 [xs : (List X)] #:where (Eq X) -> (List X)) xs) 243 (typecheck-fail (id-fn2 (list #f)) #:with-msg "\\(Eq Bool\\) instance undefined") 244 (check-type (id-fn2 (list 1)) : (List Int) -> (list 1)) 245 246 ;; TODO: #:where TC, where TC has a tycon, like #:where (List X) 247 ;; still doesnt work I dont think 248 #;(define (list-eq2 [l1 : (List X)] [l2 : (List X)] #:where (List X) -> Bool) 249 (== l1 l2)) 250 251 ;; TODO: implement subclasses 252 ;; 2016-05-25: Done. see memsq2 253 (define (memsq? [x : X] [xs : (List X)] #:where (Eq X) (Num X) -> Bool) 254 (member? (square x) xs)) 255 (check-type (memsq? 1 (list 1)) : Bool -> #t) 256 (check-type (memsq? 2 (list 2)) : Bool -> #f) 257 (check-type (memsq? 2 (list 3 4)) : Bool -> #t) 258 (typecheck-fail (memsq? (list 1) (list (list 1))) 259 #:with-msg "\\(Num \\(List Int\\)\\) instance undefined") 260 261 262 (define (andmap [p? : (→ X Bool)] [lst : (List X)] -> Bool) 263 (match lst with 264 [[] -> #t] 265 [x :: xs -> (and (p? x) (andmap p? xs))])) 266 267 ;; Set 268 ;; type classes for non-base types: user-defined 269 (define-type (Set X) (MkSet (List X))) 270 (define-instance (Eq X) => (Eq (Set X)) 271 [== (λ ([s1 : (Set X)] [s2 : (Set X)]) 272 (match2 (tup s1 s2) with 273 [((MkSet xs),(MkSet ys)) -> (and (andmap (λ ([y : X]) (member? y xs)) ys) 274 (andmap (λ ([x : X]) (member? x ys)) xs))]))]) 275 (check-type (== (MkSet (list 1)) (MkSet (list 1))) : Bool -> #t) 276 (check-type (== (MkSet (list 1)) (MkSet (list 2))) : Bool -> #f) 277 (check-type (== (MkSet (list 1 2)) (MkSet (list 1 2))) : Bool -> #t) 278 (check-type (== (MkSet (list 1 2)) (MkSet (list 2 1))) : Bool -> #t) 279 (check-type (== (MkSet (list 1 2)) (MkSet (list 1 2 3))) : Bool -> #f) 280 (check-type (== (MkSet (list 3 1 2)) (MkSet (list 1 2 3))) : Bool -> #t) 281 282 (check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1 2)))) : Bool -> #t) 283 (check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1)) (MkSet (list 2 1)))) 284 : Bool -> #t) 285 (check-type (member? (MkSet (list "1" "2")) (list (MkSet (list "1")) (MkSet (list "2" "1")))) 286 : Bool -> #t) 287 288 ;; type classes for non-base types: multiple constraints 289 (define-instance (Eq X) (Eq Y) => (Eq (× X Y)) 290 [== (λ ([p1 : (× X Y)] [p2 : (× X Y)]) 291 (match2 (tup p1 p2) with 292 [((u,v),(x,y)) -> (and (== u x) (== v y))]))]) 293 294 (check-type (== (tup 1 2) (tup 3 4)) : Bool -> #f) 295 (check-type (== (tup 1 2) (tup 1 2)) : Bool -> #t) 296 (check-type (== (tup (list 1) (list 2)) (tup (list 1) (list 2))) : Bool -> #t) 297 (check-type (== (tup (list 1) (list 1 2)) (tup (list 1) (list 2 1))) : Bool -> #f) 298 (check-type (== (tup (list #\a) (list #\b)) (tup (list #\a) (list #\b))) 299 : Bool -> #t) 300 (check-type (== (tup (list #\a) (list #\a #\b)) (tup (list #\a) (list #\b #\a))) 301 : Bool -> #f) 302 303 (check-type (== (tup (list #\a) (list 1)) (tup (list #\a) (list 1))) 304 : Bool -> #t) 305 (check-type (== (tup (list #\a) (list 1 2)) (tup (list #\a) (list 2 1))) 306 : Bool -> #f) 307 308 (check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6))) : Bool -> #f) 309 (check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6) (tup 1 2))) 310 : Bool -> #t) 311 (check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6"))) 312 : Bool -> #f) 313 (check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6") (tup 1 "2"))) 314 : Bool -> #t) 315 (check-type 316 (member? 317 (tup (list 1) "2") 318 (list (tup (list 3) "4") (tup (list 5) "6"))) 319 : Bool -> #f) 320 (check-type 321 (member? 322 (tup (list 1) "2") 323 (list (tup (list 3) "4") (tup (list 5) "6") (tup (list 1) "2"))) 324 : Bool -> #t) 325 326 (define-typeclass (Eq X) => (Num2 X) 327 [ad : (→ X X X)] 328 [sb : (→ X X X)] 329 [mu : (→ X X X)]) 330 331 (typecheck-fail 332 (define-instance (Num2 Bool) 333 [ad +] [sb -] [mu *]) 334 #:with-msg "No instance defined for \\(Eq Bool\\)") 335 336 (define-instance (Num2 Int) 337 [ad +] [sb -] [mu *]) 338 339 (define (f/sub1 [x : X] #:where (Num2 X) -> X) 340 (ad x x)) 341 #;(typecheck-fail ; fails 342 (define (f/sub2 [x : X] #:where (Num2 X) -> X) (== x x)) 343 #:with-msg "Body has type Bool, expected/given X") 344 (define (f/sub2 [x : X] #:where (Num2 X) -> Bool) 345 (== x x)) 346 347 (check-type f/sub1 : (=>/test (Num2 X) (→ X X))) 348 (check-type f/sub2 : (=>/test (Num2 X) (→ X Bool))) 349 350 (check-type (f/sub1 1) : Int -> 2) 351 (typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined") 352 (check-type (f/sub2 1) : Bool -> #t) 353 (typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined") 354 355 (define-instance (Num2 Float) 356 [ad fl+] [sb fl-] [mu fl*]) 357 358 (define (square3 [x : X] #:where (Num2 X) -> X) 359 (mu x x)) 360 (check-type (square3 5) : Int -> 25) 361 (check-type (square3 2.5) : Float -> 6.25) 362 (define (memsq2? [x : X] [xs : (List X)] #:where (Num2 X) -> Bool) 363 (member? (square3 x) xs)) 364 (check-type (memsq2? 1 (list 1)) : Bool -> #t) 365 (check-type (memsq2? 2 (list 2)) : Bool -> #f) 366 (check-type (memsq2? 2 (list 3 4)) : Bool -> #t) 367 (typecheck-fail (memsq2? (list 1) (list (list 1))) 368 #:with-msg "\\(Num2 \\(List Int\\)\\) instance undefined") 369 (typecheck-fail (memsq2? #f (list #f)) 370 #:with-msg "\\(Num2 Bool\\) instance undefined") 371 372 (define-typeclass (Top X) 373 [fun1 : (→ X X X)]) 374 (define-typeclass (Top X) => (Left X) 375 [fun2 : (→ X X X)]) 376 (define-typeclass (Top X) => (Right X) 377 [fun3 : (→ X X X)]) 378 (define-typeclass (Left X) (Right X) => (Bottom X) 379 [fun4 : (→ X X X)]) 380 381 (define-instance (Top Int) 382 [fun1 +]) 383 (define-instance (Left Int) 384 [fun2 +]) 385 (define-instance (Right Int) 386 [fun3 +]) 387 (define-instance (Bottom Int) 388 [fun4 +]) 389 (define (left-fun2 [x : X] #:where (Left X) -> X) 390 (fun2 x x)) 391 (check-type (left-fun2 6) : Int -> 12) 392 (define (left-fun1 [x : X] #:where (Left X) -> X) 393 (fun1 x x)) 394 (check-type (left-fun1 6) : Int -> 12) 395 (define (bott-fun4 [x : X] #:where (Bottom X) -> X) 396 (fun4 x x)) 397 (check-type (bott-fun4 5) : Int -> 10) 398 (define (bott-fun3 [x : X] #:where (Bottom X) -> X) 399 (fun3 x x)) 400 (check-type (bott-fun3 5) : Int -> 10) 401 (define (bott-fun2 [x : X] #:where (Bottom X) -> X) 402 (fun2 x x)) 403 (check-type (bott-fun2 5) : Int -> 10) 404 (define (bott-fun-Int [x : Int] -> Int) 405 (fun1 x x)) 406 (check-type (bott-fun-Int 5) : Int -> 10) 407 ;; lookup more than one parent level 408 (define (bott-fun1 [x : X] #:where (Bottom X) -> X) 409 (fun1 x x)) 410 (check-type (bott-fun1 5) : Int -> 10) 411 412 ;; non-base typeclass instances with subclassing 413 (define-instance (Top X) => (Top (List X)) 414 [fun1 (λ ([l1 : (List X)] [l2 : (List X)]) 415 (match2 (tup l1 l2) with 416 [(nil,nil) -> l2] 417 [((x :: xs),(y :: ys)) -> (cons (fun1 x y) (fun1 xs ys))] 418 [_ -> l1]))]) 419 (define (top-list-fun1 [xs : (List X)] #:where (Top X) -> (List X)) 420 (fun1 xs xs)) 421 (check-type (top-list-fun1 (list 5)) : (List Int) -> (list 10)) 422 (check-type (top-list-fun1 (list 5 6)) : (List Int) -> (list 10 12)) 423 424 (define-instance (Left X) => (Left (List X)) 425 [fun2 (λ ([l1 : (List X)] [l2 : (List X)]) 426 (match2 (tup l1 l2) with 427 [(nil,nil) -> l2] 428 [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun2 x1 y1) (fun2 xs1 ys1))] 429 [_ -> l1]))]) 430 431 (define (left-list-fun2 [zs : (List X)] #:where (Left X) -> (List X)) 432 (fun2 zs zs)) 433 (check-type (left-list-fun2 (list 6)) : (List Int) -> (list 12)) 434 (define (left-list-fun1 [xx : (List X)] #:where (Left X) -> (List X)) 435 (fun1 xx xx)) 436 (check-type (left-list-fun1 (list 6)) : (List Int) -> (list 12)) 437 438 ;; can use fun1 (from Top), for both X and (List X), 439 ;; in both instance def, and regular fns 440 (define-instance (Right X) => (Right (List X)) 441 [fun3 (λ ([l1 : (List X)] [l2 : (List X)]) 442 (match2 (tup l1 l2) with 443 [(nil,nil) -> l2] 444 [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun1 x1 y1) (fun1 xs1 ys1))] 445 [_ -> l1]))]) 446 (define (right-list-fun1 [xx : (List X)] #:where (Right X) -> (List X)) 447 (fun1 xx xx)) 448 (check-type (right-list-fun1 (list 6)) : (List Int) -> (list 12)) 449 450 (define-instance (Bottom X) => (Bottom (List X)) 451 [fun4 (λ ([l1 : (List X)] [l2 : (List X)]) 452 (match2 (tup l1 l2) with 453 [(nil,nil) -> l2] 454 [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun4 x1 y1) (fun4 xs1 ys1))] 455 [_ -> l1]))]) 456 457 ;; lookup more than one parent level 458 (define (bott-list-fun1 [xs : (List X)] #:where (Bottom X) -> (List X)) 459 (fun1 xs xs)) 460 (check-type (bott-list-fun1 (list 5)) : (List Int) -> (list 10))