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

Add subtyping for types inside filters

Browse Source 
This makes a type like

  (-> Any Boolean : #:+ Integer)

a subtype of a type like

  (-> Any Boolean : #:+ Number)

For not filters, the direction is reversed.
This commit is contained in:
Asumu Takikawa 2015-04-01 18:50:46 -04:00
parent 889d96ca78
commit 8acc86bb9b
2 changed files with 13 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -142,6 +142,10 @@
[(f f) A0]
[((Bot:) t) A0]
[(s (Top:)) A0]
[((TypeFilter: t1 p) (TypeFilter: t2 p))
(subtype* A0 t1 t2)]
[((NotTypeFilter: t1 p) (NotTypeFilter: t2 p))
(subtype* A0 t2 t1)]
[(_ _) #f]))
(define (subtypes/varargs args dom rst)

9
typed-racket-test/unit-tests/subtype-tests.rkt
View File

@ -258,6 +258,15 @@
(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
(-> Univ -Boolean : (-FS (-filter -String 0) (-not-filter -String 0)))]
;; subtyping for types inside filters
[(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))
(-> Univ -Boolean : (-FS (-filter (-opt -Symbol) 0) (-not-filter -Symbol 0)))]
[(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter (-opt -Symbol) 0)))
(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
[FAIL
(-> Univ -Boolean : (-FS (-filter (-opt -Symbol) 0) (-not-filter (-opt -Symbol) 0)))
(-> Univ -Boolean : (-FS (-filter -Symbol 0) (-not-filter -Symbol 0)))]
[FAIL (make-ListDots (-box (make-F 'a)) 'a) (-lst (-box Univ))]
[(make-ListDots (-> -Symbol (make-F 'a)) 'a) (-lst (-> -Symbol Univ))]