These features are currently experimental and subject to change.
(define-typed-struct/exec forms ...)
(define-new-subtype name (constructor t))
This is purely a type-level distinction, with no way to distinguish the new type from the base type at runtime. Predicates made by make-predicate won’t be able distinguish them properly, so they will return true for all values that the base type’s predicate would return true for. This is usually not what you want, so you shouldn’t use make-predicate with these types.
Refinement types have been added to Typed Racket’s core, but Typed Racket does not yet have function types which allow dependencies between argument types, limiting how useful refinements are for now. Allowing argument dependencies is on our ‘to do’ list.
proposition = Top | Bot | (: symbolic-object type) | (! symbolic-object type) | (and proposition ...) | (or proposition ...) | (when proposition proposition) | (unless proposition proposition) | (if proposition proposition proposition) | (linear-comp symbolic-object symbolic-object) linear-comp = < | <= | = | >= | > symbolic-object = exact-integer | linear-term | (+ linear-term linear-term ...) linear-term = symbolic-path | (* exact-integer symbolic-path) symbolic-path = id | (path-elem symbolic-path) path-elem = car | cdr | vector-length
Note: The identifier in a refinement type is in scope inside the proposition, but not the type.
(: o t) used as a proposition holds when symbolic object o is of type t.
(! sym-obj type)
Typed Racket’s linear integer reasoning is turned off by default. If you want to activate it, you must add the #:with-linear-integer-arithmetic keyword when specifying the language of your program:
With this language option on, code such as the following will type check:
i.e. with linear integer reasoning enabled, Typed Racket detects that the comparison is guaranteed to produce #f, and thus the clearly ill-typed ‘then’-branch is ignored by the type checker since it is guaranteed to be dead code.