This is a major to some of the internal representation of things
within Typed Racket (mostly affecting structs that inherited from Rep
(see rep/rep-utils.rkt)), and lots of tweaks and bug fixes that
happened along the way.
This PR includes the following major changes:
A new rep-utils implementation, which uses struct properties for the
generic operations and properties of the various Reps (see
rep-utils.rkt)
More specific Rep inheritance (i.e. arr no longer inherits from Type,
because it is not a Type, etc ...) (see type-rep.rkt, core-rep.rkt,
values-rep.rkt), and thus things like Type/c no longer exist
New Rep's to classify the things that are no longer Type or Prop,
(such as PropSets, SomeValues, Results, etc -- see core-rep.rkt and
values-rep.rkt)
uses of type-case now replaced by uses of Rep-fold and Rep-walk
structural types can specify their fields' variance and operations
like subtyping and free-vars can generically operate over these types
(see type-rep.rkt)
type-mask replaces types key -- types masks are described in detail in
(rep/type-mask.rkt)
Types can specify a predicate to recognize their "top type" via [#:top
pred])
There is an explicit 'Bottom' type now (i.e. neither union or
intersection are used)
subtyping re-organized, slight tweaking to inference
various environments got for-each functions in addition to the map
functions they had (e.g. type-name-env.rkt)
Empty is no longer an Object? -- the OptObject? predicate checks for
either Object or Empty, and so it is easier to be clear about where
Empty makes sense appearing and where it does not
Previously signatures were created with promises in their fields, now
we create a promise around each signature (this way the contracts for
Signature fields are cleaner)
Names for structs now use the args field to describe how many type
arguments they take (Note: this could use further tidying for sure!)
simplified the propositional logic code in several places, got rid of
escape continuations, etc (see prop-ops.rkt, tc-envops.rkt,
tc-metafunctions.rkt)
we now use subsumption more to simplify type results from type
checking, e.g. if the type does not overlap w/ false, it's false
proposition is FalseProp, etc (see tc-expr-unit.rkt and prop-ops.rkt,
the function is called reduce-tc-results/subsumption)
updating along a path will now intersect with the expected structural
type if it is not encountered (e.g. updating Any with (Int @ car) now
produces (Pairof Int Any) instead of Any -- see update.rkt)
lots of tests were tweaked to match up w/ the new prop subsumption
that occurs
remove was renamed subtract (so as to not conflict w/ racket/base's
remove)
a restrict function was added, which acts like intersect but is never
additive (i.e. it will never create an intersection if it can't figure
out how the two types relate -- see intersect.rkt)
tc-subst was modified to substitute out all the variables leaving
scope at once (and I simplified/tweaked some of the logic in there a
little, see tc-subst.rkt)
Type checking function applications now propagates information learned
why type checking the arguments, (e.g. (begin (f (assert x boolean?))
...)) ; the remainder of the begin is aware that x is a boolean)
* call compute-constraints instead of sc->constraints in get-max-contract-kind
* test cast on an intersection type involving Rec
* remove memory limit on sandboxed-unsafe-ops test
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
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.
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.
In the case that a let rhs doesn't return and therefore the
bodies of the let are unreachable, the bodies need to be marked
as ignored for the optimizer.
In addition, don't attempt unboxed let optimization at all
if the return type is Nothing since it probably means some
body expressions have no type.
Closes GH issue #165
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
Because -let-internal wasn't rename-out'd, users would see its name in
syntax error messages. Adding #:context forces the error messages to be
phrased in terms of the given form.
Since these promises re-evaluate their bodies every time they
are forced, allowing them makes `force` not idempotent and not
safe to treat as a path.
This change is slightly backwards-incompatible, since programs
that previously passed `delay/name` promises across the typed
boundary will now fail at runtime. The alternative is also
incompatible: stop treating `force` as a path. Since `delay/name`
is quite obscure, this approach seems like the safer choice.
This enables contract generation in the negative
direction (untyped->typed) for row polymorphic types
(basically mixin types).
Depends on `class-seal` and `class-unseal` in
the racket/class library.