be less eager about bottom propogation

Moving to eager propagating of bottom works for most cases,
but in some cases flattening types such as (Pairof Bottom Any)
to Bottom made things like type inference break for some cases
(since (Listof Nothing) == Null, and (Listof A) did not structurally
like up like it used to). Perhaps w/ a little more effort
inference and any other potential issues could work better
with propagating bottom, but for now we'll be slightly less
aggressive about it.

i.e. this fixes pfds, which commit 8e7f390 broke.
This commit is contained in:
Andrew Kent 2016-12-19 08:28:49 -05:00
parent 708e0782fa
commit da30fb6f74
7 changed files with 62 additions and 107 deletions

View File

@ -51,15 +51,15 @@
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(-pair (rec a1 a2) (rec d1 d2))]
(rebuild -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*))
(-Syntax (rec t1* t2*))]
(rebuild -Syntax (rec t1* t2*))]
[((Promise: t1*) (Promise: t2*))
(-Promise (rec t1* t2*))]
(rebuild -Promise (rec t1* t2*))]
[((Union: t1s) t2)
(match t2
@ -130,9 +130,6 @@
;; and sometimes we want to make sure and _not_ add t2 to the result
;; we just want to keep the parts of t1 consistent with t2)
(define (restrict 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 restrict cases
;; (i.e. pairs of t1 t2) to prevent infinite unfolding.
;; subtyping performs a similar check for the same
@ -150,17 +147,17 @@
;; structural recursion on types
[((Pair: a1 d1) (Pair: a2 d2))
(build-type -pair
(restrict a1 a2 resolved)
(restrict d1 d2 resolved))]
(rebuild -pair
(restrict a1 a2 resolved)
(restrict 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 (restrict t1* t2* resolved))]
(rebuild -Syntax (restrict t1* t2* resolved))]
[((Promise: t1*) (Promise: t2*))
(build-type -Promise (restrict t1* t2* resolved))]
(rebuild -Promise (restrict t1* t2* resolved))]
;; unions
[((Union: t1s) t2)

View File

@ -199,11 +199,7 @@
;; left and right are Types
(def-structural Pair ([left #:covariant]
[right #:covariant])
[#:mask mask:pair]
[#:custom-constructor
(if (or (Bottom? left) (Bottom? right))
-Bottom
(make-Pair left right))])
[#:mask mask:pair])
;;----------------
;; Mutable Pairs
@ -216,11 +212,7 @@
;; *mutable* pairs - distinct from regular pairs
;; left and right are Types
(def-structural MPair ([left #:invariant] [right #:invariant])
[#:mask mask:mpair]
[#:custom-constructor
(if (or (Bottom? left) (Bottom? right))
-Bottom
(make-MPair left right))])
[#:mask mask:mpair])
;;----------
;; Vectors
@ -242,11 +234,7 @@
[#:singleton -BoxTop])
(def-structural Box ([elem #:invariant])
[#:mask mask:box]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-Box elem))])
[#:mask mask:box])
;;----------
;; Channel
@ -257,11 +245,7 @@
[#:singleton -ChannelTop])
(def-structural Channel ([elem #:invariant])
[#:mask mask:channel]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-Channel elem))])
[#:mask mask:channel])
;;----------------
;; Async-Channel
@ -272,11 +256,7 @@
[#:singleton -Async-ChannelTop])
(def-structural Async-Channel ([elem #:invariant])
[#:mask mask:channel]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-Async-Channel elem))])
[#:mask mask:channel])
;;-------------
;; ThreadCell
@ -287,33 +267,21 @@
[#:singleton -ThreadCellTop])
(def-structural ThreadCell ([elem #:invariant])
[#:mask mask:thread-cell]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-ThreadCell elem))])
[#:mask mask:thread-cell])
;;----------
;; Promise
;;----------
(def-structural Promise ([elem #:covariant])
[#:mask mask:promise]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-Promise elem))])
[#:mask mask:promise])
;;------------
;; Ephemeron
;;------------
(def-structural Ephemeron ([elem #:covariant])
[#:mask mask:ephemeron]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-Ephemeron elem))])
[#:mask mask:ephemeron])
;;-----------
@ -325,11 +293,7 @@
[#:singleton -Weak-BoxTop])
(def-structural Weak-Box ([elem #:invariant])
[#:mask mask:other-box]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-Weak-Box elem))])
[#:mask mask:other-box])
;;---------------
@ -337,11 +301,7 @@
;;---------------
(def-structural CustodianBox ([elem #:covariant])
[#:mask mask:other-box]
[#:custom-constructor
(if (Bottom? elem)
-Bottom
(make-CustodianBox elem))])
[#:mask mask:other-box])
;;------
;; Set
@ -385,22 +345,14 @@
;; t is the type of the result of syntax-e, not the result of syntax->datum
(def-structural Syntax ([t #:covariant])
[#:mask mask:syntax]
[#:custom-constructor
(if (Bottom? t)
-Bottom
(make-Syntax t))])
[#:mask mask:syntax])
;;---------
;; Future
;;---------
(def-structural Future ([t #:covariant])
[#:mask mask:future]
[#:custom-constructor
(if (Bottom? t)
-Bottom
(make-Future t))])
[#:mask mask:future])
;;---------------
@ -417,11 +369,7 @@
;; and the codomains of `handler`
(def-structural Prompt-Tagof ([body #:invariant]
[handler #:invariant])
[#:mask mask:prompt-tag]
[#:custom-constructor
(if (or (Bottom? body) (Bottom? handler))
-Bottom
(make-Prompt-Tagof body handler))])
[#:mask mask:prompt-tag])
;;--------------------------
;; Continuation-Mark-Keyof
@ -460,11 +408,7 @@
[#:frees (f) (make-invariant (combine-frees (map f elems)))]
[#:fmap (f) (make-HeterogeneousVector (map f elems))]
[#:for-each (f) (for-each f elems)]
[#:mask mask:vector]
[#:custom-constructor
(if (ormap Bottom? elems)
-Bottom
(make-HeterogeneousVector elems))])
[#:mask mask:vector])
;; * * * * * * *
@ -617,14 +561,12 @@
;; This should eventually be based on understanding of struct properties.
[#:mask (mask-union mask:struct mask:procedure)]
[#:custom-constructor
(cond
[(ormap (λ (fld) (Bottom? (fld-t fld))) flds) -Bottom]
[else (make-Struct (normalize-id name)
parent
flds
proc
poly?
(normalize-id pred-id))])])
(make-Struct (normalize-id name)
parent
flds
proc
poly?
(normalize-id pred-id))])
;; Represents prefab structs
;; key : prefab key encoding mutability, auto-fields, etc.
@ -634,11 +576,7 @@
[#:frees (f) (combine-frees (map f flds))]
[#:fmap (f) (make-Prefab key (map f flds))]
[#:for-each (f) (for-each f flds)]
[#:mask mask:prefab]
[#:custom-constructor
(cond
[(ormap Bottom? flds) -Bottom]
[else (make-Prefab key flds)])])
[#:mask mask:prefab])
(def-type StructTypeTop ()
[#:mask mask:struct-type]
@ -772,10 +710,7 @@
[#:fmap (f) (make-Refinement (f parent) pred)]
[#:for-each (f) (f parent)]
[#:mask (λ (t) (mask (Refinement-parent t)))]
[#:custom-constructor
(if (Bottom? parent)
-Bottom
(make-Refinement parent (normalize-id pred)))])
[#:custom-constructor (make-Refinement parent (normalize-id pred))])
;; A Row used in type instantiation
;; For now, this should not appear in user code. It's used

View File

@ -22,6 +22,16 @@
(rename-out [make-Listof -lst]
[make-MListof -mlst]))
(define-syntax (rebuild stx)
(syntax-case stx ()
[(_ mk args ...)
(with-syntax ([(t ...) (generate-temporaries #'(args ...))])
(syntax/loc stx
(let ([t args] ...)
(if (or (Bottom? t) ...)
-Bottom
(mk t ...)))))]))
(define/decl -False (make-Value #f))
(define/decl -True (make-Value #t))
(define/decl -Boolean (Un -False -True))

View File

@ -23,9 +23,6 @@
;; in *syntactic order* (e.g. (car (cdr x)) -> '(car cdr))
(define/cond-contract (update t new-t pos? path-elems)
(Type? Type? boolean? (listof PathElem?) . -> . Type?)
;; build-type: build a type while propogating bottom
(define (build constructor . args)
(if (memf Bottom? args) -Bottom (apply constructor args)))
;; update's inner recursive loop
;; puts path in *accessed* order
;; (i.e. (car (cdr x)) --> (list cdr car))
@ -38,15 +35,15 @@
(match* ((resolve t) path-elem)
;; pair ops
[((Pair: t s) (CarPE:))
(build -pair (update t rst) s)]
(rebuild -pair (update t rst) s)]
[((Pair: t s) (CdrPE:))
(build -pair t (update s rst))]
(rebuild -pair t (update s rst))]
;; syntax ops
[((Syntax: t) (SyntaxPE:))
(build -Syntax (update t rst))]
(rebuild -Syntax (update t rst))]
;; promise op
[((Promise: t) (ForcePE:))
(build -Promise (update t rst))]
(rebuild -Promise (update t rst))]
;; struct ops
[((Struct: nm par flds proc poly pred)

View File

@ -1,5 +1,5 @@
#;
(exn-pred #rx"expected: \\Null.*given: \\(Listof Pos\\*\\)")
(exn-pred #rx"expected: \\(Listof Nothing\\).*given: \\(Listof Pos\\*\\)")
#lang typed/racket
(define-type Pos Integer)
(define-new-subtype Pos* (p Pos))

View File

@ -1,5 +1,5 @@
#;
(exn-pred #rx"expected: \\Null.*given: \\(Listof Pos\\*\\)")
(exn-pred #rx"expected: \\(Listof Nothing\\).*given: \\(Listof Pos\\*\\)")
#lang typed/racket
(define-type Pos Integer)
(define-new-subtype Pos* (p Pos))

View File

@ -0,0 +1,16 @@
#lang typed/racket
(define-type (Promiseof A) (Boxof (U ( (Listof A)) (Listof A))))
(struct: (A) Queue ([fld : (Promiseof A)]))
(define-syntax-rule (empty A)
((inst Queue A) (box (lambda: () '()))))
(: empty? : (All (A) ((Queue A) -> Boolean)))
(define (empty? q)
(null? (Queue-fld q)))
;; make sure that inference works on nested 'Nothing' types
(empty? (empty Nothing))