14 Experimental Features

These features are currently experimental and subject to change.

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.

14.1 Logical Refinements and Linear Integer Reasoning

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.

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.

Propositions can also describe linear inequalities (e.g. (<= x 42) holds when x is less than or equal to 42), using any of the following relations: <=, <, =, >=, >.

The following logical combinators hold as one would expect depending on which of their subcomponents hold hold: and, or, if, not.

(when p q) is equivalent to (or (not p) (and p q)).

(unless p q) is equivalent to (or p q).

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:

#lang typed/racket #:with-refinements

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:

(if (< 5 4)

(+ "Luke," "I am your father")

"that's impossible!")

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.

14.2 Dependent Function Types

Typed Racket supports explicitly dependent function types:

syntax (-> ([id : opt-deps arg-type] ...)     opt-pre     range-type     opt-props)

opt-deps   =       |   (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!"

> (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₀

(vector-length x₀)))

Given:    (Refine (z₀ : One) (= 1 z₀))

in: 1

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!"

> (safe-ref2 (vector "not safe!") 1)

eval:14:0: Type Checker: could not apply function;

unable to prove

precondition: (<= 2 (vector-length a))

in: 1

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.