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.
loop, f, a, and v are names, t is a type.
e and body are expressions.
(define: (f [v : t] ...) : t body)
(define: v : t e)
(pdefine: (a ...) (f [v : t] ...) : t body)
(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 third element of a plambda:
name, parent, f, and v are names,
t is a type. parent must name a structure type.
(define-typed-struct name ([f : t] ...))
(define-typed-struct (name parent) ([f : t] ...))
(define-typed-struct (v ...) name ([f : t] ...))
(define-typed-struct (v ...) (name parent) ([f : t] ...))
name and v are names, t is a type.
(define-type-alias name t)
(define-type-alias (name v ...) t)
v is a variable name, e is an expression, t is a type.
These annotations require the use of the following declaration before the beginning of the module:
#reader (planet "typed-reader.ss" ("plt" "typed-scheme.plt"))
This will not affect the reading or parsing of any other syntax.
#{v : t} This is legal only for binding occurences of v
#{e :: t} This is legal only in expression contexts
v is a variable name, t is a type, and m is
a require-spec.
(require/typed v t m)