Racket 6.11 brings refinement types and dependent function types to its Typed Racket variant.
Refinement types are types associated to a predicate which is assumed to hold for any element of that type. The general syntax to express a refinement type is (Refine [v : t] p), which describes the type of all values v of type t that satisfy the predicate p.
A basic example of a refinement type is the following function type that guarantees that its return value is at least as big as each of its inputs:
(-> ([x : Integer] [y : Integer]) (Refine [z : Integer] (and (>= z x) (>= z y))))
In Racket, refinement predicates can refer to program terms, thus making the refined type depend on the values of those terms. For example, you could define the following refined type which only contains the integer 42:
> (ann 42 (Refine [n : Integer] (<= n 42)))
Dependent function types allow to specify dependencies between arguments or between the argument and the function range using a syntax similar to those of refinement types. Cyclic dependencies are not allowed. For example, this is how you could define a function to access the elements of a vector ruling out out-of-bounds conditions:
(: safe-ref1 (All (A) (-> ([v : (Vectorof A)]
[n : (v) (Refine [i : Natural]
(< i (vector-length v)))])
A)))
The same effect could be obtained by using a precondition in the function signature:
(: safe-ref2 (All (A) (-> ([v : (Vectorof A)]
[n : Natural])
#:pre (v n) (< n (vector-length v))
A)))
In conversation with InfoQ, Sam Tobin-Hochstadt, creator and maintainer of Typed Racket, explained that
Having dependent types in Typed Racket makes it possible to check properties of programs that you can’t express in almost any other language. We’re just starting to explore the kinds of improvements we can make to programs by using this new information, but we hope to make both faster and more reliable software using refinement and dependent types in Typed Racket.
Both refinement types and dependent functions were available in previous Racket versions as experimental features and are now available by default, although it is suggested that you regularly update to a snapshot build to get the latest fixes. If you want to know more about dependent types usage in Racket 6.11, do not miss this introduction by Andrew Kent, who did the primary work behind them under the guidance of Tobin-Hochstadt.
Dependent types are a feature of type systems that enables the creation of more expressive types, which can be used to catch more bugs at compile time. Other languages supporting dependent types include Idris, Coq, and F*, while Haskell has them in the works.
