improve subtyping

Author: pnwamk

typed-racket-lib/typed-racket/rep/object-rep.rkt

@@ -37,6 +37,7 @@
          obj-seq-next
          scale-obj
          uninterpreted-PE?
+         intersect-objects
          (rename-out [make-LExp* make-LExp]
                      [make-LExp raw-make-LExp])
          (all-from-out "fme-utils.rkt"))
@@ -395,4 +396,12 @@
 (define (add-path-to-lexp p l)
   (match l
     [(LExp: const terms)
-     (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
+     (make-LExp* const (terms-set terms p (add1 (terms-ref terms p))))]))
+
+
+(define (intersect-objects o1 o2)
+  (match* (o1 o2)
+    [(o o) o]
+    [((Empty:) _) o2]
+    [(_ (Empty:)) o1]
+    [(_ _) o1]))

typed-racket-lib/typed-racket/types/subtype.rkt

@@ -21,7 +21,7 @@
                     one-of/c))
 
 (lazy-require
- ("../infer/infer.rkt" (infer))
+ ("../infer/infer.rkt" (infer intersect))
  ("prop-ops.rkt" (-and))
  ("../typecheck/tc-subst.rkt" (instantiate-obj+simplify))
  ("../typecheck/tc-envops.rkt" (env+ implies-in-env?)))
@@ -186,7 +186,7 @@
 ;; NOTE: This function takes into account that domains are
 ;; contravariant w.r.t. subtyping, i.e. callers should NOT
 ;; flip argument order.
