www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

stlc+occurrence-tests.rkt (16687B)

      1 #lang s-exp "../stlc+occurrence.rkt"
      2 (require turnstile/examples/tests/rackunit-typechecking)
      3 
      4 ;; -----------------------------------------------------------------------------
      5 ;; basic types & syntax
      6 
      7 (check-type 1 : Int)
      8 (check-type #f : Boolean)
      9 (check-type "hello" : Str)
     10 (check-type 1 : Top)
     11 (check-type (λ ([x : (∪ Boolean Int)]) x)
     12             : (→ (∪ Boolean Int) (∪ Boolean Int)))
     13 
     14 (typecheck-fail
     15  (λ ([x : ∪]) x)
     16  #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
     17 (typecheck-fail
     18  (λ ([x : (∪)]) x)
     19  #:with-msg "Improper usage of type constructor ∪")
     20 (typecheck-fail
     21  (λ ([x : (∪ ∪)]) x)
     22  #:with-msg "Improper usage of type constructor ∪")
     23 (typecheck-fail
     24  (λ ([x : (1 ∪)]) x)
     25  #:with-msg "")
     26 (typecheck-fail
     27  (λ ([x : (Int ∪)]) x)
     28  #:with-msg "expected identifier")
     29 (typecheck-fail
     30  (λ ([x : (→ ∪ ∪)]) x)
     31  #:with-msg "Improper usage of type constructor ∪")
     32 (typecheck-fail
     33  (λ ([x : (→ Int ∪)]) x)
     34  #:with-msg "Improper usage of type constructor ∪: ∪, expected >= 1 arguments")
     35 (typecheck-fail
     36  (λ ([x : (∪ Int →)]) x)
     37  #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
     38 
     39 ;; -----------------------------------------------------------------------------
     40 ;; --- type evaluation
     41 
     42 (check-type (λ ([x : (∪ Int Int Int Int)]) x)
     43             : (→ Int Int))
     44 (check-type (λ ([x : (∪ Int Boolean)]) 42)
     45             : (→ (∪ Boolean Int) Int))
     46 (check-type (λ ([x : (∪ Int Boolean Boolean Int)]) x)
     47             : (→ (∪ Boolean Int) (∪ Boolean Int)))
     48 (check-type (λ ([x : (∪ (∪ Int Boolean))]) 42)
     49             : (→ (∪ Int Boolean) Int))
     50 (check-type (λ ([x : (∪ Int Boolean)]) 42)
     51             : (→ (∪ (∪ Int Boolean)) Int))
     52 (check-type (λ ([x : (∪ Int Boolean)]) 42)
     53             : (→ (∪ (∪ Int Boolean) (∪ Int Boolean)) Int))
     54 
     55 
     56 ;; -----------------------------------------------------------------------------
     57 ;; --- subtyping
     58 
     59 ;; ---- basics
     60 (check-type 1 : (∪ Int))
     61 (check-type 1 : (∪ (∪ Int)))
     62 (check-type (λ ([x : Int]) x)
     63             : (→ Bot Top))
     64 
     65 (check-not-type 1 : (∪ Boolean))
     66 
     67 ;; - AMB : t <: t' => t <: (U ... t' ...)
     68 (check-type 1 : (∪ Boolean Int))
     69 (check-type -1 : (∪ Int Boolean))
     70 (check-type 1 : (∪ Boolean Int (→ Boolean Boolean)))
     71 (check-type 1 : (∪ (∪ Int Boolean) (∪ Int Boolean)))
     72 
     73 (check-not-type 1 : (∪ Boolean (→ Int Int)))
     74 
     75 ;; --- EXT : (U t' ...) <: (U t t' ...)
     76 (check-type (λ ([x : (∪ Int Boolean)]) x)
     77             : (→ (∪ Int Boolean) (∪ Int Boolean Str)))
     78 (check-type (λ ([x : (∪ Int Boolean)]) x)
     79             : (→ (∪ Boolean) (∪ Int Boolean Str)))
     80 
     81 (check-not-type (λ ([x : (∪ Int Boolean)]) x)
     82             : (→ (∪ Int Boolean) (∪ Int)))
     83 (check-not-type (λ ([x : (∪ Int Boolean)]) x)
     84             : (→ (∪ Boolean Int Str) (∪ Int Boolean)))
     85 
     86 ;; --- SUB : a<:b => (U a t' ...) <: (U b t' ...)
     87 (check-type (λ ([x : (∪ Int Str)]) x)
     88             : (→ (∪ Int Str) (∪ Num Str)))
     89 (check-type (λ ([x : (∪ Int Str)]) x)
     90             : (→ (∪ Nat Str) (∪ Num Str)))
     91 
     92 (check-type (λ ([x : (∪ Int Str)]) x)
     93             : (→ (∪ Int Str) Top))
     94 
     95 (check-not-type (λ ([x : (∪ Int Str)]) x)
     96             : (→ Top (∪ Num Str)))
     97 
     98 ;; --- ALL
     99 (check-type (λ ([x : (∪ Boolean Int Str)]) x)
    100             : (→ (∪ Boolean Int Str) Top))
    101 (check-type (λ ([x : (∪ Nat Int Num)]) x)
    102             : (→ (∪ Nat Int Num) Num))
    103 (check-type (λ ([x : (∪ Nat Int Num)]) x)
    104             : (→ Nat Num))
    105 
    106 ;; --- misc
    107 ;; Because Int<:(U Int ...)
    108 (check-type (λ ([x : (∪ Int Nat)]) #t)
    109                   : (→ Int Boolean))
    110 
    111 ;; -----------------------------------------------------------------------------
    112 ;; --- Basic Filters (applying functions)
    113 
    114 ;; --- is-boolean?
    115 (check-type
    116  (λ ([x : (∪ Boolean Int)])
    117     (test [Boolean ? x]
    118           #t
    119           #f))
    120  : (→ (∪ Boolean Int) Boolean))
    121 (check-type
    122  ((λ ([x : (∪ Boolean Int)])
    123      (test (Boolean ? x)
    124            #t
    125            #f)) #t)
    126   : Boolean ⇒ #t)
    127 (check-type
    128  ((λ ([x : (∪ Boolean Int)])
    129      (test (Boolean ? x)
    130            #t
    131            #f)) 902)
    132   : Boolean ⇒ #f)
    133 
    134 ;; --- successor
    135 (check-type
    136  (λ ([x : (∪ Int Boolean)])
    137     (test (Int ? x)
    138           (+ 1 x)
    139           0))
    140  : (→ (∪ Int Boolean) (∪ Num Nat)))
    141 (check-type
    142  ((λ ([x : (∪ Int Boolean)])
    143     (test (Int ? x)
    144           (+ 1 x)
    145           0)) #f)
    146  : Num ⇒ 0)
    147 (check-type
    148  ((λ ([x : (∪ Int Boolean)])
    149     (test (Int ? x)
    150           (+ 1 x)
    151           1)) #t)
    152  : Num ⇒ 1)
    153 (check-type
    154  ((λ ([x : (∪ Int Boolean)])
    155     (test (Int ? x)
    156           (+ 1 x)
    157           0)) 9000)
    158  : Num ⇒ 9001)
    159 
    160 ;; ;; --- Do-nothing filter
    161 (check-type
    162  (λ ([x : Int])
    163     (test (Int ? x) #t #f))
    164  : (→ Int Boolean))
    165 (check-type
    166  (λ ([x : Int])
    167     (test (Boolean ? x) 0 x))
    168  : (→ Int (∪ Nat Int)))
    169 
    170 ;; --- Filter a subtype
    171 (check-type
    172  (λ ([x : (∪ Nat Boolean)])
    173     (test (Int ? x)
    174           x
    175           x))
    176  : (→ (∪ Nat Boolean) (∪ Int (∪ Nat Boolean))))
    177 
    178 (check-type
    179  (λ ([x : (∪ Int Boolean)])
    180     (test (Nat ? x)
    181           x
    182           x))
    183  : (→ (∪ Boolean Int) (∪ Int Nat Boolean)))
    184 
    185 ;; --- Filter a supertype
    186 (check-type
    187  (λ ([x : (∪ Int Boolean)])
    188     (test (Num ? x)
    189           1
    190           x))
    191  : (→ (∪ Boolean Int) (∪ Nat Boolean)))
    192 
    193 (check-type
    194  ((λ ([x : (∪ Int Boolean)])
    195      (test (Num ? x)
    196            #f
    197            x)) #t)
    198  : Boolean
    199  ⇒ #t)
    200 
    201 ;; Should filter all the impossible types 
    202 (check-type
    203  ((λ ([x : (∪ Nat Int Num Boolean)])
    204      (test (Num ? x)
    205            #f
    206            x)) #t)
    207  : Boolean
    208  ⇒ #t)
    209 
    210 ;; Can refine non-union types
    211 (check-type
    212  ((λ ([x : Top])
    213     (test (Str ? x)
    214           x
    215           "nope"))
    216   "yes")
    217  : Str ⇒ "yes")
    218 
    219 ;; ----------------------------------------------------------------------------- 
    220 ;; --- misc subtyping + filters (regression tests)
    221 (check-type
    222  (λ ([x : (∪ Int Boolean)])
    223     (test (Int ? x)
    224           0
    225           1))
    226  : (→ (∪ Int Boolean) Nat))
    227 (check-type
    228  (λ ([x : (∪ Int Boolean)])
    229     (test (Int ? x)
    230           0
    231           1))
    232  : (→ (∪ Int Boolean) Int))
    233 
    234 ;; -----------------------------------------------------------------------------
    235 ;; --- Invalid filters
    236 
    237 (typecheck-fail
    238  (λ ([x : (∪ Int Boolean)])
    239     (test (1 ? x) #t #f))
    240  #:with-msg "not a well-formed type")
    241 (typecheck-fail
    242  (test (1 ? 1) #t #f)
    243  #:with-msg "not a well-formed type")
    244 (typecheck-fail
    245  (test (1 ? 1) #t #f)
    246  #:with-msg "not a well-formed type")
    247 (typecheck-fail
    248  (test (#f ? #t) #t #f)
    249  #:with-msg "not a well-formed type")
    250 
    251 ;; -----------------------------------------------------------------------------
    252 ;; --- Subtypes should not be collapsed
    253 
    254 (check-not-type (λ ([x : (∪ Int Nat)]) #t)
    255                 : (→ Num Boolean))
    256 (check-type ((λ ([x : (∪ Int Nat Boolean)])
    257                 (test (Int ? x)
    258                       2
    259                       (test (Nat ? x)
    260                             1
    261                             0)))
    262              #t)
    263             : Nat ⇒ 0)
    264 (check-type ((λ ([x : (∪ Int Nat)])
    265                 (test (Nat ? x)
    266                       1
    267                       (test (Int ? x)
    268                             2
    269                             0)))
    270              1)
    271             : Nat ⇒ 1)
    272 (check-type ((λ ([x : (∪ Int Nat)])
    273                 (test (Int ? x)
    274                       2
    275                       (test (Nat ? x)
    276                             1
    277                             0)))
    278              -10)
    279             : Nat ⇒ 2)
    280                
    281 ;; -----------------------------------------------------------------------------
    282 ;; --- Functions in union
    283 
    284 (check-type (λ ([x : (∪ Int (∪ Nat) (∪ (→ Int Str Int)) (→ (→ (→ Int Int)) Int))]) #t)
    285             : (→ (∪ Int Nat (→ Int Str Int) (→ (→ (→ Int Int)) Int)) Boolean))
    286 
    287 (check-type (λ ([x : (∪ Int (→ Int Int))]) #t)
    288             : (→ Int Boolean))
    289 
    290 ;; --- filter functions
    291 (check-type
    292  (λ ([x : (∪ Int (→ Int Int))])
    293     (test ((→ Int Int) ? x)
    294           (x 0)
    295           x))
    296  : (→ (∪ Int (→ Int Int)) Int))
    297 
    298 (check-type
    299  (λ ([x : (∪ (→ Int Int Int) (→ Int Int))])
    300     (test ((→ Int Int) ? x)
    301           (x 0)
    302     (test (Int ? x)
    303           x
    304           (x 1 0))))
    305  : (→ (∪ (→ Int Int Int) (→ Int Int)) Int))
    306 
    307 (check-type
    308  ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
    309     (test ((→ Int Int) ? x)
    310           (x 0)
    311     (test (Int ? x)
    312           x
    313           (x 1 0)))) 1)
    314  : Int ⇒ 1)
    315 
    316 (check-type
    317  ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
    318     (test ((→ Int Int) ? x)
    319           (x 0)
    320     (test (Int ? x)
    321           x
    322           (x 1 0)))) (λ ([y : Int]) 5))
    323  : Int ⇒ 5)
    324 
    325 (check-type
    326  ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
    327     (test ((→ Int Int) ? x)
    328           (x 0)
    329     (test (Int ? x)
    330           x
    331           (x 1 0)))) (λ ([y : Int] [z : Int]) z))
    332  : Int ⇒ 0)
    333 
    334 ;; --- disallow same-arity functions
    335 (typecheck-fail
    336  (λ ([x : (∪ (→ Int Int) (→ Str Str))]) 1)
    337  #:with-msg "Cannot discriminate")
    338 
    339 ;; -----------------------------------------------------------------------------
    340 ;; --- Filter with unions
    341 
    342 (check-type
    343  (λ ([x : (∪ Int Str)])
    344   (test ((∪ Int Str) ? x)
    345         x
    346         "nope"))
    347  : (→ (∪ Int Str) (∪ Int Str)))
    348 
    349 (check-type
    350  (λ ([x : (∪ Int Str Boolean)])
    351     (test ((∪ Int Str) ? x)
    352           x
    353           "Nope"))
    354  : (→ (∪ Int Str Boolean) (∪ Int Str)))
    355 
    356 (check-type
    357  (λ ([x : (∪ Int Str Boolean)])
    358     (test ((∪ Int Str) ? x)
    359           (test (Str ? x)
    360                 "yes"
    361                 "int")
    362           "bool"))
    363  : (→ (∪ Int Str Boolean) Str))
    364 
    365 (check-type
    366  ((λ ([x : (∪ Str Boolean)])
    367      (test ((∪ Int Nat Num) ? x)
    368            x
    369            (+ 1 2))) "hi")
    370  : Num ⇒ 3)
    371 
    372 (check-type
    373   ((λ ([x : (∪ Str Int Boolean)])
    374       (test ((∪ Int Str) ? x)
    375             x
    376             "error")) 1)
    377   : (∪ Str Int) ⇒ 1)
    378 
    379 (check-type
    380   ((λ ([x : (∪ Str Int Boolean)])
    381       (test ((∪ Int Str) ? x)
    382             x
    383             "error")) "hi")
    384   : (∪ Int Str) ⇒ "hi")
    385 
    386 ;; -----------------------------------------------------------------------------
    387 ;; --- Subtyping products
    388 
    389 (check-type (tup 1) : (× Nat))
    390 (check-type (tup 1) : (× Int))
    391 (check-type (tup 1) : (× Num))
    392 (check-type (tup 1) : (× Top))
    393 (check-type (tup 1) : Top)
    394 
    395 (check-not-type (tup 1) : Boolean)
    396 (check-not-type (tup 1) : Str)
    397 (check-not-type (tup 1) : (× Str))
    398 (check-not-type (tup 1) : (× Int Str))
    399 (check-not-type (tup 1) : Bot)
    400 
    401 (check-type (tup 1 2 3) : (× Int Nat Num))
    402 (check-type (tup 1 2 3) : (× Num Nat Num))
    403 (check-type (tup 1 2 3) : (× Top Top Num))
    404 (check-type (tup 1 "2" 3) : (× Int Top Int))
    405 
    406 (check-not-type (tup 1 2 3) : (× Nat Nat Str))
    407 
    408 ;; -----------------------------------------------------------------------------
    409 ;; --- Latent filters (on products)
    410 
    411 (check-type
    412  (λ ([v : (× (∪ Int Str) Int)])
    413     (test (Int ? (proj v 0))
    414           (+ (proj v 0) (proj v 1))
    415           0))
    416  : (→ (× (∪ Int Str) Int) Num))
    417 
    418 (check-type
    419  ((λ ([v : (× (∪ Int Str) Int)])
    420     (test (Int ? (proj v 0))
    421           (+ (proj v 0) (proj v 1))
    422           0))
    423   (tup ((λ ([x : (∪ Int Str)]) x) -2) -3))
    424  : Num ⇒ -5)
    425 
    426 (check-type
    427  ((λ ([v : (× (∪ Int Str) Int)])
    428     (test (Int ? (proj v 0))
    429           (+ (proj v 0) (proj v 1))
    430           0))
    431   (tup "hi" -3))
    432  : Num ⇒ 0)
    433 
    434 ;; --- Use a product as filter
    435 
    436 (check-type
    437  (λ ([x : (∪ Int (× Int Int Int))])
    438     (test (Int ? x)
    439           (+ 1 x)
    440           (+ (proj x 0) (+ (proj x 1) (proj x 2)))))
    441  : (→ (∪ (× Int Int Int) Int) Num))
    442 
    443 (check-type
    444  ((λ ([x : (∪ Int (× Int Int Int))])
    445      (test (Int ? x)
    446            (+ 1 x)
    447            (+ (proj x 0) (+ (proj x 1) (proj x 2)))))
    448   0)
    449  : Num ⇒ 1)
    450 
    451 (check-type
    452  ((λ ([x : (∪ Int (× Int Int Int))])
    453      (test (Int ? x)
    454            (+ 1 x)
    455            (+ (proj x 0) (+ (proj x 1) (proj x 2)))))
    456   (tup 2 2 2))
    457  : Num ⇒ 6)
    458 
    459 (check-type
    460  ((λ ([x : (∪ Int (× Str Nat) (× Int Int Int))])
    461      (test (Int ? x)
    462            (+ 1 x)
    463      (test ((× Int Int Int) ? x)
    464            (+ (proj x 0) (+ (proj x 1) (proj x 2)))
    465            (proj x 1))))
    466   (tup 2 2 2))
    467  : Num ⇒ 6)
    468 
    469 (check-type
    470  ((λ ([x : (∪ Int (× Str Nat) (× Int Int Int))])
    471      (test (Int ? x)
    472            (+ 1 x)
    473      (test ((× Int Int Int) ? x)
    474            (+ (proj x 0) (+ (proj x 1) (proj x 2)))
    475            (proj x 1))))
    476   (tup "yolo" 33))
    477  : Num ⇒ 33)
    478 
    479 ;; -- All together now
    480 
    481 (check-type
    482  ((λ ([x : (∪ Int (× Boolean Boolean) (× Int (∪ Str Int)))])
    483      (test (Int ? x)
    484            "just an int"
    485      (test ((× Boolean Boolean) ? x)
    486            "pair of bools"
    487            (test (Str ? (proj x 1))
    488                  (proj x 1)
    489                  "pair of ints"))))
    490   (tup 33 "success"))
    491  : Str ⇒ "success")
    492 
    493 (check-type
    494  ((λ ([x : (∪ Int (× Int Int) (× Int (∪ Str Int)))])
    495      (test (Int ? x)
    496            "just an int"
    497      (test ((× Int Int) ? x)
    498            "pair of ints"
    499            (test (Str ? (proj x 1))
    500                  (proj x 1)
    501                  "another pair of ints"))))
    502   (tup 33 "success"))
    503  : Str ⇒ "success")
    504 
    505 ;; -----------------------------------------------------------------------------
    506 ;; --- Filter lists
    507 
    508 (check-type
    509  (λ ([x : (List (∪ Int Str))])
    510     (test ((List Str) ? x)
    511           x
    512           #f))
    513  : (→ (List (∪ Int Str)) (∪ Boolean (List Str))))
    514 
    515 ;; -- -subtyping lists
    516 (check-type
    517  (cons 1 (nil {Nat}))
    518  : (List Int))
    519 
    520 (check-type
    521  ((λ ([filter/3 : (→ (List (∪ Int Str)) (List Int))]
    522       [add*/3 : (→ Num (List Num) (List Num))]
    523       [xs : (×  (∪ Int Str) (∪ Int Str) (∪ Int Str))])
    524      (add*/3 5 (filter/3 (cons (proj xs 0)
    525                                (cons (proj xs 1)
    526                                      (cons (proj xs 2)
    527                                            (nil {(∪ Str Int)})))))))
    528   ;; filter (okay this is a little tricky for recursion)
    529   (λ ([xs : (List (∪ Int Str))])
    530      ((λ ([v1 : (∪ Int Str)]
    531           [v2 : (∪ Int Str)]
    532           [v3 : (∪ Int Str)])
    533          (test (Int ? v1)
    534                (cons v1 (test (Int ? v2)
    535                               (cons v2 (test (Int ? v3)
    536                                              (cons v3 (nil {Int}))
    537                                              (nil {Int})))
    538                               (test (Int ? v3)
    539                                     (cons v3 (nil {Int}))
    540                                     (nil {Int}))))
    541                (test (Int ? v2)
    542                      (cons v2 (test (Int ? v3)
    543                                     (cons v3 (nil {Int}))
    544                                     (nil {Int})))
    545                      (test (Int ? v3)
    546                            (cons v3 (nil {Int}))
    547                            (nil {Int})))))
    548       (head xs) (head (tail xs)) (head (tail (tail xs)))))
    549   ;; add3
    550   (λ ([n : Num] [xs : (List Num)])
    551      (cons (+ n (head xs))
    552       (cons (+ n (head (tail xs)))
    553        (cons (+ n (head (tail (tail xs))))
    554         (nil {Num})))))
    555   ;; xs (3-tuple)
    556   (tup 1 "foo" 3))
    557  : (List Num))
    558 
    559 ;; -----------------------------------------------------------------------------
    560 ;; --- ICFP'10 examples
    561 
    562 ;; -- Exaple 1 (x can have any type)
    563 (check-type
    564  (λ ([x : Top])
    565     (test (Num ? x)
    566        (+ 1 x)
    567        0))
    568  : (→ Top Num))
    569 
    570 ;; -- Example 2
    571 (check-type
    572  (λ ([x : (∪ Str Num)]
    573      [str-length : (→ Str Num)])
    574     (test (Num ? x)
    575           (+ 1 x)
    576           (str-length x)))
    577  : (→ (∪ Str Num) (→ Str Num) Num))
    578 
    579 ;; -- TODO Example 3 (requires IF)
    580 ;; (check-type
    581 ;;  (λ ([member : (→ Num (List Num) Boolean)])
    582 ;;     (λ ([x : Num] [l : (List Num)])
    583 ;;        (if (member x l)
    584 ;;            <compute with x>
    585 ;;            <fail>)))
    586 ;;  : <compute-result>
    587 
    588 ;; -- Example 4
    589 (check-type
    590  (λ ([x : (∪ Num Str Top)] [f : (→ (∪ Num Str) Num)])
    591     (test ((∪ Num Str) ? x)
    592           (f x)
    593           0))
    594  : (→ (∪ Num Str Top) (→ (∪ Num Str) Num) Num))
    595 
    596 ;; Exmample 10 (we don't allow non-homogenous lists, so need to select head before filtering)
    597 (check-type
    598  (λ ([p : (List (∪ Nat Str))])
    599     ((λ ([x : (∪ Nat Str)])
    600        (test (Num ? x)
    601              (+ 1 x)
    602              7))
    603     (head p)))
    604  : (→ (List (∪ Nat Str)) Num))
    605 
    606 ;; -----------------------------------------------------------------------------
    607 ;; --- TODO CPS filters
    608 
    609 ;; -----------------------------------------------------------------------------
    610 ;; --- TODO Filter on values (should do nothing)
    611 
    612 ;; (check-type
    613 ;;  (test (Int ? 1) #t #f)
    614 ;;  : Boolean)
    615 
    616 ;; -----------------------------------------------------------------------------
    617 ;; --- TODO Values as filters (check equality)
    618