On this page:
declare-refinement
Refinement
define-typed-struct/  exec
define-new-subtype
14.1 Refinements and Linear Integer Reasoning
Refine
!
6.9

14 Experimental Features

These features are currently experimental and subject to change.

syntax

(declare-refinement id)

Declares id to be usable in refinement types.

syntax

(Refinement id)

Includes values that have been tested with the predicate id, which must have been specified with declare-refinement.

syntax

(define-typed-struct/exec forms ...)

Defines an executable structure.

syntax

(define-new-subtype name (constructor t))

Defines a new type name that is a subtype of t. The constructor is defined as a function that takes a value of type t and produces a value of the new type name. A define-new-subtype definition is only allowed at the top level of a file or module.

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.

Examples:
> (module m typed/racket
    (provide Radians radians f)
    (define-new-subtype Radians (radians Real))
    (: f : [Radians -> Real])
    (define (f a)
      (sin a)))
> (require 'm)
> (radians 0)

- : Real [more precisely: Radians]

0

> (f (radians 0))

- : Real

0

14.1 Refinements and Linear Integer Reasoning

Refinement types have been added to Typed Racket’s core, but Typed Racket does not yet have function types which allow dependencies between argument types, limiting how useful refinements are for now. Allowing argument dependencies is on our ‘to do’ list.

syntax

(Refine [id : type] proposition)

 
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
  | linear-term
  | (+ linear-term linear-term ...)
     
linear-term = symbolic-path
  | (* exact-integer symbolic-path)
     
symbolic-path = id
  | (path-elem symbolic-path)
     
path-elem = car
  | cdr
  | vector-length
(Refine [v : t] p) is a refinement of type t with logical proposition p, or in other words it describes any value v of type t for which the logical proposition p holds.

Example:
> (ann 42 (Refine [n : Integer] (= n 42)))

- : Integer [more precisely: (Refine (n : Integer) (= 42 n))]

42

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.

syntax

(! sym-obj type)

This is the dual of (: o t), holding when o is not 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).

Typed Racket’s linear integer reasoning is turned off by default. If you want to activate it, you must add the #:with-linear-integer-arithmetic keyword when specifying the language of your program:

#lang typed/racket #:with-linear-integer-arithmetic

With this language option on, code such as the following will type check:

(if (< 5 4)
    (+ "Luke," "I am your father")
    "that's impossible!")

i.e. with linear integer 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.