variance-constraints.rkt (17045B)
1 #lang racket/base 2 3 (provide solve-variance-constraints 4 variance-mapping 5 variance= 6 variance-var 7 variance-join/expr 8 variance-compose/expr 9 variance-mapping-ref 10 ) 11 12 (require racket/bool 13 racket/list 14 racket/match 15 racket/set 16 (only-in (for-template "typecheck.rkt") 17 variance? 18 irrelevant 19 covariant 20 contravariant 21 invariant 22 variance-irrelevant? 23 variance-covariant? 24 variance-contravariant? 25 variance-invariant? 26 variance-join 27 variance-compose 28 )) 29 30 (module+ test 31 (require rackunit)) 32 33 ;; variance<=? : Variance Variance -> Boolean 34 ;; irrelevant < covariant 35 ;; irrelevant < contravariant 36 ;; covariant < invariant 37 ;; contravariant < invariant 38 (define (variance<=? v1 v2) 39 (and (implies (variance-covariant? v2) 40 (variance-covariant? v1)) 41 (implies (variance-contravariant? v2) 42 (variance-contravariant? v1)))) 43 44 ;; A Variance-Constraint is a (variance= Variance-Expr Variance-Expr) 45 (struct variance= (v1 v2) #:prefab) 46 ;; variance<= : Variance-Expr Variance-Expr -> Variance-Constraint 47 (define (variance<= v1 v2) 48 (variance= (variance-expr-join v1 v2) v2)) 49 50 ;; A Variance-Expr is one of: 51 ;; - Variance-Var 52 ;; - Variance 53 ;; - (variance-expr-join Variance-Expr Variance-Expr) 54 ;; - (variance-expr-compose Variance-Expr Variance-Expr) 55 (struct variance-expr-join (v1 v2) #:prefab) 56 (struct variance-expr-compose (v1 v2) #:prefab) 57 58 ;; A Variance-Var is a Symbol 59 (define (variance-var sym) sym) 60 (define (variance-var? v) (symbol? v)) 61 (define (variance-var=? v1 v2) (symbol=? v1 v2)) 62 63 ;; A Variance-Mapping is a (Hashof Variance-Var Variance-Expr) 64 ;; variance-mapping : -> Variance-Mapping 65 (define (variance-mapping) (hash)) 66 ;; variance-mapping-has? : Variance-Mapping Variance-Var -> Boolean 67 (define (variance-mapping-has? mapping var) 68 (hash-has-key? mapping var)) 69 ;; variance-mapping-ref : Variance-Mapping Variance-Var -> Variance-Expr 70 (define (variance-mapping-ref mapping var) 71 (hash-ref mapping var)) 72 ;; variance-mapping-set : Variance-Mapping Variance-Var Variance-Expr -> Variance-Mapping 73 (define (variance-mapping-set mapping var variance) 74 (hash-set mapping var variance)) 75 76 ;; An Unfinished-Mapping is a (Hashof Variance-Var Variance) 77 ;; If a var is mapped to something in an Unfinished-Mapping, that 78 ;; means that the var is at least as restrictive as the variance it's 79 ;; mapped to. 80 (define (unfinished-mapping-ref mapping var) 81 (hash-ref mapping var irrelevant)) 82 (define (unfinished-mapping-set mapping var value) 83 (hash-update mapping var (λ (v) (variance-join v value)) irrelevant)) 84 85 ;; solve-variance-constraints : 86 ;; (Listof Variance-Var) (Listof Variance-Constraint) Variance-Mapping 87 ;; -> (U False Variance-Mapping) 88 (define (solve-variance-constraints vars constraints mapping) 89 (match constraints 90 [(list) 91 (variance-mapping-interp-exprs vars mapping)] 92 [(cons constraint rest-cs) 93 (match constraint 94 [(variance= (? variance? v1) (? variance? v2)) 95 (and 96 (equal? v1 v2) 97 (solve-variance-constraints vars rest-cs mapping))] 98 [constraint 99 (define free-vars (variance-constraint-variables #false constraint '())) 100 (cond 101 [(empty? free-vars) 102 (match-define (variance= v1 v2) constraint) 103 (solve-variance-constraints 104 vars 105 (cons (variance= (variance-expr-interp free-vars v1 mapping) 106 (variance-expr-interp free-vars v2 mapping)) 107 rest-cs) 108 mapping)] 109 [else 110 (define valss 111 (for/list ([var (in-list free-vars)]) 112 (list irrelevant covariant contravariant invariant))) 113 (for/or ([vals (in-list (apply cartesian-product valss))]) 114 (define-values [constraints* mapping*] 115 (for/fold ([constraints constraints] [mapping mapping]) 116 ([var (in-list free-vars)] 117 [val (in-list vals)]) 118 (values (variance-constraints-substitute constraints var val) 119 (variance-mapping-set/substitute mapping var val)))) 120 (solve-variance-constraints vars constraints* mapping*))])])])) 121 122 ;; variance-expr-substitute : Variance-Expr Variance-Var Variance-Expr -> Variance-Expr 123 (define (variance-expr-substitute expr var value) 124 (match expr 125 [(? variance-var? v) (if (variance-var=? v var) value v)] 126 [(? variance? v) v] 127 [(variance-expr-join v1 v2) 128 (variance-expr-join (variance-expr-substitute v1 var value) 129 (variance-expr-substitute v2 var value))] 130 [(variance-expr-compose v1 v2) 131 (variance-expr-compose (variance-expr-substitute v1 var value) 132 (variance-expr-substitute v2 var value))])) 133 134 ;; variance-constraint-substitute : 135 ;; Variance-Constraint Variance-Var Variance-Expr -> Variance-Constraint 136 (define (variance-constraint-substitute constraint var value) 137 (match constraint 138 [(variance= v1 v2) 139 (variance= (variance-expr-substitute v1 var value) 140 (variance-expr-substitute v2 var value))])) 141 142 ;; variance-constraints-substitute : 143 ;; (Listof Variance-Constraint) Variance-Var Variance-Expr -> (Listof Variance-Constraint) 144 (define (variance-constraints-substitute constraints var value) 145 (for/list ([constraint (in-list constraints)]) 146 (variance-constraint-substitute constraint var value))) 147 148 ;; variance-mapping-set/substitute : Variance-Mapping Variance-Var Variance-Expr -> Variance-Mapping 149 (define (variance-mapping-set/substitute mapping var value) 150 (variance-mapping-set 151 (for/hash ([(k v) (in-hash mapping)]) 152 (values k (variance-expr-substitute v var value))) 153 var value)) 154 155 ;; variance-constraint-variables : (Listof Variance-Var) Variance-Constraint [(Setof Variance-Var)] -> (Setof Variance-Var) 156 (define (variance-constraint-variables vars constraint [acc (seteq)]) 157 (match constraint 158 [(variance= v1 v2) 159 (variance-expr-variables vars v2 (variance-expr-variables vars v1 acc))])) 160 161 ;; variance-expr-variables : 162 ;; (Listof Variance-Var) Variance-Expr [(Setof Variance-Var)] -> (Setof Variance-Var) 163 (define (variance-expr-variables vars expr [acc (seteq)]) 164 (match expr 165 [(? variance-var? v) 166 (if (implies vars (member v vars)) (set-add acc v) acc)] 167 [(? variance? v) 168 acc] 169 [(variance-expr-join v1 v2) 170 (variance-expr-variables vars v2 (variance-expr-variables vars v1 acc))] 171 [(variance-expr-compose v1 v2) 172 (variance-expr-variables vars v2 (variance-expr-variables vars v1 acc))])) 173 174 ;; variance-mapping-interp-exprs : (Listof Variance-Var) Variance-Mapping -> Variance-Mapping 175 (define (variance-mapping-interp-exprs vars mapping) 176 (for/fold ([mapping mapping]) 177 ([(k v) (in-hash mapping)]) 178 (variance-mapping-set mapping k (variance-expr-interp vars v mapping)))) 179 180 ;; variance-expr-interp : (Listof Variance-Var) Variance-Expr Variance-Mapping -> Variance-Expr 181 (define (variance-expr-interp vars expr mapping) 182 (match expr 183 [(? variance? v) v] 184 [(? variance-var? v) 185 (cond 186 [(variance-mapping-has? mapping v) 187 (define expr (variance-mapping-ref mapping v)) 188 (cond [(member v (variance-expr-variables #f expr '())) 189 (error 'variance-expr-interp "bad stufs is happening right now:\n~v = ~v" v expr) 190 v] 191 [else 192 (variance-expr-interp vars expr mapping)])] 193 [else v])] 194 [(variance-expr-join v1 v2) 195 (variance-join/expr (variance-expr-interp vars v1 mapping) 196 (variance-expr-interp vars v2 mapping))] 197 [(variance-expr-compose v1 v2) 198 (variance-compose/expr (variance-expr-interp vars v1 mapping) 199 (variance-expr-interp vars v2 mapping))])) 200 201 ;; variance-join/expr : Variance-Expr Variance-Expr -> Variance-Expr 202 (define/match (variance-join/expr v1 v2) 203 [[(? variance? v1) (? variance? v2)] (variance-join v1 v2)] 204 [[(? variance? (? variance-invariant? v1)) _] v1] 205 [[_ (? variance? (? variance-invariant? v2))] v2] 206 [[(? variance? (? variance-irrelevant? v1)) v2] v2] 207 [[v1 (? variance? (? variance-irrelevant? v2))] v1] 208 [[v1 v2] #:when (equal? v1 v2) v1] 209 [[v1 v2] (variance-expr-join v1 v2)]) 210 211 ;; variance-compose/expr : Variance-Expr Variance-Expr -> Variance-Expr 212 (define/match (variance-compose/expr v1 v2) 213 [[(? variance? v1) (? variance? v2)] (variance-compose v1 v2)] 214 [[(? variance? (? variance-irrelevant? v1)) _] v1] 215 [[_ (? variance? (? variance-irrelevant? v2))] v2] 216 [[(? variance? (? variance-invariant? v1)) _] v1] 217 [[_ (? variance? (? variance-invariant? v2))] v2] 218 [[(? variance? (? variance-covariant? v1)) v2] v2] 219 [[v1 (? variance? (? variance-covariant? v2))] v1] 220 [[v1 v2] (variance-expr-compose v1 v2)]) 221 222 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 223 224 (module+ test 225 (test-case "variance<=?" 226 (test-case "irrelevant <= everything" 227 (check-true (variance<=? irrelevant irrelevant)) 228 (check-true (variance<=? irrelevant covariant)) 229 (check-true (variance<=? irrelevant contravariant)) 230 (check-true (variance<=? irrelevant invariant))) 231 (test-case "nothing else is <= irrelevant" 232 (check-false (variance<=? covariant irrelevant)) 233 (check-false (variance<=? contravariant irrelevant)) 234 (check-false (variance<=? invariant irrelevant))) 235 (test-case "everything <= invariant" 236 (check-true (variance<=? irrelevant invariant)) 237 (check-true (variance<=? covariant invariant)) 238 (check-true (variance<=? contravariant invariant)) 239 (check-true (variance<=? invariant invariant))) 240 (test-case "invariant is not <= anything else" 241 (check-false (variance<=? invariant irrelevant)) 242 (check-false (variance<=? invariant covariant)) 243 (check-false (variance<=? invariant contravariant))) 244 (test-case "covariant and contravariant are not <= or >=" 245 (check-false (variance<=? covariant contravariant)) 246 (check-false (variance<=? contravariant covariant)))) 247 (test-case "solve-variance-constraints" 248 (check-equal? (solve-variance-constraints 249 (list) (list) (hash)) 250 (hash)) 251 (check-equal? (solve-variance-constraints 252 (list 'a) (list (variance= 'a irrelevant)) (hash)) 253 (hash 'a irrelevant)) 254 (check-equal? (solve-variance-constraints 255 (list 'a) (list (variance= 'a covariant)) (hash)) 256 (hash 'a covariant)) 257 (check-equal? (solve-variance-constraints 258 (list 'a) (list (variance= 'a contravariant)) (hash)) 259 (hash 'a contravariant)) 260 (check-equal? (solve-variance-constraints 261 (list 'a) (list (variance= 'a invariant)) (hash)) 262 (hash 'a invariant)) 263 (check-equal? (solve-variance-constraints 264 (list 'a 'b) 265 (list (variance= (variance-expr-compose covariant 'a) 266 (variance-expr-join covariant 'b))) 267 (hash)) 268 (hash 'a covariant 'b irrelevant)) 269 (check-equal? (solve-variance-constraints 270 (list 'a) 271 (list (variance= 'a 272 (variance-expr-join 273 (variance-expr-join 274 covariant 275 (variance-expr-compose 276 covariant 277 'a)) 278 irrelevant))) 279 (hash)) 280 (hash 'a covariant)) 281 (check-equal? (solve-variance-constraints 282 (list 'a) 283 (list (variance= 'a 284 (variance-expr-join 285 (variance-expr-compose 286 contravariant 287 covariant) 288 irrelevant))) 289 (hash)) 290 (hash 'a contravariant)) 291 (check-equal? (solve-variance-constraints 292 (list 'a) 293 (list (variance= 'a 294 (variance-expr-join 295 (variance-expr-compose 296 contravariant 297 'a) 298 irrelevant))) 299 (hash)) 300 (hash 'a irrelevant)) 301 (check-equal? (solve-variance-constraints 302 (list 'a) 303 (list (variance= 'a 304 (variance-expr-join 305 (variance-expr-compose 306 contravariant 307 'a) 308 covariant))) 309 (hash)) 310 (hash 'a invariant)) 311 (check-equal? (solve-variance-constraints 312 (list 'a) 313 (list (variance= 'a 314 (variance-expr-join 315 (variance-expr-compose 316 covariant 317 covariant) 318 (variance-expr-compose 319 contravariant 320 covariant)))) 321 (hash)) 322 (hash 'a invariant)) 323 (check-equal? (solve-variance-constraints 324 (list 'a) 325 (list (variance= 'a 326 (variance-expr-join 327 (variance-expr-join 328 (variance-expr-compose 329 covariant 330 'a) 331 (variance-expr-compose 332 contravariant 333 'a)) 334 covariant))) 335 (hash)) 336 (hash 'a invariant)) 337 (check-equal? (solve-variance-constraints 338 (list 'a 'b 'c 'd) 339 (list (variance= 'a 340 (variance-expr-join 341 (variance-expr-join 342 (variance-expr-join 343 (variance-expr-compose 344 contravariant 345 covariant) 346 irrelevant) 347 (variance-expr-compose 348 covariant 349 'c)) 350 (variance-expr-compose 351 irrelevant 352 'd))) 353 (variance= 'b 354 (variance-expr-join 355 (variance-expr-join 356 (variance-expr-join 357 (variance-expr-compose 358 contravariant 359 irrelevant) 360 covariant) 361 (variance-expr-compose 362 covariant 363 'c)) 364 (variance-expr-compose 365 covariant 366 'd))) 367 (variance= 'c 368 (variance-expr-join 369 (variance-expr-compose 370 covariant 371 'a) 372 (variance-expr-compose 373 covariant 374 'b))) 375 (variance= 'd 376 (variance-expr-join 377 (variance-expr-compose 378 irrelevant 379 'a) 380 (variance-expr-compose 381 irrelevant 382 'd)))) 383 (hash)) 384 (hash 'a invariant 385 'b invariant 386 'c invariant 387 'd irrelevant)) 388 ) 389 )