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

Subtyping between (List T ... a) and (Listof T[Any/a])

Browse Source 
original commit: fd5a662ccc7aa2fbc3f29974c075dcabf2a870fe
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-28 11:53:54 -04:00
parent 4f2a113076
commit 92c48f6521
2 changed files with 11 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
collects/tests/typed-scheme/succeed/list-dots.rkt
View File

@ -7,3 +7,12 @@
(define (g . x) x)
(g 7 7 7)
(: h (All (a ...) (a ... -> (Listof Any))))
(define (h . x) x)
(: h2 (All (a ...) ((Pair String a) ... -> (Listof (Pair String Any)))))
(define (h2 . x) x)
(: h3 (All (a ...) ((Pair String a) ... -> (Listof Any))))
(define (h3 . x) x)

2
collects/typed-scheme/types/subtype.rkt
View File

@ -298,6 +298,8 @@
;; recur structurally on dotted lists, assuming same bounds
[((ListDots: s-dty dbound) (ListDots: t-dty dbound))
(subtype* A0 s-dty t-dty)]
[((ListDots: s-dty dbound) (Listof: t-elem))
(subtype* A0 (substitute Univ dbound s-dty) t-elem)]
;; quantification over two types preserves subtyping
[((Poly: ns b1) (Poly: ms b2))
(=> unmatch)