► |  | The Typed Scheme Reference

1 | Type Reference
2 | Special Form Reference

1`` Type Reference
Number
Integer
Boolean
String
Keyword
Symbol
Void
Port
Path
Char
Any
Listof
Boxof
Vectorof
Option
Parameter
Pair
->
U
case-lambda
All
List
values
Rec
2`` Special Form Reference
2.1`` Binding Forms
define:
let:
letrec:
let*:
lambda:
plambda:
case-lambda:
pcase-lambda:
2.2`` Structure Definitions
define-struct:
2.3`` Type Aliases
define-type-alias
2.4`` Type Annotation and Instantiation
:
ann
inst
2.5`` Require
require/ typed
require/ opaque-type
require-typed-struct

Version: 4.1.4
top← prev up next →

## The Typed Scheme Reference

Sam Tobin-Hochstadt

#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

A character

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)

top← prev up next →