BT

Your opinion matters! Please fill in the InfoQ Survey!

Refinement Types and Dependent Functions Stable in Racket 6.11

| by Sergio De Simone Follow 5 Followers on Nov 13, 2017. Estimated reading time: 2 minutes |

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.

Rate this Article

Adoption Stage
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and don't miss out on content that matters to you

BT