www

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

inst.mlish (2070B)

      1 #lang s-exp "../../mlish.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 ;; tests for instantiation of polymorphic functions and constructors
      5 
      6 (define-type (Result A B)
      7   (Ok A)
      8   (Error B))
      9 
     10 (define (ok [a : A] -> (Result A B))
     11   (Ok a))
     12 
     13 (check-type ok : (→/test A (Result A B))) ; test inferred
     14 (check-type (inst ok Int String) : (→/test Int (Result Int String)))
     15 
     16 (define (f -> (Result Int String))
     17   (ok 1))
     18 
     19 (check-type f : (→/test (Result Int String)))
     20 
     21 (define (g -> (Result Int String))
     22   (Ok 1))
     23 
     24 (check-type g : (→/test (Result Int String)))
     25 
     26 (define (h -> (Result Int Y))
     27   (Ok 1))
     28 
     29 (check-type h : (→/test (Result Int Y)))
     30 
     31 (define (i -> (Result Int String))
     32   (h))
     33 
     34 (check-type i : (→/test (Result Int String)))
     35 
     36 (define (f/cond [b : Bool] -> (Result Int String))
     37   (cond [b (ok 1)]
     38         [else (ok 0)]))
     39 
     40 (check-type f/cond : (→/test Bool (Result Int String)))
     41 
     42 (define-type-alias (Read-Result A) (Result (× A (List Char)) String))
     43 
     44 (define (alias-test -> (Read-Result A))
     45   (Error "asd"))
     46 
     47 (check-type alias-test : (→/test (Result (× A (List Char)) String)))
     48 (check-type alias-test : (→/test (Read-Result A)))
     49 
     50 (define (alias-test2 [in : A] -> (Read-Result A))
     51   (ok (tup in nil)))
     52 (define (alias-test3 [in : A] -> (Read-Result A))
     53   (ok (tup in (list #\a #\b #\c))))
     54 
     55 (check-type alias-test2 : (→/test A (Result (× A (List Char)) String)))
     56 (check-type alias-test2 : (→/test A (Read-Result A)))
     57 (check-type alias-test3 : (→/test A (Result (× A (List Char)) String)))
     58 (check-type alias-test3 : (→/test A (Read-Result A)))
     59 
     60 (check-type alias-test2 : (→/test B (Result (× B (List Char)) String)))
     61 (check-type alias-test2 : (→/test B (Read-Result B)))
     62 (check-type alias-test3 : (→/test B (Result (× B (List Char)) String)))
     63 (check-type alias-test3 : (→/test B (Read-Result B)))
     64 
     65 (define (expect-listof-int [loi : (List Int)] → Int)
     66   0)
     67 
     68 (check-type (expect-listof-int nil) : Int -> 0)
     69 
     70 (define (expect-→listof-int [f : (→ (List Int))] → Int)
     71   0)
     72 
     73 (check-type (expect-→listof-int (λ () nil)) : Int -> 0)
     74