Previously expected propositions were erased frequently
(at lets and ifs) and checking for logical entailment
was unidirectional instead of bidirectional. In other words,
instead of checking if propositions held at the leaves
of the AST, we would typecheck the AST and blindly propagate
up ALL logical info we learned at each step. This meant that
we would get exponential blow up of propositions even when
we didn't care about their content.
With this commit, instead now we send down expected types
*and* propositions so we can verify expected types and
propisitions are satisfied at leaves, thereby relieving the
need to constantly report up huge amounts of logical info
while typechecking.
Moving to eager propagating of bottom works for most cases,
but in some cases flattening types such as (Pairof Bottom Any)
to Bottom made things like type inference break for some cases
(since (Listof Nothing) == Null, and (Listof A) did not structurally
like up like it used to). Perhaps w/ a little more effort
inference and any other potential issues could work better
with propagating bottom, but for now we'll be slightly less
aggressive about it.
i.e. this fixes pfds, which commit 8e7f390 broke.
Prior to this change (which was Typed Racket PR 469) all internal TR
objects (Reps) were interned and kept around for the entire duration
of type checking. Because of this, frequent operations that rebuilt
types were particularly costly (e.g. various forms of
substitution). To recoup some of this cost, caching was being used in
a lot of places. This PR sought to remove interning as the default
behavior for Reps and allow for more flexibility in how we approach
time/space performance needs going forward.
The following changes were included in this overhaul:
Interning: All Reps are no longer interned. Right now we only intern
unions and some propositions.
Rep generic operations: we now use racket/generic so we're not
reinventing this wheel.
Singletons: Reps (e.g. TrueProp, Univ, etc) can be declared singleton,
which creates a single instance of the rep that all visible operations
(even within the declaring module) are defined in terms of
(e.g. predicates are defined as (λ (x) (eq? x singleton-instance)),
etc).
Custom constructors: Custom constructors can be specified for Reps,
which allows for simple normalization, interning, or other invariants
to be enfored whenever a Rep is created.
Union: Unions used to try to ensure no obviously overlaping types
would inhabit the same Union (e.g. (U String (Pairof Any Any) (Pairof
Int Int)) would be simplified to (U String (Pairof Any Any))). This,
however, required frequent calls to subtyping every time a Union was
modified and working with Unions thus had a high cost (another thing
that caching was used to reduce). Instead of this, Unions now enforce
a much simpler set of invariants on their members: (1) No duplicates
(by virtue of using a hash-based set), (2) Any and Nothing do not
appear in unions, and (3) Nested unions are flattened. Also, using a
hashset as the internal data structure meant that we could easily
intern unions w.r.t. equal? equality. NOTE: we do reduce unions to not
contain obviously overlapping terms when printing to users and when
generating contracts (so obviously and avoidable inneficient contracts
are not generated – See union.rkt for 'normalize-type').
Subtyping changes: Subtyping has been designed to reduce dispatch time
w/ a switch since we no longer cache _all_ subtyping calls (we only
cache subtyping results for unions since they have some costly
subtyping).
prop-ops changes: AndProps now are careful to sort OrProps by length
before building the resulting proposition. This is done because
OrProp implication only checks if one Or is a subset of another Or.
By ordering Or props by size, we only ever check if an OrProp implies
another if its size is <= the other OrProp. This also makes the
smart constructor '-and' more robust, since the order the props
appear does not affect if some Ors are kept or not.
Testing: More subtype tests have been added (we are still probably
relying too much on typecheck-tests.rkt and not the more granular unit
tests in general). Also, typecheck-tests.rkt has been changed to
check for type-equivalence (i.e. subtyping in both directions)
instead of equal? equivalence.
This commit cleans up some helper functions that have been
pretty awful for a while. The code is (hopefully) more readable
and it does less work (i.e. unneeded substitutions are no longer
performed).
The previous fix relied on finding and manipulating all dead code.
But we missed some; in particular code of the form:
(begin (error 'x) ...dead...)
So switch to a different strategy that tolerates untraversed
dead code.
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)
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.
* 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
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.
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
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.
`typed-racket-test/main` is now the file to run for almost everything.
`typed-racket-test/run` continues to exist so that DrDr preserves the
timing history.
Integration tests now print a progress meter, which should fix the
Travis timeouts.
See also commit 5cd5f77 “Don't allow promises created with `delay/name` as `(Promise T)`.”.
The contracts in `typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt` should be just a single identifier, not a lambda expression, because `typed-racket-lib/typed-racket/private/type-contract.rkt` relies on that, and passes the contract name to free-identifier=?, which won't work on a lambda.
