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.
Typed Racket allows types to be ‘refined’ or ‘constrained’ by logical propositions. These propositions can mention certain program terms, allowing a program’s types to depend on the values of terms.
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 | symbolic-path | (+ symbolic-object ...) | (- symbolic-object ...) | (* exact-integer symbolic-object) 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)
In addition to reasoning about propositions regarding types (i.e. something is or is not of some particular type), Typed Racket is equipped with a linear integer arithmetic solver that can prove linear constraints when necessary. To turn on this solver (and some other refinement reasoning), you must add the #:with-refinements keyword when specifying the language of your program:
With this language option on, type checking the following primitives will produce more specific logical info (when they are being applied to 2 or 3 arguments): *, +, -, <, <=, =, >=, >, and make-vector.
This allows code such as the following to type check:
i.e. with refinement 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.
Typed Racket supports explicitly dependent function types:
| (id ...) opt-pre =
| #:pre (id ...) prop opt-props =
| opt-pos-prop opt-neg-prop opt-obj opt-pos-prop =
| #:+ prop opt-neg-prop =
| #:- prop opt-obj =
| #:object obj
The syntax is similar to Racket’s dependent contracts syntax (i.e. ->i).
Each function argument has a name, an optional list of identifiers it depends on, an argument type. An argument’s type can mention (i.e. depend on) other arguments by name if they appear in its list of dependencies. Dependencies cannot be cyclic.
A function may have also have a precondition. The precondition is introduced with the #:pre keyword followed by the list of arguments on which it depends and the proposition which describes the precondition.
A function’s range may depend on any of its arguments.
The grammar of supported propositions and symbolic objects (i.e. prop and obj) is the same as the proposition and symbolic-object grammars from Refine’s syntax.
For example, here is a dependently typed version of Racket’s vector-ref which eliminates vector bounds errors during type checking instead of at run time:
> (require racket/unsafe/ops)
> (: safe-ref1 (All (A) (-> ([v : (Vectorof A)] [n : (v) (Refine [i : Natural] (< i (vector-length v)))]) A))) > (define (safe-ref1 v n) (unsafe-vector-ref v n)) > (safe-ref1 (vector "safe!") 0)
- : String
> (safe-ref1 (vector "not safe!") 1)
eval:10:0: Type Checker: Polymorphic function `safe-ref1'
could not be applied to arguments:
Argument x₀ (position 1):
Expected: (Vectorof A)
Given: (Mutable-Vector String)
Argument y₀ (position 2):
Expected: (Refine (z₀ : Nonnegative-Integer) (< z₀
Given: (Refine (z₀ : One) (= 1 z₀))
Here is an equivalent type that uses a precondition instead of a refinement type:
> (: safe-ref2 (All (A) (-> ([v : (Vectorof A)] [n : Natural]) #:pre (v n) (< n (vector-length v)) A))) > (define (safe-ref2 v n) (unsafe-vector-ref v n)) > (safe-ref2 (vector "safe!") 0)
- : String
> (safe-ref2 (vector "not safe!") 1)
eval:14:0: Type Checker: could not apply function;
unable to prove
precondition: (<= 2 (vector-length a))
Using preconditions can provide more detailed type checker error messages, i.e. they can indicate when the arguments were of the correct type but the precondition could not be proven.