www

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

infer-variances.mlish (10203B)

      1 #lang s-exp "../../mlish.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 (define-type T1 t1)
      5 ;; No type arguments to determine variance for.
      6 
      7 (check-type t1 : T1 -> t1)
      8 
      9 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     10 
     11 ;; Non-Recursive Types
     12 
     13 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     14 
     15 (define-type (T2 X) t2)
     16 ;; X should be inferred to be irrelevant within (T2 X).
     17 ;; That means it should be both covariant and contravariant.
     18 
     19 ;; This checks that X is covariant within (T2 X).
     20 (define (t2* → (T2 X)) t2)
     21 (define (t2** → (→ (T2 X))) (inst t2* X))
     22 (check-type (t2**) : (→/test (T2 X)))
     23 
     24 ;; This checks that X is contravariant within (T2 X),
     25 ;; by checking that X is covariant within (→ (T2 X) Int).
     26 (define (t2->int [t2 : (T2 X)] → Int) 0)
     27 (define (t2->int* → (→ (T2 X) Int)) (inst t2->int X))
     28 (check-type (t2->int*) : (→/test (T2 X) Int))
     29 
     30 ;; This checks that X is irrelevant, even within a Ref type,
     31 ;; by checking that X is covariant within (Ref (T2 X)).
     32 ;; This is still sound because a value of type (Ref (T2 X)) will never
     33 ;; contain anything of type X anyway. X is irrelevant within it.
     34 (define (ref-t2* → (Ref (T2 X))) (ref (t2 {X})))
     35 (define (ref-t2** → (→ (Ref (T2 X)))) (inst ref-t2* X))
     36 (check-type (ref-t2**) : (→/test (Ref (T2 X))))
     37 
     38 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     39 
     40 (define-type (T3 X) t3-none (t3-some X))
     41 ;; X should be inferred to be covariant within (T3 X).
     42 
     43 ;; This checks that X is covariant within (T3 X).
     44 (define (t3-none* → (T3 X)) t3-none)
     45 (define (t3-none** → (→ (T3 X))) (inst t3-none* X))
     46 (check-type (t3-none**) : (→/test (T3 X)))
     47 
     48 ;; This checks that X is not contravariant within (T3 X),
     49 ;; by checking that X is not covariant within (→ (T3 X) Int).
     50 (define (t3->int [t3 : (T3 X)] → Int) 0)
     51 (define (t3->int* → (→ (T3 X) Int)) (inst t3->int X))
     52 (typecheck-fail (t3->int*))
     53 
     54 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     55 
     56 (define-type (T4 X) t4-none (t4-some (→ X Int)))
     57 ;; X should be inferred to be contravariant within (T4 X).
     58 
     59 ;; This checks that X is not covariant within (T4 X).
     60 (define (t4-none* → (T4 X)) t4-none)
     61 (define (t4-none** → (→ (T4 X))) (inst t4-none* X))
     62 (typecheck-fail (t4-none**))
     63 
     64 ;; This checks that X is contravariant within (T4 X),
     65 ;; by checking that X is covariant within (→ (T4 X) Int).
     66 (define (t4->int [t4 : (T4 X)] → Int) 0)
     67 (define (t4->int* → (→ (T4 X) Int)) (inst t4->int X))
     68 (check-type (t4->int*) : (→/test (T4 X) Int))
     69 
     70 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     71 
     72 (define-type (T5 X) t5-none (t5-some+ X) (t5-some- (→ X Int)))
     73 ;; X should be inferred to be invariant within (T5 X).
     74 
     75 ;; This checks that X is not covariant within (T5 X).
     76 (define (t5-none* → (T5 X)) t5-none)
     77 (define (t5-none** → (→ (T5 X))) (inst t5-none* X))
     78 (typecheck-fail (t5-none**))
     79 
     80 ;; This checks that X is not contravariant within (T5 X),
     81 ;; by checking that X is not covariant within (→ (T5 X) Int).
     82 (define (t5->int [t5 : (T5 X)] → Int) 0)
     83 (define (t5->int* → (→ (T5 X) Int)) (inst t5->int X))
     84 (typecheck-fail (t5->int*))
     85 
     86 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     87 
     88 ;; Recursive Types
     89 
     90 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
     91 
     92 (define-type (T6 X) t6-none (t6-same (T6 X)))
     93 ;; X should be inferred to be irrelevant within (T6 X).
     94 
     95 ;; This checks that X is covariant within (T6 X).
     96 (define (t6-none* → (T6 X)) t6-none)
     97 (define (t6-none** → (→ (T6 X))) (inst t6-none* X))
     98 (check-type (t6-none**) : (→/test (T6 X)))
     99 
    100 ;; This checks that X is contravariant within (T6 X),
    101 ;; by checking that X is covariant within (→ (T6 X) Int).
    102 (define (t6->int [t6 : (T6 X)] → Int) 0)
    103 (define (t6->int* → (→ (T6 X) Int)) (inst t6->int X))
    104 (check-type (t6->int*) : (→/test (T6 X) Int))
    105 
    106 ;; This checks that X is irrelevant, even within a Ref type,
    107 ;; by checking that X is covariant within (Ref (T6 X)).
    108 ;; This is still sound because a value of type (Ref (T6 X)) will never
    109 ;; contain anything of type X anyway. X is irrelevant within it.
    110 (define (ref-t6* → (Ref (T6 X))) (ref (t6-none {X})))
    111 (define (ref-t6** → (→ (Ref (T6 X)))) (inst ref-t6* X))
    112 (check-type (ref-t6**) : (→/test (Ref (T6 X))))
    113 
    114 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    115 
    116 (define-type (T7 X) t7-none (t7-weird (→ (T7 X) Int)))
    117 (define-type (T8 X) t8-none (t8-weird (T8 (→ X Int))))
    118 (define-type (T9 X) t9-none (t9-weird (→ (T9 (→ X Int)) Int)))
    119 ;; X should be inferred to be irrelevant within (T7 X), (T8 X), and
    120 ;; (T9 X). None of these types could contain or recieve an actual X.
    121 
    122 (define-type (T10 X) (t10 (T7 X) (T8 X) (T9 X)))
    123 ;; So because of that, X should be irrelevant within (T10 X).
    124 
    125 ;; This checks that X is covariant within (T10 X).
    126 (define (t10-none* → (T10 X)) (t10 t7-none t8-none t9-none))
    127 (define (t10-none** → (→ (T10 X))) (inst t10-none* X))
    128 (check-type (t10-none**) : (→/test (T10 X)))
    129 
    130 ;; This checks that X is contravariant within (T10 X),
    131 ;; by checking that X is covariant within (→ (T10 X) Int).
    132 (define (t10->int [t10 : (T10 X)] → Int) 0)
    133 (define (t10->int* → (→ (T10 X) Int)) (inst t10->int X))
    134 (check-type (t10->int*) : (→/test (T10 X) Int))
    135 
    136 ;; This checks that X is irrelevant, even within a Ref type,
    137 ;; by checking that X is covariant within (Ref (T10 X)).
    138 ;; This is still sound because a value of type (Ref (T10 X)) will never
    139 ;; contain anything of type X anyway. X is irrelevant within it.
    140 (define (ref-t10* → (Ref (T10 X))) (ref (t10 (t7-none {X}) (t8-none {X}) (t9-none {X}))))
    141 (define (ref-t10** → (→ (Ref (T10 X)))) (inst ref-t10* X))
    142 (check-type (ref-t10**) : (→/test (Ref (T10 X))))
    143 
    144 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    145 
    146 (define-type (T11 X) t11-none (t11+ X) (t11-weird (→ (T11 X) Int)))
    147 (define-type (T12 X) t12-none (t12+ X) (t12-weird (T12 (→ X Int))))
    148 (define-type (T13 X) t13-none (t13+ X)
    149   (t13-weird (→ (T13 (→ X Int)) Int)))
    150 (define-type (T14 X) t14-none (t14- (→ X Int))
    151   (t14-weird (→ (T14 (→ X Int)) Int)))
    152 ;; X should be inferred to be invariant within (T11 X) and (T12 X),
    153 ;; but covariant within (T13 X), and contravariant within (T14 X).
    154 
    155 ;; This checks that X is covariant within (T13 X), but not any of the
    156 ;; others.
    157 (define (t11-none* → (T11 X)) t11-none)
    158 (define (t12-none* → (T12 X)) t12-none)
    159 (define (t13-none* → (T13 X)) t13-none)
    160 (define (t14-none* → (T14 X)) t14-none)
    161 (define (t11-none** → (→ (T11 X))) (inst t11-none* X))
    162 (define (t12-none** → (→ (T12 X))) (inst t12-none* X))
    163 (define (t13-none** → (→ (T13 X))) (inst t13-none* X))
    164 (define (t14-none** → (→ (T14 X))) (inst t14-none* X))
    165 (typecheck-fail (t11-none**))
    166 (typecheck-fail (t12-none**))
    167 (check-type (t13-none**) : (→/test (T13 X)))
    168 (typecheck-fail (t14-none**))
    169 
    170 ;; This checks that X is contravariant within (T14 X), but not any of
    171 ;; the others.
    172 (define (t11->int [t11 : (T11 X)] → Int) 0)
    173 (define (t12->int [t12 : (T12 X)] → Int) 0)
    174 (define (t13->int [t13 : (T13 X)] → Int) 0)
    175 (define (t14->int [t14 : (T14 X)] → Int) 0)
    176 (define (t11->int* → (→ (T11 X) Int)) (inst t11->int X))
    177 (define (t12->int* → (→ (T12 X) Int)) (inst t12->int X))
    178 (define (t13->int* → (→ (T13 X) Int)) (inst t13->int X))
    179 (define (t14->int* → (→ (T14 X) Int)) (inst t14->int X))
    180 (typecheck-fail (t11->int*))
    181 (typecheck-fail (t12->int*))
    182 (typecheck-fail (t13->int*))
    183 (check-type (t14->int*) : (→/test (T14 X) Int))
    184 
    185 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    186 
    187 (define-type (T15 X) t15-none (t15-cons+ X (T15 X)))
    188 (define-type (T16 X) t16-none (t16-cons- (→ X Int) (T16 X)))
    189 ;; X should be inferred to be covariant within (T15 X), and
    190 ;; contravariant within (T16 X). (T15 X) is just like a (List X) type,
    191 ;; and (T16 X) is just like a (List (→ X Int)).
    192 
    193 ;; This checks that X is covariant within (T15 X).
    194 (define (t15-none* → (T15 X)) t15-none)
    195 (define (t15-none** → (→ (T15 X))) (inst t15-none* X))
    196 (check-type (t15-none**) : (→/test (T15 X)))
    197 ;; This checks that X is not covariant within (T16 X).
    198 (define (t16-none* → (T16 X)) t16-none)
    199 (define (t16-none** → (→ (T16 X))) (inst t16-none* X))
    200 (typecheck-fail (t16-none**))
    201 
    202 ;; This checks that X is not contravariant within (T15 X),
    203 ;; by checking that X is not covariant within (→ (T15 X) Int).
    204 (define (t15->int [t15 : (T15 X)] → Int) 0)
    205 (define (t15->int* → (→ (T15 X) Int)) (inst t15->int X))
    206 (typecheck-fail (t15->int*))
    207 ;; This checks that X is contravariant within (T16 X),
    208 ;; by checking that X is covariant within (→ (T16 X) Int).
    209 (define (t16->int [t16 : (T16 X)] → Int) 0)
    210 (define (t16->int* → (→ (T16 X) Int)) (inst t16->int X))
    211 (check-type (t16->int*) : (→/test (T16 X) Int))
    212 
    213 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    214 
    215 ;; Mutually Recursive Types
    216 
    217 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
    218 
    219 (define-type (T17 X) (t17-some X) (t18 (T18 X)))
    220 (define-type (T18 X) t18-none (t18-cons (T17 X) (T18 X)))
    221 ;; X should be inferred to be covariant in both (T17 X) and (T18 X).
    222 ;; This is similar to an arbitrary-arity tree type.
    223 
    224 ;; This checks that X is covariant within (T17 X).
    225 (define (t17-none* → (T17 X)) (t18 t18-none))
    226 (define (t17-none** → (→ (T17 X))) (inst t17-none* X))
    227 (check-type (t17-none**) : (→/test (T17 X)))
    228 ;; This checks that X is covariant within (T18 X).
    229 (define (t18-none* → (T18 X)) t18-none)
    230 (define (t18-none** → (→ (T18 X))) (inst t18-none* X))
    231 (check-type (t18-none**) : (→/test (T18 X)))
    232 
    233 ;; This checks that X is not contravariant within (T17 X),
    234 ;; by checking that X is not covariant within (→ (T17 X) Int).
    235 (define (t17->int [t17 : (T17 X)] → Int) 0)
    236 (define (t17->int* → (→ (T17 X) Int)) (inst t17->int X))
    237 (typecheck-fail (t17->int*))
    238 ;; This checks that X is not contravariant within (T18 X),
    239 ;; by checking that X is not covariant within (→ (T18 X) Int).
    240 (define (t18->int [t18 : (T18 X)] → Int) 0)
    241 (define (t18->int* → (→ (T18 X) Int)) (inst t18->int X))
    242 (typecheck-fail (t18->int*))
    243