suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

fix intersect, make it (hopefully) commutative

Browse Source
This commit is contained in:
Andrew Kent 2016-10-25 10:41:05 -04:00
parent db1e7183aa
commit 9c33a54c6a
2 changed files with 122 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

159
typed-racket-lib/typed-racket/infer/intersect.rkt
View File

@ -10,73 +10,116 @@
(import infer^)
(export intersect^)
;; compute the intersection of two types
;; (note: previously called restrict)
;; (note: previously called restrict, however now restrict is
;; a non-additive intersection computation defined below
;; (i.e. only parts of t1 will remain, no parts from t2 are added))
(define (intersect t1 t2)
;; build-type: build a type while propogating bottom
(define (build-type constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
;; resolved is a set tracking previously seen intersect cases
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
;; subtyping performs a similar check for the same
;; reason
(let intersect
([t1 t1] [t2 t2] [resolved '()])
(match*/no-order
(t1 t2)
;; no overlap
[(_ _) #:when (disjoint-masks? (Type-mask t1) (Type-mask t2))
-Bottom]
;; already a subtype
[(t1 t2) #:no-order #:when (subtype t1 t2) t1]
;; polymorphic intersect
[(t1 (Poly: vars t))
#:no-order
#:when (infer vars null (list t1) (list t) #f)
t1]
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair
(intersect a1 a2 resolved)
(intersect d1 d2 resolved))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
;; (Struct: _ _ _ _ _ _))]
[((Syntax: t1*) (Syntax: t2*))
(build-type -Syntax (intersect t1* t2* resolved))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (intersect t1* t2* resolved))]
;; unions
[((Union: t1s) t2)
#:no-order
(apply Un (map (λ (t1) (intersect t1 t2 resolved)) t1s))]
(cond
;; we dispatch w/ Error first, because it behaves in
;; strange ways (e.g. it is ⊤ and ⊥ w.r.t subtyping) and
;; mucks up what might otherwise be commutative behavior
[(or (Error? t1) (Error? t2)) Err]
[else
(let intersect
([t1 t2] [t2 t1] [seen '()])
;; t1 : Type?
;; t2 : Type?
;; seen : (listof (cons/c (cons/c Type? Type?) symbol?))
;; A mapping tracking previously seen instances of potentially
;; recursive types in order to prevent infinite looping
;; and build a recursive type when appropriate. See the 'resolvable?'
;; cases below.
(define (rec t1 t2) (intersect t1 t2 seen))
(match* (t1 t2)
;; quick overlap check
[(_ _) #:when (disjoint-masks? (Type-mask t1) (Type-mask t2)) -Bottom]
;; already a subtype
[(t1 t2) #:when (subtype t1 t2) t1]
[(t1 t2) #:when (subtype t2 t1) t2]
;; intersections
[((Intersection: t1s) t2)
#:no-order
(apply -unsafe-intersect (for/list ([t1 (in-list t1s)])
(intersect t1 t2 resolved)))]
;; resolve resolvable types if we haven't already done so
[((? resolvable? t1) t2)
#:no-order
#:when (not (member (cons t1 t2) resolved))
(intersect (resolve t1) t2 (cons (cons t1 t2) resolved))]
;; polymorphic intersect
[(t1 (Poly: vars body))
#:when (infer vars null (list t1) (list body) #f)
t1]
[((Poly: vars body) t2)
#:when (infer vars null (list t2) (list body) #f)
t2]
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair (rec a1 a2) (rec d1 d2))]
;; FIXME: support structural updating for structs when structs are updated to
;; contain not only *if* they are polymorphic, but *which* fields are too
;;[((Struct: _ _ _ _ _ _)
;; (Struct: _ _ _ _ _ _))]
[((Syntax: t1*) (Syntax: t2*))
(build-type -Syntax (rec t1* t2*))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (rec t1* t2*))]
;; if we're intersecting two recursive types, intersect their body
;; and have their recursive references point back to the result
[((? Mu?) (? Mu?))
(define name (gensym))
(make-Mu name (intersect (Mu-body name t1) (Mu-body name t2) resolved))]
[((Union: t1s) t2)
(match t2
;; let's be consistent in slamming together unions
;; (i.e. if we don't do this dual traversal, the order the
;; unions are passed to 'intersect' can produces different
;; albeit equivalent (modulo subtyping, we hope) answers)
[(Union: t2s) (apply Un (for*/list ([t1 (in-list t1s)]
[t2 (in-list t2s)])
(rec t1 t2)))]
[_ (apply Un (map (λ (t1) (rec t1 t2)) t1s))])]
[(t1 (Union: t2s)) (apply Un (map (λ (t2) (rec t1 t2)) t2s))]
;; t2 and t1 have a complex relationship, so we build an intersection
;; (note: intersection checks for overlap)
[(t1 t2) (-unsafe-intersect t1 t2)])))
[((Intersection: t1s) t2)
(apply -unsafe-intersect (map (λ (t1) (rec t1 t2)) t1s))]
[(t1 (Intersection: t2s))
(apply -unsafe-intersect (map (λ (t2) (rec t1 t2)) t2s))]
;; For resolvable types, we record the occurrence and save a back pointer
;; in 'seen'. Then, if this pair of types emerges again, we know that we are
;; traversing an infinite type tree and instead we insert the back edge
;; and create a finite graph (i.e. a μ-type). If the back pointer is never used,
;; we don't create a μ-type, we just return the result
[(t1 t2)
#:when (or (resolvable? t1) (resolvable? t2))
(cond
[(assoc (cons t1 t2) seen)
;; we've seen these types before! -- use the stored symbol
;; as a back pointer with an 'F' type (i.e. a type variable)
=> (match-lambda
[(cons _ record)
;; record that we did indeed use the back
;; pointer by set!-ing the flag
(set-mcdr! record #t)
(make-F (mcar record))])]
[else
;; we've never seen these types together before! let's gensym a symbol
;; so that if we do encounter them again, we can create a μ type.
(define name (gensym 'rec))
;; the 'record' contains the back pointer symbol we may or may not use in
;; the car, and a flag for whether or not we actually used the back pointer
;; in the cdr.
(define record (mcons name #f))
(define t (intersect (resolve t1)
(resolve t2)
(list* (cons (cons t1 t2) record)
(cons (cons t2 t1) record)
seen)))
(cond
;; check if we used the backpointer, if so,
;; make a recursive type using that name
[(mcdr record) (make-Mu name t)]
;; otherwise just return the result
[else t])])]
;; t2 and t1 have a complex relationship, so we build an intersection
;; (note: intersection checks for overlap)
[(t1 t2) (-unsafe-intersect t1 t2)]))]))
;; restrict

21
typed-racket-test/succeed/intersect-no-intersections.rkt Normal file
View File

@ -0,0 +1,21 @@
#lang typed/racket/base
;; verify the casts in this file succeed
;; i.e. the calls to 'intersect' shouldn't not
;; generate intersection types
(define-type Json1 (Rec Json1 (U (Listof Json1) (HashTable Symbol Json1))))
(: scan1 (Json1 -> (Listof (HashTable Symbol Json1))))
(define (scan1 items-js)
(if (and (list? items-js) (andmap hash? items-js))
(cast items-js (Listof (HashTable Symbol Json1)))
(list)))
(define-type Json2 (Rec Json2 (U Null (Pairof Json2 (Listof Json2)) (HashTable Symbol Json2))))
(: scan2 (Json2 -> (Listof (HashTable Symbol Json2))))
(define (scan2 items-js)
(if (and (list? items-js) (andmap hash? items-js))
(cast items-js (Listof (HashTable Symbol Json2)))
(list)))