14 Experimental Features
These features are currently experimental and subject to change.
syntax
(declare-refinement id)
syntax
(Refinement id)
syntax
(define-typed-struct/exec forms ...)
syntax
(define-new-subtype name (constructor t))
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.
> (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
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
> (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)
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.