generic.mlish (17230B)
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 (string-append "Type error defining typeclass instance \\(Num Int\\).*" 134 (expected "(→ Int Int Int), (→ Int Int Int), (→ Int Int Int)" 135 #:given "(→ Int Int Int), (→ Int Int Int), (→ Float Float Float)"))) 136 137 (define-instance (Num Int) 138 [add +] [sub -] [mul *]) 139 (define-instance (Num Float) 140 [add fl+] [sub fl-] [mul fl*]) 141 142 (define (square [x : X] #:where (Num X) -> X) 143 (mul x x)) 144 (check-type (square 5) : Int -> 25) 145 (check-type (square 2.5) : Float -> 6.25) 146 ;; "propagation" of typeclass constraints to other constrained fns 147 ;; (memsq tests the same thing?) 148 (define (square2 [x : X] #:where (Num X) -> X) 149 (square x)) 150 (check-type (square2 5) : Int -> 25) 151 (check-type (square2 2.5) : Float -> 6.25) 152 (define (squares [xyz : (× X Y Z)] #:where (Num X) (Num Y) (Num Z)-> (× X Y Z)) 153 (match2 xyz with 154 [(x,y,z) -> (tup (square x) (square y) (square z))])) 155 (check-type (squares (tup 5 5 5)) : (× Int Int Int) -> (tup 25 25 25)) 156 (check-type (squares (tup 2.5 5 5)) : (× Float Int Int) -> (tup 6.25 25 25)) 157 (check-type (squares (tup 5 2.5 5)) : (× Int Float Int) -> (tup 25 6.25 25)) 158 (check-type (squares (tup 5 5 2.5)) : (× Int Int Float) -> (tup 25 25 6.25)) 159 (check-type (squares (tup 2.5 2.5 2.5)) : (× Float Float Float) -> (tup 6.25 6.25 6.25)) 160 (typecheck-fail (squares (tup 5 5 #f)) #:with-msg "\\(Num Bool\\) instance undefined") 161 (typecheck-fail (squares (tup 5 #f 5)) #:with-msg "\\(Num Bool\\) instance undefined") 162 (typecheck-fail (squares (tup #f 5 5)) #:with-msg "\\(Num Bool\\) instance undefined") 163 164 ;; -------------------------------------------------- 165 166 (define-type (TypeA X) (A [x : X] [y : X])) 167 168 ;; constraint of nested tyvar 169 (define (test-a1 [a : (TypeA X)] #:where (Eq X) -> Bool) 170 (== (A-x a) (A-y a))) 171 (check-type (test-a1 (A 1 2)) : Bool -> #f) 172 (check-type (test-a1 (A "1" "2")) : Bool -> #f) 173 (typecheck-fail (test-a1 (A #t #f)) 174 #:with-msg 175 "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool") 176 177 (define (test-a2 [a : (TypeA X)] [fa : (→ (TypeA X) X)] #:where (Eq X) -> Bool) 178 (== (fa a) (fa a))) 179 180 (check-type (test-a2 (A 1 2) (inst A-x Int)) : Bool -> #t) 181 (check-type (test-a2 (A "1" "2") (inst A-x String)) : Bool -> #t) 182 183 (define-type (Heap X) 184 Emp 185 (H X)) 186 187 (define (hf [h : (Heap X)] #:where (Ord X) -> Bool) 188 (match h with 189 [Emp -> #f] 190 [H x -> (lte x x)])) 191 192 (check-type (hf (H 1)) : Bool -> #t) 193 (typecheck-fail (hf (H #f)) 194 #:with-msg 195 "Ord Bool.*instance undefined.*Cannot instantiate function with constraints.*Ord X.*with.*X : Bool") 196 197 ;; type classes for non-base types 198 (define-instance (Eq X) => (Eq (List X)) 199 [== (λ ([l1 : (List X)] [l2 : (List X)]) 200 (match2 (tup l1 l2) with 201 [(nil,nil) -> #t] 202 [((x :: xs),(y :: ys)) -> (and (== x y) (== xs ys))] 203 [_ -> #f]))]) 204 205 ;; nil and nil 206 (check-type (== (nil {Int}) (nil {Int})) : Bool -> #t) 207 ;; TODO: better err msg? 208 ;; as of 2016-04-04: "== operation undefined for input types: Int, Bool" 209 ;; should somehow indicate that the two values are not equal because types differ? 210 (typecheck-fail (== (nil {Int}) (nil {Bool}))) 211 ;; nil and non-nil 212 (check-type (== (nil {Int}) (list 1)) : Bool -> #f) 213 (check-type (== (nil {Int}) (cons 1 nil)) : Bool -> #f) 214 (check-type (== (nil {Int}) (cons 1 (cons 2 nil))) : Bool -> #f) 215 ;; non-nil and nil 216 (check-type (== (list 1) (nil {Int})) : Bool -> #f) 217 (check-type (== (cons 1 nil) (nil {Int})) : Bool -> #f) 218 (check-type (== (cons 1 (cons 2 nil)) (nil {Int})) : Bool -> #f) 219 ;; non-nil and non-nil 220 (check-type (== (list 1) (list 1)) : Bool -> #t) 221 (check-type (== (cons 1 nil) (list 1)) : Bool -> #t) 222 (check-type (== (list 1) (cons 1 nil)) : Bool -> #t) 223 (check-type (== (list 1) (list 1 2)) : Bool -> #f) 224 (check-type (== (list 1 2) (list 1)) : Bool -> #f) 225 (check-type (== (list 1 2) (list 1 2)) : Bool -> #t) 226 (check-type (== (list 1 2) (list 1 3)) : Bool -> #f) 227 (check-type (== (list 1 3) (list 1 2)) : Bool -> #f) 228 229 (define (list-eq1 [l1 : (List X)] [l2 : (List X)] #:where (Eq X) -> Bool) 230 (== l1 l2)) 231 232 (check-type (list-eq1 (nil {Int}) (nil {Int})) : Bool -> #t) 233 (check-type (list-eq1 (nil {Int}) (list 1)) : Bool -> #f) 234 (check-type (list-eq1 (list 1) (nil {Int})) : Bool -> #f) 235 (check-type (list-eq1 (list 1) (list 1)) : Bool -> #t) 236 (check-type (list-eq1 (list 1) (list 2)) : Bool -> #f) 237 (check-type (list-eq1 (list 1) (list 1 2)) : Bool -> #f) 238 239 (check-type (member? (list 1) (list (list 1))) : Bool -> #t) 240 (check-type (member? (list 1) (list (list 2))) : Bool -> #f) 241 (check-type (member? (list 1) (list (list 2) (list 1))) : Bool -> #t) 242 243 (define (id-fn2 [xs : (List X)] #:where (Eq X) -> (List X)) xs) 244 (typecheck-fail (id-fn2 (list #f)) #:with-msg "\\(Eq Bool\\) instance undefined") 245 (check-type (id-fn2 (list 1)) : (List Int) -> (list 1)) 246 247 ;; TODO: #:where TC, where TC has a tycon, like #:where (List X) 248 ;; still doesnt work I dont think 249 #;(define (list-eq2 [l1 : (List X)] [l2 : (List X)] #:where (List X) -> Bool) 250 (== l1 l2)) 251 252 ;; TODO: implement subclasses 253 ;; 2016-05-25: Done. see memsq2 254 (define (memsq? [x : X] [xs : (List X)] #:where (Eq X) (Num X) -> Bool) 255 (member? (square x) xs)) 256 (check-type (memsq? 1 (list 1)) : Bool -> #t) 257 (check-type (memsq? 2 (list 2)) : Bool -> #f) 258 (check-type (memsq? 2 (list 3 4)) : Bool -> #t) 259 (typecheck-fail (memsq? (list 1) (list (list 1))) 260 #:with-msg "\\(Num \\(List Int\\)\\) instance undefined") 261 262 263 (define (andmap [p? : (→ X Bool)] [lst : (List X)] -> Bool) 264 (match lst with 265 [[] -> #t] 266 [x :: xs -> (and (p? x) (andmap p? xs))])) 267 268 ;; Set 269 ;; type classes for non-base types: user-defined 270 (define-type (Set X) (MkSet (List X))) 271 (define-instance (Eq X) => (Eq (Set X)) 272 [== (λ ([s1 : (Set X)] [s2 : (Set X)]) 273 (match2 (tup s1 s2) with 274 [((MkSet xs),(MkSet ys)) -> (and (andmap (λ ([y : X]) (member? y xs)) ys) 275 (andmap (λ ([x : X]) (member? x ys)) xs))]))]) 276 (check-type (== (MkSet (list 1)) (MkSet (list 1))) : Bool -> #t) 277 (check-type (== (MkSet (list 1)) (MkSet (list 2))) : Bool -> #f) 278 (check-type (== (MkSet (list 1 2)) (MkSet (list 1 2))) : Bool -> #t) 279 (check-type (== (MkSet (list 1 2)) (MkSet (list 2 1))) : Bool -> #t) 280 (check-type (== (MkSet (list 1 2)) (MkSet (list 1 2 3))) : Bool -> #f) 281 (check-type (== (MkSet (list 3 1 2)) (MkSet (list 1 2 3))) : Bool -> #t) 282 283 (check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1 2)))) : Bool -> #t) 284 (check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1)) (MkSet (list 2 1)))) 285 : Bool -> #t) 286 (check-type (member? (MkSet (list "1" "2")) (list (MkSet (list "1")) (MkSet (list "2" "1")))) 287 : Bool -> #t) 288 289 ;; type classes for non-base types: multiple constraints 290 (define-instance (Eq X) (Eq Y) => (Eq (× X Y)) 291 [== (λ ([p1 : (× X Y)] [p2 : (× X Y)]) 292 (match2 (tup p1 p2) with 293 [((u,v),(x,y)) -> (and (== u x) (== v y))]))]) 294 295 (check-type (== (tup 1 2) (tup 3 4)) : Bool -> #f) 296 (check-type (== (tup 1 2) (tup 1 2)) : Bool -> #t) 297 (check-type (== (tup (list 1) (list 2)) (tup (list 1) (list 2))) : Bool -> #t) 298 (check-type (== (tup (list 1) (list 1 2)) (tup (list 1) (list 2 1))) : Bool -> #f) 299 (check-type (== (tup (list #\a) (list #\b)) (tup (list #\a) (list #\b))) 300 : Bool -> #t) 301 (check-type (== (tup (list #\a) (list #\a #\b)) (tup (list #\a) (list #\b #\a))) 302 : Bool -> #f) 303 304 (check-type (== (tup (list #\a) (list 1)) (tup (list #\a) (list 1))) 305 : Bool -> #t) 306 (check-type (== (tup (list #\a) (list 1 2)) (tup (list #\a) (list 2 1))) 307 : Bool -> #f) 308 309 (check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6))) : Bool -> #f) 310 (check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6) (tup 1 2))) 311 : Bool -> #t) 312 (check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6"))) 313 : Bool -> #f) 314 (check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6") (tup 1 "2"))) 315 : Bool -> #t) 316 (check-type 317 (member? 318 (tup (list 1) "2") 319 (list (tup (list 3) "4") (tup (list 5) "6"))) 320 : Bool -> #f) 321 (check-type 322 (member? 323 (tup (list 1) "2") 324 (list (tup (list 3) "4") (tup (list 5) "6") (tup (list 1) "2"))) 325 : Bool -> #t) 326 327 (define-typeclass (Eq X) => (Num2 X) 328 [ad : (→ X X X)] 329 [sb : (→ X X X)] 330 [mu : (→ X X X)]) 331 332 (typecheck-fail 333 (define-instance (Num2 Bool) 334 [ad +] [sb -] [mu *]) 335 #:with-msg "No instance defined for \\(Eq Bool\\)") 336 337 (define-instance (Num2 Int) 338 [ad +] [sb -] [mu *]) 339 340 (define (f/sub1 [x : X] #:where (Num2 X) -> X) 341 (ad x x)) 342 #;(typecheck-fail ; fails 343 (define (f/sub2 [x : X] #:where (Num2 X) -> X) (== x x)) 344 #:with-msg "Body has type Bool, expected/given X") 345 (define (f/sub2 [x : X] #:where (Num2 X) -> Bool) 346 (== x x)) 347 348 (check-type f/sub1 : (=>/test (Num2 X) (→ X X))) 349 (check-type f/sub2 : (=>/test (Num2 X) (→ X Bool))) 350 351 (check-type (f/sub1 1) : Int -> 2) 352 (typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined") 353 (check-type (f/sub2 1) : Bool -> #t) 354 (typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined") 355 356 (define-instance (Num2 Float) 357 [ad fl+] [sb fl-] [mu fl*]) 358 359 (define (square3 [x : X] #:where (Num2 X) -> X) 360 (mu x x)) 361 (check-type (square3 5) : Int -> 25) 362 (check-type (square3 2.5) : Float -> 6.25) 363 (define (memsq2? [x : X] [xs : (List X)] #:where (Num2 X) -> Bool) 364 (member? (square3 x) xs)) 365 (check-type (memsq2? 1 (list 1)) : Bool -> #t) 366 (check-type (memsq2? 2 (list 2)) : Bool -> #f) 367 (check-type (memsq2? 2 (list 3 4)) : Bool -> #t) 368 (typecheck-fail (memsq2? (list 1) (list (list 1))) 369 #:with-msg "\\(Num2 \\(List Int\\)\\) instance undefined") 370 (typecheck-fail (memsq2? #f (list #f)) 371 #:with-msg "\\(Num2 Bool\\) instance undefined") 372 373 (define-typeclass (Top X) 374 [fun1 : (→ X X X)]) 375 (define-typeclass (Top X) => (Left X) 376 [fun2 : (→ X X X)]) 377 (define-typeclass (Top X) => (Right X) 378 [fun3 : (→ X X X)]) 379 (define-typeclass (Left X) (Right X) => (Bottom X) 380 [fun4 : (→ X X X)]) 381 382 (define-instance (Top Int) 383 [fun1 +]) 384 (define-instance (Left Int) 385 [fun2 +]) 386 (define-instance (Right Int) 387 [fun3 +]) 388 (define-instance (Bottom Int) 389 [fun4 +]) 390 (define (left-fun2 [x : X] #:where (Left X) -> X) 391 (fun2 x x)) 392 (check-type (left-fun2 6) : Int -> 12) 393 (define (left-fun1 [x : X] #:where (Left X) -> X) 394 (fun1 x x)) 395 (check-type (left-fun1 6) : Int -> 12) 396 (define (bott-fun4 [x : X] #:where (Bottom X) -> X) 397 (fun4 x x)) 398 (check-type (bott-fun4 5) : Int -> 10) 399 (define (bott-fun3 [x : X] #:where (Bottom X) -> X) 400 (fun3 x x)) 401 (check-type (bott-fun3 5) : Int -> 10) 402 (define (bott-fun2 [x : X] #:where (Bottom X) -> X) 403 (fun2 x x)) 404 (check-type (bott-fun2 5) : Int -> 10) 405 (define (bott-fun-Int [x : Int] -> Int) 406 (fun1 x x)) 407 (check-type (bott-fun-Int 5) : Int -> 10) 408 ;; lookup more than one parent level 409 (define (bott-fun1 [x : X] #:where (Bottom X) -> X) 410 (fun1 x x)) 411 (check-type (bott-fun1 5) : Int -> 10) 412 413 ;; non-base typeclass instances with subclassing 414 (define-instance (Top X) => (Top (List X)) 415 [fun1 (λ ([l1 : (List X)] [l2 : (List X)]) 416 (match2 (tup l1 l2) with 417 [(nil,nil) -> l2] 418 [((x :: xs),(y :: ys)) -> (cons (fun1 x y) (fun1 xs ys))] 419 [_ -> l1]))]) 420 (define (top-list-fun1 [xs : (List X)] #:where (Top X) -> (List X)) 421 (fun1 xs xs)) 422 (check-type (top-list-fun1 (list 5)) : (List Int) -> (list 10)) 423 (check-type (top-list-fun1 (list 5 6)) : (List Int) -> (list 10 12)) 424 425 (define-instance (Left X) => (Left (List X)) 426 [fun2 (λ ([l1 : (List X)] [l2 : (List X)]) 427 (match2 (tup l1 l2) with 428 [(nil,nil) -> l2] 429 [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun2 x1 y1) (fun2 xs1 ys1))] 430 [_ -> l1]))]) 431 432 (define (left-list-fun2 [zs : (List X)] #:where (Left X) -> (List X)) 433 (fun2 zs zs)) 434 (check-type (left-list-fun2 (list 6)) : (List Int) -> (list 12)) 435 (define (left-list-fun1 [xx : (List X)] #:where (Left X) -> (List X)) 436 (fun1 xx xx)) 437 (check-type (left-list-fun1 (list 6)) : (List Int) -> (list 12)) 438 439 ;; can use fun1 (from Top), for both X and (List X), 440 ;; in both instance def, and regular fns 441 (define-instance (Right X) => (Right (List X)) 442 [fun3 (λ ([l1 : (List X)] [l2 : (List X)]) 443 (match2 (tup l1 l2) with 444 [(nil,nil) -> l2] 445 [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun1 x1 y1) (fun1 xs1 ys1))] 446 [_ -> l1]))]) 447 (define (right-list-fun1 [xx : (List X)] #:where (Right X) -> (List X)) 448 (fun1 xx xx)) 449 (check-type (right-list-fun1 (list 6)) : (List Int) -> (list 12)) 450 451 (define-instance (Bottom X) => (Bottom (List X)) 452 [fun4 (λ ([l1 : (List X)] [l2 : (List X)]) 453 (match2 (tup l1 l2) with 454 [(nil,nil) -> l2] 455 [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun4 x1 y1) (fun4 xs1 ys1))] 456 [_ -> l1]))]) 457 458 ;; lookup more than one parent level 459 (define (bott-list-fun1 [xs : (List X)] #:where (Bottom X) -> (List X)) 460 (fun1 xs xs)) 461 (check-type (bott-list-fun1 (list 5)) : (List Int) -> (list 10))