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'' (``samth'' ``typed-scheme.plt'' 1))
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)