Before this, row instantiation was done with an ad-hoc
and undocumented syntax. Adding a new form works better
because rows should not be parsed as types.
This fills the corresponding entries in the cast table with a Dead-Code
type so that when the contract-generation pass calls the contract-def
thunk, it finds that in the table.
Avoids using mzlib/pconvert in favor of a few big match
clauses. This lets us cut out a package dependency and
makes the code easier to understand.
This commit also removes the use of mzlib/pconvert
in the debug printer in favor of just using the type
serialization performed in init-envs.rkt.
In addition, a few optimizations for type serialization
were implemented that cut a few percent off of zo sizes.
Note that this commit regresses for zo sizes for modules
that heavily use GUI classes, but that is fixed in a
future commit.
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
Guard opaque predicates with an (-> Any Any) contract. This uses the
contract generation infrastructure to avoid wrapping struct predicates.
Also, relax `any-wrap/c` (the contract used for `Any` in positive
position) to allow opaque structures. This also requires an enumeration
of all the other kinds of values that TR understands, so that they are
not confused with opaque structures.
Joint work with @bennn.
Closes#202.
Closes#203.
Closes#241.
When a typing error is located inside macro-expanded code, a message such as “wrong number of arguments to polymorphic type: expected 1 and got 2” does not help much in locating which instantiation is wrong.
This case only comes up when something else unfortunate has happened
with type printing, but the current implementation can lead to paths
in the type printing.
Most unit forms are supported, including most of the "infer" forms that
infer imports/exports/linkages from the current context.
Notably, none of the structural linking forms for units are supported, and
`define-unit-binding` is also currently unsupported.
The old check was broken for cases with type constructors
with more than one type argument and was also too conservative
in some cases (e.g., when one cycle refers to another cycle of
aliases in a non-recursive manner).
The new check is still conservative, but it allows more types
than before.
Closes GH issue #157
This makes a type like
(-> Any Boolean : #:+ Integer)
a subtype of a type like
(-> Any Boolean : #:+ Number)
For not filters, the direction is reversed.
