Refinement Types in Typed Racket
posted by Andrew Kent
With the Racket v6.11 release, Typed Racket has begun to support basic refinement and dependent function types. This post gives an overview for working with these types while writing some simple vector operations.
Currently these types are documented under Typed Racket’s experimental features. They are experimental in the sense that they are relatively new. We look forward to improving their usefulness by incorporating user feedback.
Note: If you wish to experiment with refinement and/or dependent function types in the near future, you should use a snapshot build, as it will have additional features and bug fixes from user feedback. Some of the examples in this post will require a build from early November 2017 or later.
Refinement Types
Let us examine the type of vectorref
in Typed Racket:
It states that the index (the second argument) must be an Integer
, i.e. any wholenumber value in the exclusive range (∞ , ∞). This description, however, is somewhat coarse: we obviously cannot use any integer. To avoid a runtime error when indexing into a vector v
, we must use an integer in the range [0, (vectorlength
v)
). With a refinement type we can precisely describe this subset of the integers:
This refinement type describes values i
of type Integer
such that (<= 0 i ( (vectorlength v) 1))
produces #true
. The documentation for Refine describes precisely what propositions can be used in refinements. Today it includes logical statements about the types of terms, standard logical combinators (e.g. and, or), and linear integer constraints.
Dependent function types
By combining refinement types with dependent function types (i.e. functions whose domain and range may depend on argument and/or program values), we can now give a more precise function type for many basic vector operations, e.g.:
Here we have stated that safevectorref
’s second argument (n
) depends on its first argument (v
) and that the type of n
is an Integer
which is a valid index for v
.
If we try and use safevectorref
with a vector and index which Typed Racket cannot prove satisfy the respective types:
(safevectorref (vector 0 1) 2)
Typed Racket will report an error while type checking:
Type Checker: type mismatch
expected: (Refine
(i : Integer)
(and (<= i ( (vectorlength v) 1)) (<= 0 v)))
given: (Refine (z : PositiveByte) (= 2 z)) in: 2
Preconditions
Sometimes the refinements used in a dependent function type can also be written conveniently as a “precondition”, e.g.:
This function type is equivalent to the previous version, but the refining proposition that requires that n
be a valid index for v
now references n
directly and has been written after the list of arguments:
#:pre (v n) (<= 0 n ( (vectorlength v) 1))
We can read the precondition specification above as follows: the precondition for the function depends on arguments v
and n
and it requires that Typed Racket can prove (<= 0 n ( (vectorlength v)
1))
in order for a call to be welltyped.
Typed Racket may be able to provide more detailed feedback when the arguments are of the correct type but the precondition cannot be proved:
Type Checker: could not apply function;
unable to prove precondition
precondition: (<= 2 ( (vectorlength v) 1))
in: (safevectorref (vector 0 1) 2)
Here, Typed Racket first performed type inference and confirmed that the arguments (vector 0 1)
and 2
had acceptable types before discovering the precondition was unprovable at the call site.
We believe the error messages produced when using preconditions may be more informative in general. Your mileage may vary.
Programming with refinement types
Note: the below examples will work on Racket v6.11 with one additional snippet of code or on any Racket build more recent than November 11 2017.
When programming with refinement types, use the #:withrefinements
option on the #lang
line to tell Typed Racket to track additional logical information about program terms:
;; safevectorops.rkt #lang typed/racket/base #:withrefinements
In particular, this will tell Typed Racket to remember that the vector produced by (makevector n ...)
has length n
, which will be essential for typing our vector operations.
Now we can also declare more detailed types for vectorset!
and vectorref
since these more specific types are subtypes of their more permissive standard types. If we’re feeling adventurous, we may use the unsafe
variants from racket/unsafe/ops
that do not check their bounds, since Typed Racket proves they are never used with invalid indices:
(require (onlyin racket/unsafe/ops unsafevectorref unsafevectorset!)) (: safevectorref (All (A) (> ([v : (Vectorof A)] [n : Natural]) #:pre (v n) (< n (vectorlength v)) A))) (define safevectorref unsafevectorref) (: safevectorset! (All (A) (> ([v : (Vectorof A)] [n : Natural] [a : A]) #:pre (v n) (< n (vectorlength v)) Void))) (define safevectorset! unsafevectorset!)
Now that we have these foundational operations in place (i.e. makevector
, safevectorref
, and safevectorset!
) , let’s see if we can define some of the vector operations that are provided by racket/base
and racket/vector
, but with more precise types!
buildvector
Let’s look at the documentation for buildvector
:
(buildvector n proc) → vector?
n : exactnonnegativeinteger?
proc : (exactnonnegativeinteger? . > . any/c)
Creates a vector of n elements by applying proc to the
integers from 0 to (sub1 n) in order. If vec is the
resulting vector, then (vectorref vec i) is the value
produced by (proc i).
Example:
> (buildvector 5 add1)
'#(1 2 3 4 5)
First let’s consider its type signature. It seems like there are two places where we could use refinement types to create a more precise typebased specification:

the
proc
procedure will always be given an integer in the range [0,n
), and 
the length of the returned vector is equal to
n
.
We can encode both of these directly in the type of buildvector
:
With the type signature in place, we can proceed to define the function:
There are a few things to note about the definition:
a. In order to make a (Vectorof A)
, we need some value of type A
to initialize the vector with (i.e. the second arg to makevector
). Because of this, we first check if n
is greater than 0. If it is greater than 0, we can compute (proc 0)
and use that to initialize the vector we create, otherwise we simply return (vector)
(i.e. an empty vector) which is “vacuously” a vector of A
for any A
.
b. The recursive loop we use to populate indices 1 through (sub1 n)
, which we named loop!
, requires a type annotation Natural
on its argument i
so that its being greater than or equal to 0 is known in the body of the recursive function. That, combined with the test (< i
n)
, allows us to successfully use safevectorset!
to update the contents at i
. (Note: if Typed Racket had smarter type inference, this annotation may not be necessary.)
vectormap
vectormap
takes a vector vec
and a function proc
and produces a new vector vec*
where (vectorref vec* i)
equals (proc
(vectorref vec i))
for each valid index i
:
> (vectormap add1 (vector 0 1 2 3)) '#(1 2 3 4)
Because we now have a version of buildvector
that uses refinement types to more precisely describe its specification (see previous section), we can implement vectormap
entirely in terms of buildvector
:
(: vectormap (All (A B) (> ([proc : (> A B)] [vec : (Vectorof A)]) (Refine [v : (Vectorof B)] (= (vectorlength vec) (vectorlength v)))))) (define (vectormap proc vec) (buildvector (vectorlength vec) (λ ([i : (Refine [i : Natural] (< i (vectorlength vec)))]) (proc (safevectorref vec i)))))
Now vectormap
’s type indicates that the length of the returned vector is equal to the length of the vector it received as input.
vectorcopy
vectorcopy
takes a vector vec
and copies its elements in the range [start
,end
) into a fresh vector:
> (vectorcopy (vector 0 1 2 3) 1 3) '#(1 2)
To precisely type this function, we will use a precondition to assert the range specified by start
and end
is some sensible (although possibly empty) portion of the input vector vec
. A Refine
allows us to indicate that the length of the returned vector will always be ( end start)
:
(: vectorcopy (All (A) (> ([vec : (Vectorof A)] [start : Natural] [end : Natural]) #:pre (vec start end) (<= start end (vectorlength vec)) (Refine [res : (Vectorof A)] (= ( end start) (vectorlength res)))))) (define (vectorcopy vec start end) (define len ( end start)) (cond [(= 0 len) (vector)] [else (define res (makevector len (safevectorref vec start))) (let loop! ([i : Natural 0]) (when (< i len) (define a (safevectorref vec (+ start i))) (safevectorset! res i a) (loop! (+ 1 i)))) res]))
vectorcopy!
vectorcopy!
is similar, but instead of returning a fresh vector, the elements in the specified range are copied from a source vector s
into a destination vector d
:
Here the precondition is larger because it includes constraints that must hold with respect to both vectors s
and d
, i.e. the range in the source s
[sstart
,send
) must be a valid, and the destination vector d
must have a corresponding valid range [dstart
,(+ dstart ( send sstart))
):
(: vectorcopy! (All (A) (> ([d : (Vectorof A)] [dstart : Natural] [s : (Vectorof A)] [sstart : Natural] [send : Natural]) #:pre (d dstart s sstart send) (and (<= sstart send (vectorlength s)) (<= dstart (vectorlength d)) (<= ( send sstart) ( (vectorlength d) dstart))) Void))) (define (vectorcopy! d dstart s sstart send) (define count ( send sstart)) (let loop! ([i : Natural 0]) (when (< i count) (define a (safevectorref s (+ sstart i))) (safevectorset! d (+ dstart i) a) (loop! (+ 1 i)))))
quicksort
Finally, here is a version of quicksort that has been typed using dependent function types to sort vectors of reals:
(: quicksort! (> (Vectorof Real) Void)) (define (quicksort! A) (quicksorthelper! A 0 ( (vectorlength A) 1))) (: quicksorthelper! (> ([A : (Vectorof Real)] [lo : Natural] [hi : Integer]) #:pre (A lo hi) (and (<= lo (vectorlength A)) (< hi (vectorlength A))) Void)) (define (quicksorthelper! A lo hi) (when (< lo hi) (define pivot (partition! A lo hi)) (quicksorthelper! A lo ( pivot 1)) (quicksorthelper! A (+ pivot 1) hi))) (: swap! (> ([A : (Vectorof Real)] [i : Natural] [j : Natural]) #:pre (A i j) (and (< i (vectorlength A)) (< j (vectorlength A))) Void)) (define (swap! A i j) (define tmp (safevectorref A i)) (safevectorset! A i (safevectorref A j)) (safevectorset! A j tmp)) (: partition! (> ([A : (Vectorof Real)] [lo : Natural] [hi : Natural]) #:pre (A lo hi) (< lo hi (vectorlength A)) (Refine [pivot : Natural] (<= lo pivot hi)))) (define (partition! A lo hi) (define pivot (safevectorref A lo)) (let outerloop! ([i : (Refine [n : Natural] (< lo n)) (+ 1 lo)] [j : (Refine [n : Natural] (and (<= n hi) (<= lo n))) hi]) (let iloop! ([i : (Refine [n : Natural] (< lo n)) i]) (cond [(and (<= i j) (< (safevectorref A i) pivot)) (iloop! (+ i 1))] [else (let jloop! ([j : (Refine [n : Natural] (and (<= n hi) (<= lo n))) j]) (cond [(and (>= (safevectorref A j) pivot) (>= j i)) (jloop! ( j 1))] [(> i j) (swap! A lo j) j] [else (swap! A i j) (outerloop! i j)]))]))))
Typed/Untyped interaction
Typed Racket will generate dependent function contracts (e.g. >i contracts) to protect dependent functions when they are used in untyped modules:
As always, care should be taken when designing APIs that involve contract boundaries which may be frequently crossed by performance sensitive code since each boundary crossing will involve runtime checks for the respective types.
Final Notes
Linear integer arithmetic
Typed Racket today only reasons about linear integer constraints, i.e. arithmetic constraints expressible with <=
, and
, and or
over linear combinations of select program terms. If the specification you wish to encode in types requires nonlinear arithmetic, Typed Racket will not be able to verify those constraints.
Dependent function type limitations
Dependent function types currently only support mandatory positional arguments. In the future we plan to add optional, rest, and keyword argument support.
Currently functions with dependencies between arguments and/or preconditions cannot be used within a case>
form.
There is not yet support for dependent struct types.
Type checking the above examples in Racket v6.11
To type check the examples in this post on Racket v6.11, the following snippet must be added to the module:
(require typed/racket/unsafe) (unsaferequire/typed/provide typed/racket/base [makevector (All (A) (> ([n : Natural] [val : A]) (Refine [v : (Vectorof A)] (= n (vectorlength v)))))])
This axiomatizes a more specific type for makevector
. Any snapshot builds of Racket from November 10 2017 or later will not require this snippet.
Bugs
If you have found a bug or have an idea for how these features might be more useful, feel free to open an issue on Typed Racket’s github repo.