5fbf4d30a8
5 Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
Andrew Kent
|
81b134cbb9 |
add refinement types, linear expr objs, and ineq props (#510)
This PR adds about half of the needed primitives and logic for reasoning about linear integer arithmetic in programs with interesting dependent types. Things have been added in a way s.t. programs will still continue to typecheck as they did, but if you want integer literals and certain operations (e.g. *,+,<,<=,=,>=,>) to include linear inequality information by default, you need to include the '#:with-linear-integer-arithmetic' keyword at the top of your module. The other features needed to get TR to be able to check things like verified vector operations will be to ajust function types so dependencies can exist between arguments and a minor tweak to get type inference to consider the symbolic objects of functions arguments. These features should be coming shortly in a future pull request. |
||
|
Andrew Kent
|
8e7f39025a |
remove interning for most Reps in TR
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. |
||
|
Andrew Kent
|
24c64e9de0 |
new representation scheme for typed racket internals
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) |
||
|
Andrew Kent
|
f9c5a534d0 |
filter -> prop
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 |
||
|
Vincent St-Amour
|
134f793ccc | Reduce directory nesting for tests. |