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

Add a predicate field to base types, which makes checking for

Browse Source 
subtyping of value types easier.

However, this means that base types can't be marshaled as before,
since these predicates can't be marshaled. Instead, we now marshal
base types as identifiers that refer to their base type object.

original commit: e56663c943fe4ae355b6d626d3c84b6ec8ea7fd1
This commit is contained in:
Vincent St-Amour 2011-01-06 17:57:11 -05:00
parent 881a3d31e7
commit 3d6b5893ba
11 changed files with 150 additions and 86 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/tests/typed-scheme/unit-tests/subtype-tests.rkt
View File

@ -112,12 +112,12 @@
[(-values (list -Number)) (-values (list Univ))]
[(-poly (b) ((Un (make-Base 'foo #'dummy)
[(-poly (b) ((Un (make-Base 'foo #'dummy values #'values)
(-struct 'bar #f
(list (make-fld -Number #'values #f) (make-fld b #'values #f))
#'values))
. -> . (-lst b)))
((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values))
((Un (make-Base 'foo #'dummy values #'values) (-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values))
. -> . (-lst (-pair -Number (-v a))))]
[(-poly (b) ((-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f)) #'values) . -> . (-lst b)))
((-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values) . -> . (-lst (-pair -Number (-v a))))]

2
collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt
View File

@ -7,7 +7,7 @@
(provide type-equal-tests)
(define (-base x) (make-Base x #'dummy))
(define (-base x) (make-Base x #'dummy values #'values))
(define-syntax (te-tests stx)

2
collects/typed-scheme/env/init-envs.rkt vendored
View File

@ -23,7 +23,7 @@
(string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
(match v
[(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))]
[(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))]
[(Base: n cnt pred marshaled) marshaled]
[(Name: stx) `(make-Name (quote-syntax ,stx))]
[(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)]
[(Struct: name parent flds proc poly? pred-id cert maker-id)

6
collects/typed-scheme/infer/infer-unit.rkt
View File

@ -368,11 +368,11 @@
(cg t t*)))]
[((Vector: t) (Sequence: (list t*)))
(cg t t*)]
[((Base: 'String _) (Sequence: (list t*)))
[((Base: 'String _ _ _) (Sequence: (list t*)))
(cg -Char t*)]
[((Base: 'Bytes _) (Sequence: (list t*)))
[((Base: 'Bytes _ _ _) (Sequence: (list t*)))
(cg -Nat t*)]
[((Base: 'Input-Port _) (Sequence: (list t*)))
[((Base: 'Input-Port _ _ _) (Sequence: (list t*)))
(cg -Nat t*)]
[((Vector: t) (Sequence: (list t*)))
(cg t t*)]

4
collects/typed-scheme/private/type-contract.rkt
View File

@ -172,7 +172,7 @@
(inexact-real? (real-part x))))))]
[(== t:-Number type-equal?) #'(flat-named-contract 'Number number?)]
[(Base: sym cnt) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))]
[(Base: sym cnt _ _) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))]
[(Refinement: par p? cert)
#`(and/c #,(t->c par) (flat-contract #,(cert p?)))]
[(Union: elems)
@ -257,7 +257,7 @@
(maker fld-cnts ...))))])
rec))]
[else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
[(Syntax: (Base: 'Symbol _)) #'identifier?]
[(Syntax: (Base: 'Symbol _ _ _)) #'identifier?]
[(Syntax: t) #`(syntax/c #,(t->c t))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
[(Param: in out) #`(parameter/c #,(t->c out))]

9
collects/typed-scheme/rep/type-rep.rkt
View File

@ -131,7 +131,14 @@
[#:key 'channel])
;; name is a Symbol (not a Name)
(dt Base ([name symbol?] [contract syntax?])
;; contract is used when generating contracts from types
;; predicate is used to check (at compile-time) whether a value belongs
;; to that base type. This is used to check for subtyping between value
;; types and base types.
;; marshaled has to be a syntax object that refers to the base type
;; being created. this allows us to avoid reconstructing the base type
;; when using it from its marshaled representation
(dt Base ([name symbol?] [contract syntax?] [predicate procedure?] [marshaled syntax?])
[#:frees #f] [#:fold-rhs #:base] [#:intern name]
[#:key (case name
[(Number Integer) 'number]

67
collects/typed-scheme/types/abbrev.rkt
View File

@ -11,7 +11,9 @@
(except-in racket/contract ->* ->)
(prefix-in c: racket/contract)
(for-syntax racket/base syntax/parse)
(for-template racket/base racket/contract racket/promise racket/tcp racket/flonum))
(for-template racket/base racket/contract racket/promise racket/tcp racket/flonum)
;; for base type predicates
racket/promise racket/tcp racket/flonum)
(provide (all-defined-out)
(rename-out [make-Listof -lst]
@ -106,32 +108,45 @@
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
(define -Boolean (make-Base 'Boolean #'boolean?))
(define -Symbol (make-Base 'Symbol #'symbol?))
(define -Void (make-Base 'Void #'void?))
(define -Undefined (make-Base 'Undefined #'(lambda (x) (equal? (letrec ([y y]) y) x)))) ; initial value of letrec bindings
(define -Bytes (make-Base 'Bytes #'bytes?))
(define -Regexp (make-Base 'Regexp #'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))))
(define -PRegexp (make-Base 'PRegexp #'(and/c pregexp? (not/c byte-pregexp?))))
(define -Byte-Regexp (make-Base 'Byte-Regexp #'(and/c byte-regexp? (not/c byte-pregexp?))))
(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp?))
(define -String (make-Base 'String #'string?))
(define -Keyword (make-Base 'Keyword #'keyword?))
(define -Char (make-Base 'Char #'char?))
(define -Thread (make-Base 'Thread #'thread?))
(define -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path?))
(define -Module-Path (make-Base 'Module-Path #'module-path?))
(define -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index?))
(define -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression?))
(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag?))
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set?))
(define -Path (make-Base 'Path #'path?))
(define -Namespace (make-Base 'Namespace #'namespace?))
(define -Output-Port (make-Base 'Output-Port #'output-port?))
(define -Input-Port (make-Base 'Input-Port #'input-port?))
(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener?))
(define -Boolean (make-Base 'Boolean #'boolean? boolean? #'-Boolean))
(define -Symbol (make-Base 'Symbol #'symbol? symbol? #'-Symbol))
(define -Void (make-Base 'Void #'void? void? #'-Void))
(define -Undefined
(make-Base 'Undefined
#'(lambda (x) (equal? (letrec ([y y]) y) x)) ; initial value of letrec bindings
(lambda (x) (equal? (letrec ([y y]) y) x))
#'-Undefined))
(define -Bytes (make-Base 'Bytes #'bytes? bytes? #'-Bytes))
(define -Regexp (make-Base 'Regexp
#'(and/c regexp? (not/c pregexp?) (not/c byte-regexp?))
(conjoin regexp? (negate pregexp?) (negate byte-regexp?))
#'-Regexp))
(define -PRegexp (make-Base 'PRegexp
#'(and/c pregexp? (not/c byte-pregexp?))
(conjoin pregexp? (negate byte-pregexp?))
#'-PRegexp))
(define -Byte-Regexp (make-Base 'Byte-Regexp
#'(and/c byte-regexp? (not/c byte-pregexp?))
(conjoin byte-regexp? (negate byte-pregexp?))
#'-Byte-Regexp))
(define -Byte-PRegexp (make-Base 'Byte-PRegexp #'byte-pregexp? byte-pregexp? #'-Byte-PRegexp))
(define -String (make-Base 'String #'string? string? #'-String))
(define -Keyword (make-Base 'Keyword #'keyword? keyword? #'-Keyword))
(define -Char (make-Base 'Char #'char? char? #'-Char))
(define -Thread (make-Base 'Thread #'thread? thread? #'-Thread))
(define -Resolved-Module-Path (make-Base 'Resolved-Module-Path #'resolved-module-path? resolved-module-path? #'-Resolved-Module-Path))
(define -Module-Path (make-Base 'Module-Path #'module-path? module-path? #'-Module-Path))
(define -Module-Path-Index (make-Base 'Module-Path-Index #'module-path-index? module-path-index? #'-Module-Path-Index))
(define -Compiled-Module-Expression (make-Base 'Compiled-Module-Expression #'compiled-module-expression? compiled-module-expression? #'-Compiled-Module-Expression))
(define -Prompt-Tag (make-Base 'Prompt-Tag #'continuation-prompt-tag? continuation-prompt-tag? #'-Prompt-Tag))
(define -Cont-Mark-Set (make-Base 'Continuation-Mark-Set #'continuation-mark-set? continuation-mark-set? #'-Cont-Mark-Set))
(define -Path (make-Base 'Path #'path? path? #'-Path))
(define -Namespace (make-Base 'Namespace #'namespace? namespace? #'-Namespace))
(define -Output-Port (make-Base 'Output-Port #'output-port? output-port? #'-Output-Port))
(define -Input-Port (make-Base 'Input-Port #'input-port? input-port? #'-Input-Port))
(define -TCP-Listener (make-Base 'TCP-Listener #'tcp-listener? tcp-listener? #'-TCP-Listener))
(define -FlVector (make-Base 'FlVector #'flvector?))
(define -FlVector (make-Base 'FlVector #'flvector? flvector? #'-FlVector))
(define -Syntax make-Syntax)
(define -HT make-Hashtable)

100
collects/typed-scheme/types/numeric-tower.rkt
View File

@ -4,6 +4,7 @@
(require (types abbrev numeric-predicates)
(rep type-rep)
unstable/function
(for-template racket/base racket/contract racket/flonum (types numeric-predicates)))
(provide (all-defined-out))
@ -36,33 +37,47 @@
;; Integers
(define -Byte>1 (make-Base 'Byte-Larger-Than-One ; unsigned
#'(and/c byte? (lambda (x) (> x 1)))))
#'(and/c byte? (lambda (x) (> x 1)))
(conjoin byte? (lambda (x) (> x 1)))
#'-Byte>1))
(define -PosByte (*Un -One -Byte>1))
(define -Byte (*Un -Zero -PosByte))
(define -PosIndexNotByte
(make-Base 'Positive-Index-Not-Byte
#'(and/c index? positive? (not/c byte?))))
;; index? will be checked at runtime, can be platform-specific
;; portable-index? will be checked at compile-time, must be portable
#'(and/c index? positive? (not/c byte?))
(conjoin portable-index? positive? (negate byte?))
#'-PosIndexNotByte))
(define -PosIndex (*Un -One -Byte>1 -PosIndexNotByte))
(define -Index (*Un -Zero -PosIndex))
(define -PosFixnumNotIndex
(make-Base 'Positive-Fixnum-Not-Index
#'(and/c fixnum? positive? (not/c index?))))
#'(and/c fixnum? positive? (not/c index?))
(conjoin portable-fixnum? positive? (negate portable-index?))
#'-PosFixnumNotIndex))
(define -PosFixnum (*Un -PosFixnumNotIndex -PosIndex))
(define -NonNegFixnum (*Un -PosFixnum -Zero))
(define -NegFixnum
(make-Base 'Negative-Fixnum-Not-Index
#'(and/c fixnum? negative?)))
#'(and/c fixnum? negative?)
(conjoin portable-fixnum? negative?)
#'-NegFixnum))
(define -NonPosFixnum (*Un -NegFixnum -Zero))
(define -Fixnum (*Un -NegFixnum -Zero -PosFixnum))
(define -PosIntNotFixnum
(make-Base 'Positive-Integer-Not-Fixnum
#'(and/c exact-integer? positive? (not/c fixnum?))))
#'(and/c exact-integer? positive? (not/c fixnum?))
(conjoin exact-integer? positive? (negate portable-fixnum?))
#'-PosIntNotFixnum))
(define -PosInt (*Un -PosIntNotFixnum -PosFixnum))
(define -NonNegInt (*Un -PosInt -Zero))
(define -Nat -NonNegInt)
(define -NegIntNotFixnum
(make-Base 'Negative-Integer-Not-Fixnum
#'(and/c exact-integer? negative? (not/c fixnum?))))
#'(and/c exact-integer? negative? (not/c fixnum?))
(conjoin exact-integer? negative? (negate portable-fixnum?))
#'-NegIntNotFixnum))
(define -NegInt (*Un -NegIntNotFixnum -NegFixnum))
(define -NonPosInt (*Un -NegInt -Zero))
(define -Int (*Un -NegInt -Zero -PosInt))
@ -70,31 +85,45 @@
;; Rationals
(define -PosRatNotInt
(make-Base 'Positive-Rational-Not-Integer
#'(and/c exact-rational? positive? (not/c integer?))))
#'(and/c exact-rational? positive? (not/c integer?))
(conjoin exact-rational? positive? (negate integer?))
#'-PosRatNotInt))
(define -PosRat (*Un -PosRatNotInt -PosInt))
(define -NonNegRat (*Un -PosRat -Zero))
(define -NegRatNotInt
(make-Base 'Negative-Rational-Not-Integer
#'(and/c exact-rational? negative? (not/c integer?))))
#'(and/c exact-rational? negative? (not/c integer?))
(conjoin exact-rational? negative? (negate integer?))
#'-NegRatNotInt))
(define -NegRat (*Un -NegRatNotInt -NegInt))
(define -NonPosRat (*Un -NegRat -Zero))
(define -Rat (*Un -NegRat -Zero -PosRat))
;; Floating-point numbers
(define -FlonumPosZero (make-Base 'Float-Positive-Zero
#'(lambda (x) (eq? x 0.0))))
#'(lambda (x) (eq? x 0.0))
(lambda (x) (eq? x 0.0))
#'-FlonumPosZero))
(define -FlonumNegZero (make-Base 'Float-Negative-Zero
#'(lambda (x) (eq? x -0.0))))
#'(lambda (x) (eq? x -0.0))
(lambda (x) (eq? x -0.0))
#'-FlonumNegZero))
(define -FlonumZero (*Un -FlonumPosZero -FlonumNegZero))
(define -FlonumNan (make-Base 'Float-Nan
#'(and/c flonum? (lambda (x) (eqv? x +nan.0)))))
#'(and/c flonum? (lambda (x) (eqv? x +nan.0)))
(conjoin flonum? (lambda (x) (eqv? x +nan.0)))
#'-FlonumNan))
(define -PosFlonum
(make-Base 'Positive-Float
#'(and/c flonum? positive?)))
#'(and/c flonum? positive?)
(conjoin flonum? positive?)
#'-PosFlonum))
(define -NonNegFlonum (*Un -PosFlonum -FlonumPosZero))
(define -NegFlonum
(make-Base 'Negative-Float
#'(and/c flonum? negative?)))
#'(and/c flonum? negative?)
(conjoin flonum? negative?)
#'-NegFlonum))
(define -NonPosFlonum (*Un -NegFlonum -FlonumNegZero))
(define -Flonum (*Un -NegFlonum -FlonumNegZero -FlonumPosZero -PosFlonum -FlonumNan)) ; 64-bit floats
;; inexact reals can be flonums (64-bit floats) or 32-bit floats
@ -103,27 +132,37 @@
;; eqv? equates 0.0f0 with itself, but not eq?
;; we also need to check for small-float? since eqv? also equates
;; 0.0f0 and 0.0e0
#'(and/c small-float? (lambda (x) (eqv? x 0.0f0)))))
#'(and/c small-float? (lambda (x) (eqv? x 0.0f0)))
(lambda (x) #f) ; can't assign that type at compile-time. see tc-lit for more explanation
#'-SmallFloatPosZero))
(define -SmallFloatNegZero
(make-Base 'Small-Float-Negative-Zero
#'(and/c small-float? (lambda (x) (eqv? x -0.0f0)))))
#'(and/c small-float? (lambda (x) (eqv? x -0.0f0)))
(lambda (x) #f)
#'-SmallFloatNegZero))
(define -SmallFloatZero (*Un -SmallFloatPosZero -SmallFloatNegZero))
(define -SmallFloatNan (make-Base 'Small-Float-Nan
#'(and/c small-float?
;; eqv? equates single and double precision nans
(lambda (x) (eqv? x +nan.0)))))
(lambda (x) (eqv? x +nan.0)))
(lambda (x) #f)
#'-SmallFloatNan))
(define -InexactRealPosZero (*Un -SmallFloatPosZero -FlonumPosZero))
(define -InexactRealNegZero (*Un -SmallFloatNegZero -FlonumNegZero))
(define -InexactRealZero (*Un -InexactRealPosZero -InexactRealNegZero))
(define -PosSmallFloat
(make-Base 'Positive-Small-Float
#'(and/c small-float? positive?)))
#'(and/c small-float? positive?)
(lambda (x) #f)
#'-PosSmallFloat))
(define -PosInexactReal (*Un -PosSmallFloat -PosFlonum))
(define -NonNegSmallFloat (*Un -PosSmallFloat -SmallFloatPosZero))
(define -NonNegInexactReal (*Un -PosInexactReal -InexactRealPosZero))
(define -NegSmallFloat
(make-Base 'Negative-Small-Float
#'(and/c small-float? negative?)))
#'(and/c small-float? negative?)
(lambda (x) #f)
#'-NegSmallFloat))
(define -NegInexactReal (*Un -NegSmallFloat -NegFlonum))
(define -NonPosSmallFloat (*Un -NegSmallFloat -SmallFloatNegZero))
(define -NonPosInexactReal (*Un -NegInexactReal -InexactRealNegZero))
@ -156,17 +195,32 @@
#'(and/c number?
(lambda (x)
(and (flonum? (imag-part x))
(flonum? (real-part x)))))))
(flonum? (real-part x)))))
(conjoin number?
(lambda (x)
(and (flonum? (imag-part x))
(flonum? (real-part x)))))
#'-FloatComplex))
(define -SmallFloatComplex (make-Base 'Small-Float-Complex
#'(and/c number?
(lambda (x)
(and (small-float? (imag-part x))
(small-float? (real-part x)))))))
(small-float? (real-part x)))))
(conjoin number?
(lambda (x)
(and (small-float? (imag-part x))
(small-float? (real-part x)))))
#'-SmallFloatComplex))
(define -InexactComplex (*Un -FloatComplex -SmallFloatComplex))
(define -ExactComplexNotReal
(make-Base 'Complex-Not-Real #'(and/c number?
(not/c real?)
(lambda (x) (exact? (imag-part x))))))
(make-Base 'Complex-Not-Real
#'(and/c number?
(not/c real?)
(lambda (x) (exact? (imag-part x))))
(conjoin number?
(negate real?)
(lambda (x) (exact? (imag-part x))))
#'-ExactComplexNotReal))
(define -Complex (*Un -Real -InexactComplex -ExactComplexNotReal))
(define -Number -Complex)

10
collects/typed-scheme/types/printer.rkt
View File

@ -143,7 +143,7 @@
[else (fp "~a" v)])]
[(? tuple? t)
(fp "~a" (cons 'List (tuple-elems t)))]
[(Base: n cnt) (fp "~s" n)]
[(Base: n cnt _ _) (fp "~s" n)]
[(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))]
[(Struct: (== promise-sym) #f (list (fld: t _ _)) _ _ _ _ _) (fp "(Promise ~a)" t)]
[(Struct: nm par (list (fld: t _ _) ...) proc _ _ _ _)
@ -196,10 +196,10 @@
#;
[(Mu-unsafe: b) (fp "(unsafe-mu ~a ~a)" (Type-seq c) b)]
[(Mu: x (Syntax: (Union: (list
(Base: 'Number _)
(Base: 'Boolean _)
(Base: 'Symbol _)
(Base: 'String _)
(Base: 'Number _ _ _)
(Base: 'Boolean _ _ _)
(Base: 'Symbol _ _ _)
(Base: 'String _ _ _)
(Mu: var (Union: (list (Value: '()) (Pair: (F: x) (F: var)))))
(Mu: y (Union: (list (F: x) (Pair: (F: x) (F: y)))))
(Vector: (F: x))

10
collects/typed-scheme/types/remove-intersect.rkt
View File

@ -38,16 +38,16 @@
(ormap (lambda (t*) (overlap t t*)) e)]
[(or (list _ (? Poly?)) (list (? Poly?) _))
#t] ;; these can have overlap, conservatively
[(list (Base: s1 _) (Base: s2 _)) (or (subtype t1 t2) (subtype t2 t1))]
[(list (Base: _ _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _ _)) (subtype t1 t2)] ;; conservative
[(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))]
[(list (Base: _ _ _ _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _ _ _ _)) (subtype t1 t2)] ;; conservative
[(list (Syntax: t) (Syntax: t*))
(overlap t t*)]
[(or (list (Syntax: _) _)
(list _ (Syntax: _)))
#f]
[(list (Base: _ _) _) #f]
[(list _ (Base: _ _)) #f]
[(list (Base: _ _ _ _) _) #f]
[(list _ (Base: _ _ _ _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t]
[(list (Pair: _ _) (Value: (? pair? v))) #t]
[(list (Pair: a b) (Pair: a* b*))

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

@ -233,19 +233,7 @@
;; value types
[((Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))]
;; values are subtypes of their "type"
[((Value: (? exact-integer? n)) (Base: 'Integer _)) A0]
[((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0]
[((Value: (? exact-nonnegative-integer? n)) (== -Nat =t)) A0]
[((Value: (? exact-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0]
[((Value: (? flonum? n)) (Base: 'Flonum _)) A0]
[((Value: (? real? n)) (== -Real =t)) A0]
[((Value: (? number? n)) (Base: 'Number _)) A0]
[((Value: (? keyword?)) (Base: 'Keyword _)) A0]
[((Value: (? char?)) (Base: 'Char _)) A0]
[((Value: (? boolean? n)) (Base: 'Boolean _)) A0]
[((Value: (? symbol? n)) (Base: 'Symbol _)) A0]
[((Value: (? string? n)) (Base: 'String _)) A0]
[((Value: v) (Base: _ _ pred _)) (if (pred v) A0 (fail! s t))]
;; tvars are equal if they are the same variable
[((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; sequences are covariant
@ -259,11 +247,11 @@
(subtypes* A0 ts (map (λ _ t*) ts))]
[((Vector: t) (Sequence: (list t*)))
(subtype* A0 t t*)]
[((Base: 'String _) (Sequence: (list t*)))
[((Base: 'String _ _ _) (Sequence: (list t*)))
(subtype* A0 -Char t*)]
[((Base: 'Bytes _) (Sequence: (list t*)))
[((Base: 'Bytes _ _ _) (Sequence: (list t*)))
(subtype* A0 -Nat t*)]
[((Base: 'Input-Port _) (Sequence: (list t*)))
[((Base: 'Input-Port _ _ _) (Sequence: (list t*)))
(subtype* A0 -Nat t*)]
[((Hashtable: k v) (Sequence: (list k* v*)))
(subtypes* A0 (list k v) (list k* v*))]
@ -384,4 +372,4 @@
;(subtype (make-poly '(a) (make-tvar 'a)) (make-lst N))
;;problem:
;; (subtype (make-Mu 'x (make-Syntax (make-Union (list (make-Base 'Number #'number?) (make-F 'x))))) (make-Syntax (make-Univ)))
;; (subtype (make-Mu 'x (make-Syntax (make-Union (list (make-Base 'Number #'number? number? #'-Number) (make-F 'x))))) (make-Syntax (make-Univ)))