The Typed Scheme Reference
| #lang typed-scheme |
1 Type Reference
Base Types
These types represent primitive Scheme data.
| Number |
A number
| Integer |
An integer
| Boolean |
Either #t or #f
| String |
A string
| Keyword |
A literal keyword
| Symbol |
A symbol
| Void |
#<void>
| Port |
A port
| Path |
A path
| Char |
| Any |
Any value
The following base types are parameteric in their type arguments.
| (Listof t) |
Homogenous lists of t
| (Boxof t) |
A box of t
| (Vectorof t) |
Homogenous vectors of t
| (Option t) |
Either t of #f
| (Parameter t) |
| (Parameter s t) |
A parameter of t. If two type arguments are supplied, the first is the type the parameter accepts, and the second is the type returned.
| (Pair s t) |
is the pair containing s as the car and t as the cdr
Type Constructors
| (dom -> rng) |
| (dom rest * -> rng) |
| (dom rest bound -> rng) |
| (dom -> rng : pred) |
is the type of functions from the (possibly-empty) sequence dom to the rng type. The second form specifies a uniform rest argument of type rest, and the third form specifies a non-uniform rest argument of type rest with bound bound. In the third form, the second occurrence of is literal, and bound must be an identifier denoting a type variable. In the fourth form, there must be only one dom and pred is the type checked by the predicate.
| (U t ) |
is the union of the types t
| (case-lambda fun-ty ) |
is a function that behaves like all of the fun-tys. The fun-tys must all be function types constructed with ->.
| (t t1 t2 ) |
is the instantiation of the parametric type t at types t1 t2
| (All (v ) t) |
is a parameterization of type t, with type variables v
| (List t ) |
is the type of the list with one element, in order, for each type provided to the List type constructor.
| (values t ) |
is the type of a sequence of multiple values, with types t . This can only appear as the return type of a function.
| v |
where v is a number, boolean or string, is the singleton type containing only that value
| 'sym |
where sym is a symbol, is the singleton type containing only that symbol
| i |
where i is an identifier can be a reference to a type name or a type variable
| (Rec n t) |
is a recursive type where n is bound to the recursive type in the body t
Other types cannot be written by the programmer, but are used internally and may appear in error messages.
| (struct:n (t )) |
is the type of structures named n with field types t. There may be multiple such types with the same printed representation.
| <n> |
is the printed representation of a reference to the type variable n
2 Special Form Reference
Typed Scheme provides a variety of special forms above and beyond those in PLT Scheme. They are used for annotating variables with types, creating new types, and annotating expressions.
2.1 Binding Forms
loop, f, a, and v are names, t is a type. e is an expression and body is a block.
| (define: v : t e) |
| (define: (f [v : t] ) : t . body) |
| (define: (a ) (f [v : t] ) : t . body) |
These forms define variables, with annotated types. The first form defines v with type t and value e. The second and third forms defines a function f with appropriate types. In most cases, use of : is preferred to use of define:.
| (let: ([v : t e] ) . body) |
| (let: loop : t0 ([v : t e] ) . body) |
where t0 is the type of the result of loop (and thus the result of the entire expression).
| (letrec: ([v : t e] ) . body) |
| (let*: ([v : t e] ) . body) |
| (lambda: ([v : t] ) . body) |
| (lambda: ([v : t] v : t) . body) |
| (plambda: (a ) ([v : t] ) . body) |
| (plambda: (a ) ([v : t] v : t) . body) |
| (case-lambda: [formals body] ) |
where formals is like the second element of a lambda:
| (pcase-lambda: (a ) [formals body] ) |
where formals is like the second element of a lambda:.
2.2 Structure Definitions
| (define-struct: name ([f : t] )) |
| (define-struct: (name parent) ([f : t] )) |
| (define-struct: (v ) name ([f : t] )) |
| (define-struct: (v ) (name parent) ([f : t] )) |
Defines a structure with the name name, where the fields f have types t. The second and fourth forms define name to be a substructure of parent. The last two forms define structures that are polymorphic in the type variables v.
2.3 Type Aliases
| (define-type-alias name t) |
| (define-type-alias (name v ) t) |
The first form defines name as type, with the same meaning as t. The second form is equivalent to (define-type-alias name (All (v ) t)). Type aliases may refer to other type aliases or types defined in the same module, but cycles among type aliases are prohibited.
2.4 Type Annotation and Instantiation
| (: v t) |
This declares that v has type t. The definition of v must appear after this declaration. This can be used anywhere a definition form may be used.
#{v : t} This declares that the variable v has type t. This is legal only for binding occurences of v.
| (ann e t) |
Ensure that e has type t, or some subtype. The entire expression has type t. This is legal only in expression contexts.
#{e :: t} This is identical to (ann e t).
| (inst e t ) |
Instantiate the type of e with types t . e must have a polymorphic type with the appropriate number of type variables. This is legal only in expression contexts.
#{e @ t ...} This is identical to (inst e t ...).
2.5 Require
Here, m is a module spec, pred is an identifier naming a predicate, and r is an optionally-renamed identifier.
| (require/typed r t m) |
| (require/typed m [r t] ) |
The first form requires r from module m, giving it type t. The second form generalizes this to multiple identifiers.
| (require/opaque-type t pred m) |
This defines a new type t. pred, imported from module m, is a predicate for this type. The type is defined as precisely those values to which pred produces #t. pred must have type (Any -> Boolean).
| (require-typed-struct name ([f : t] ) m) |