Typed Racket is a version of Racket with a static type checker. A module starts with #lang typed/racket instead of #lang racket, the programmer adds type annotations, and the checker verifies at compile time that the program is consistent with them. Types are checked before the program runs and then removed; where typed code meets untyped code, the checker adds contracts. The language is designed so that ordinary Racket programs need little change.
The typed languages
#lang | Is |
|---|---|
typed/racket | the typed version of racket |
typed/racket/base | the typed version of racket/base, with the smaller set of names |
typed/racket/shallow | "Shallow" types: the same checking, but typed-untyped boundaries use cheap shape checks (that a value has the right outermost constructor) instead of full contracts. Sound, with lower cost, but checked only locally |
typed/racket/optional | "Optional" types: checked at compile time and then ignored, with no run-time checks and no type-driven optimisation; the run-time behaviour is that of untyped Racket |
typed/racket/no-check | the typed syntax, with the checker turned off |
the plain typed/racket is "Deep" | Deep types check every value that crosses between typed and untyped code with a contract, which makes them fully reliable and lets the optimiser trust them |
There are also typed counterparts of many libraries, such as typed/racket/class, typed/racket/gui, typed/rackunit, typed/json and typed/net/url, and the form require/typed brings an untyped library in with types you state.
Annotations
| Form | Meaning |
|---|---|
(: id type) | declares the type of a definition, before or after it, at the module level or in an internal definition context. (: f (-> Integer Integer)) |
(define x : Type expr), (define (f [a : A] [b : B 1]) : R body) | annotations within the definition: a type after the name, after each argument, and after the argument list for the result. An optional argument's default follows its type; a rest argument is [xs : T *] and its type in the function type is T * |
(let ([x : T e]) …), let*, letrec, (let loop : R ([i : Integer 0]) …), (lambda ([x : T] …) : R body), (case-lambda …), (for ([x : T xs]) …) | the binding forms take the same annotations. A named let may state its result type |
#{x : T} | a reader extension that annotates a single variable where the form has no annotated version, such as inside match |
(ann e T) | states the expected type of an expression, and checks it |
(cast e T) | checks at run time that the value has the type, and changes the static type; fails with a contract error otherwise |
(assert e [pred]) | an error unless the value is not #f (or satisfies the predicate), narrowing the type |
(inst f T …) | instantiates a polymorphic function at the given types |
(define-type Name T), (define-type (Name A …) T) | names a type, with parameters for a polymorphic one: (define-type (Maybe A) (U Nothing (Just A))) |
(define-predicate name? T), (make-predicate T) | a predicate that tests for a type, if the type can be tested at run time |
(struct name ([field : T] …) option …) | structure with typed fields; #:mutable, #:transparent, #:prefab and a parent structure are accepted |
Older versions gave the typed forms names with a colon (define:, lambda:, let:, struct:, for:); they remain as legacy forms.
Types
| Type | Values |
|---|---|
True, False, Boolean, String, Char, Symbol, Keyword, Bytes, Void, Null, Any, Nothing | the basic ones. A symbol, number or string literal is also a type: 'foo, 23, "x" are the types that contain only that value |
Number, Real, Integer, Natural, Exact-Rational, Float (Flonum), Single-Flonum, Positive-Integer, Nonnegative-Integer, Positive-Real, Byte, Index, Fixnum, Zero, One and the other numeric-tower types | a hierarchy of number types, from Number down to those for exactness, sign and size; Integer is the exact integers only, and a number literal such as 23 is also a type of its own |
(-> A B … R), (->* (A …) (O …) R), (-> A … rest * R), (case-> …), (Values A B) | function types: required arguments then the result; optional and keyword arguments with ->* ((->* (#:x Number) (#:y Number) (values Number Number))); a repeated rest argument with *; several arities with case->; multiple results with Values |
(U A B …) | a union: a value of any of the types. Nested unions are flattened; String is a subtype of (U String Number) |
(Listof T), (Pairof A B), (List A B …), (Vectorof T), (Boxof T), (HashTable K V), (Setof T), (Sequenceof T), (Parameterof T), (Promiseof T), (Evtof T), (Channelof T) … | the types of the data structures: (List A B) is a list of exactly two elements; (Listof T) any number |
(Rec X T), a recursive define-type | a recursive type. (define-type Tree (U Number (Listof Tree))) |
(All (A …) T) (also ∀), (All (A ...) T) | a polymorphic type; the second form takes a variable number of type arguments |
(Refine [x : T] prop), (Struct name), Opaque types | refined types; the type of a structure; types of untyped values that can be only passed around and tested with their predicate |
(Syntax T), Identifier, Path, Regexp, Port, Input-Port, Output-Port, Thread, Procedure | types of the other Racket values |
(Class …), Object, Unit | types of classes, objects and units, with their own forms in the typed class and unit libraries |
#lang typed/racket
(struct pt ([x : Real] [y : Real]))
(: distance (-> pt pt Real))
(define (distance p1 p2)
(sqrt (+ (sqr (- (pt-x p2) (pt-x p1)))
(sqr (- (pt-y p2) (pt-y p1))))))
(define-type Tree (U Number (Listof Tree)))
(: sum-tree (-> Tree Number))
(define (sum-tree t)
(cond [(number? t) t] ; occurrence typing: t is a Number here
[else (apply + (map sum-tree t))])) ; ... and a (Listof Tree) here
(: first-or (All (A) (-> (Listof A) A A)))
(define (first-or xs default) (if (null? xs) default (car xs)))Occurrence typing
Typed Racket changes what it knows about a variable depending on the tests the program makes. After (if (number? x) A B), x has type Number in A and the type without Number in B. This works with cond, and, or, when, unless, case and match (with caveats), and with any predicate that has a type of the form (-> Any Boolean : T), which says "if true, the argument is a T". Struct predicates, null?, pair?, string? and the like all have such types; a user predicate can be made with define-predicate. A variable that is assigned with set! is not narrowed.
Typed and untyped code together
(require/typed module-path [name type] …)imports untyped names and gives them types you state. The checker wraps each in a contract (Deep types), a shape check (Shallow types), or nothing (Optional types).[#:struct name ([field : T] …)]imports a structure, and(require/opaque-type Name pred? "module")imports a type known only by its predicate.- Untyped code that requires a typed module gets the exports wrapped in contracts that match their types.
#:opaqueand#:structoptions andrequire/typed/providehandle common cases. - Deep boundaries on large vectors, hash tables and first-class functions can cost time; measure before moving a loop across the boundary.
The optimiser, REPL and limits
With Deep types, the checker's results let the compiler replace generic arithmetic with fixnum and flonum operations and avoid some run-time checks; types that name flonums (Float) and exact integers help most. In the typed REPL a result prints with its type, :print-type shows an expression's type and :type shows the type of a name. Some Racket features do not fit the checker: macros that expand to untypeable code, programs that depend on eval, and constructs whose type depends on values. The type Integer means the values for which exact-integer? is true, not those for which integer? is true, which also takes 1.0; a program ported from untyped Racket may need exact-round and exact-floor in place of round and floor.
How the viewer reads a typed module
A file that starts #lang typed/racket (or any typed/… language) is shown as a Typed Racket module. After : the scanner reads a type: names are coloured as types, the type constructors ->, U, All, Listof and the rest are types, and the : itself is a keyword. This applies to (: name type), to [x : T] in argument lists, binding lists and struct fields, to the result type after an argument list, and to ann, cast, inst, define-type and require/typed. In an untyped module a colon is an ordinary name.
Not described
Known, not yet covered
- Reference: only the Typed Racket Guide chapters on beginning, types, annotations, occurrence typing, typed-untyped interaction, optimisation and caveats were read, and the Reference (
ts-referenceand its pages on special forms, types, utilities, typed classes, units, regions, unsafe operations and the legacy forms) was not. The full list of types and of type-level operations (Refine,Distinction,Intersection,Exact-Positive-Integerand relatives,Flvectorand the like) is therefore a sample; the precise numeric hierarchy is not given. - Reference: occurrence typing's propositions (
: T @ path,-> … : T #:+ … #:-annotations), polymorphism with ellipsis, row polymorphism for classes, and thetyped/racket/unitandtyped/racket/classforms are not described. - Viewer:
#{x : T}reads as a vector-like prefix and not as an annotation; type forms such asRefineandAllvariable lists are coloured as types without further structure; a user-defined type is coloured as a type only where the scanner expects one.
See also
- Contracts – what a Deep boundary uses
- The #lang family – the other languages of the family
- Structs – the untyped
struct