Correctly restrict the struct predicate's filter type when
a parent struct is mutable but the child is not and they both
have polymorphic type variables.
See the discussion in GH issue #205
since 'restrict' will now create intersections when there is
a complex relationship between the two types, calling it
'intersect' makes a lot more sense.
Adds intersection types as a better way to handle the the case
when restrict cannot structurally intersect two types (e.g. when
you learn within a polymorphic function a variable x of type A
is also an Integer, but we dont know how A relates to Integer).
This allows for non-lossy refinements of type info while typechecking.
This pull request is largely a renaming effort to clean up the TR codebase. There are two primary things I wanted to change:
1. Replace all occurrences of "filter" with "prop" or "proposition"
- The word "filter" is a meaningless opaque term at this point in the Typed Racket implementation. If anything, it just adds confusion to why things are the way the are. We should use "proposition" instead, since that's what they actually are.
2. Avoid using "Top" and "Bottom" in both the type and proposition realm.
- Currently the top type is called Univ and the bottom type is called bottom, while the top proposition is called Top and the bottom proposition is called Bot. This is just unnecessarily confusing, doesn't really line up w/ the user-space names, and doesn't line up with the names we use in TR formalisms. Worse, all of the top types of primitive types---e.g. the type of all structs, StructTop--- use Top, so it is really easy to get confused about what name to use for these sorts of things.
With these issues in mind, I made the following changes to names:
Top -> TrueProp
Bot -> FalseProp
TypeFilter -> TypeProp
NotTypeFilter -> NotTypeProp
AndFilter -> AndProp
OrFilter -> OrProp
-filter t o -> -is-type o t
-not-filter t o -> -not-type o t
FilterSet -> PropSet
NoFilter -> #f
NoObject -> #f
-FS -> -PS
-top -> -tt
-bot -> -ff
implied-atomic? q p -> implies-atomic? p q
filter-rec-id -> prop-rec-id
-no-filter -> -no-propset
-top-filter -> -tt-propset
-bot-filter -> -ff-propset
-true-filter -> -true-propset
-false-filter -> -false-propset
PredicateFilter: -> PredicateProp:
add-unconditional-filter-all-args add-unconditional-prop-all-args
* Fix type of syntax->list
to return `(U False (Listof (Syntaxof Any)))` if it can't prove that the input is a syntax-list.
Fixes https://github.com/racket/typed-racket/issues/347
This makes the type `syntax->list` consistent with the type `stx->list` already has.
* Add tests for syntax->list
This makes the tooltip show the more refined function
type after application typechecking. For example, case->
types will be narrowed to the particular case that fits.
Polymorphic function types will be instantiated at the
appropriate type.
Fixes issue #325
This is used for functions with a single argument imported with
`require/typed`, and avoids unneccessary checks. This produces a
3x speedup on the following benchmark:
#lang racket/base
(module m racket/base
(provide f)
(define (f x) x))
(module n typed/racket/base
(require/typed
(submod ".." m)
[f (-> Integer Integer)])
(time
(for ([x (in-range 1000000)])
(f 1) (f 2) (f 3) (f 4))))
(require 'n)
on top of the previous improvment from using `unsafe-procedure-chaperone`
and `procedure-result-arity`.
This allows the types generated by the struct form, as well as #:struct
clauses of require/typed, to be specified explicitly using a #:type-name
option. This allows the name of a struct and the type it is assigned to
be different.
Closes#261