-(define/cond-contract (Arrow-domain-subtypes* A dom1 rst1 dom2 rst2 [objs #f])
+(define/cond-contract (positional-domain-subtypes* A dom1 rst1 dom2 rst2 [objs #f])
   (->* (list?
         (listof Type?)
         (or/c #f Rest? RestDots?)
@@ -198,12 +198,26 @@
     [((cons t1 ts1) (cons t2 ts2))
      (subtype-seq A
                   (subtype* t2 t1 (and objs (car objs)))
-                  (Arrow-domain-subtypes* ts1 rst1 ts2 rst2 (and objs (cdr objs))))]
+                  (positional-domain-subtypes* ts1 rst1 ts2 rst2 (and objs (cdr objs))))]
     [(_ _)
      (subtype* A
                (-Tuple* dom2 (Rest->Type rst2))
                (-Tuple* dom1 (Rest->Type rst1)))]))
 
+(define/cond-contract (Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2 [objs #f])
+  (->* (list?
+        (listof Type?)
+        (or/c #f Rest? RestDots?)
+        (listof Keyword?)
+        (listof Type?)
+        (or/c #f Rest? RestDots?)
+        (listof Keyword?))
+       ((listof Object?))
+       (or/c #f list?))
+  (subtype-seq A
+               (positional-domain-subtypes* dom1 rst1 dom2 rst2 objs)
+               (kw-subtypes* kws1 kws2)))
+
 (define-syntax-rule (with-fresh-ids len ids . body)
   (let-values ([(ids seq) (for/fold ([ids '()]
                                      [seq (temp-ids)])
@@ -220,7 +234,7 @@
     [((Arrow: dom1 rst1 kws1 raw-rng1)
       (Arrow: dom2 rst2 kws2 raw-rng2))
      (define A* (subtype-seq A
-                             (Arrow-domain-subtypes* dom1 rst1 dom2 rst2)
+                             (positional-domain-subtypes* dom1 rst1 dom2 rst2)
                              (kw-subtypes* kws1 kws2)))
      (cond
        [(not A*) #f]
@@ -254,7 +268,7 @@
                       (instantiate-obj d ids)))
        (define A* (subtype-seq A
                                (kw-subtypes* kws1 '())
-                               (Arrow-domain-subtypes* dom1 rst1 dom2 #f (map -id-path ids))))
+                               (positional-domain-subtypes* dom1 rst1 dom2 #f (map -id-path ids))))
        (cond
          [(not A*) #f]
          [else
@@ -310,7 +324,7 @@
   (define rst (match raw-rst
                 [(? Type?) (make-Rest (list raw-rst))]
                 [_ raw-rst]))
-  (Arrow-domain-subtypes* A dom rst argtys #f))
+  (positional-domain-subtypes* A dom rst argtys #f))
 
 
 ;;************************************************************
@@ -812,11 +826,35 @@
      [((Fun: arrows2) _)
       (cond
         [(null? arrows1) #f]
-        [else (for/fold ([A A])
-                        ([a2 (in-list arrows2)]
-                         #:break (not A))
-                (for/or ([a1 (in-list arrows1)])
-                  (arrow-subtype* A a1 a2)))])]
+        [else
+         (for/fold ([A A])
+                   ([a2 (in-list arrows2)]
+                    #:break (not A))
+           (match-define (Arrow: dom2 rst2 kws2 raw-cdom2) a2)
+           ;; A <: C₁ ∩ ... ∩ Cₙ
+           ;; D₁ ∩ ... ∩ Dₙ <: B
+           ;; ------------------------
+           ;; (C₁→D₁∩...∩Cₙ→Dₙ) <: A→B
+           (define raw-cdom1
+             (for/fold ([cdom #f])
+                       ([a1 (in-list arrows1)])
+               (match-define (Arrow: dom1 rst1 kws1 raw-cdom1) a1)
+               (cond
+                 [(Arrow-domain-subtypes* A dom1 rst1 kws1 dom2 rst2 kws2)
+                  (if cdom (intersect-values cdom raw-cdom1) raw-cdom1)]
+                 [else cdom])))
+           (cond
+             [(not raw-cdom1) #f]
+             [else
+              (with-fresh-ids (length dom2) ids
+                (define mapping
+                  (for/list ([idx (in-naturals)]
+                             [id (in-list ids)]
+                             [t (in-list dom2)])
+                    (list* idx id t)))
+                (subval* A
+                         (instantiate-obj+simplify raw-cdom1 mapping)
+                         (instantiate-obj raw-cdom2 ids)))]))])]
      [((? DepFun? dfun) _)
       (for/or ([a1 (in-list arrows1)])
         (arrow-subtype-dfun* A a1 dfun))]
@@ -1229,3 +1267,32 @@
      #false]
     [_ (continue<: A t1 t2 obj)])]
   [else: (continue<: A t1 t2 obj)])
+
+
+;; intersects two monomorphic Values (i.e. see rep/values-rep)
+;; if the values are strictly incompatible, we return ⊥,
+(define (intersect-values v1 v2)
+  (match* (v1 v2)
+    [(v v) v]
+    [((ValuesDots: rs1 dty1 dbound)
+      (ValuesDots: rs2 dty2 dbound))
+     (make-ValuesDots (map intersect-results rs1 rs2) (intersect dty1 dty2) dbound)]
+    [((? ValuesDots?) _) v1]
+    [(_ (? ValuesDots?)) v2]
+    [((AnyValues: p1) (AnyValues: p2)) (make-AnyValues (-and p1 p2))]
+    [((AnyValues: p) (Values: (cons (Result: t (PropSet: p+ p-) o) rst)))
+     (make-Values (cons (make-Result t (-PS (-and p p+) (-and p p-)) o) rst))]
+    [((Values: (cons (Result: t (PropSet: p+ p-) o) rst)) (AnyValues: p))
+     (make-Values (cons (make-Result t (-PS (-and p p+) (-and p p-)) o) rst))]
+    [((Values: rs1) (Values: rs2))
+     (cond
+       [(= (length rs1) (length rs2))
+        (make-Values (map intersect-results rs1 rs2))]
+       [else (make-AnyValues -ff)])]))
+
+;; intersects two Results (i.e. see rep/core-rep.rkt) pointwise
+(define (intersect-results r1 r2)
+  (match* (r1 r2)
+    [((Result: t1 (PropSet: p1+ p1-) o1)
+      (Result: t2 (PropSet: p2+ p2-) o2))
+     (make-Result (intersect t1 t2) (-PS (-and p1+ p2+) (-and p1- p2-)) (intersect-objects o1 o2))]))