On this page:
define
define-values
define-type
define-type-alias
require
trace
module
module+
include
define-syntax-rule
define-syntax
splice

1 Definitions

The body of a plai-typed module is a sequence of definitions and expressions, and the module implicitly exports all top-level definitions. When a plai-typed module is imported into a module that does not use plai-typed, the imports have contracts (matching reflecting the exported bindings’ types).

syntax

(define id expr)

(define id : type expr)
(define (id id/type ...) expr)
(define (id id/type ...) : type expr)
 
id/type = id
  | [id : type]
Defines id.

The expr in each of the first two forms is evaluated to get the value of id. In the first form, the type of id is inferred at the type of expr, while the second form declares a specific type for id.

The third and fourth forms define id as a function, where each id/type is a function argument (with an optional declare type) and expr is the body of the function, which is evaluated when the function is called. In the fourth form, a type before the body expr declares the function’s result type (which must match the type of expr).

Note that the first and second forms of define also define functions in the case that expr produces a function, such as when expr is a lambda form. The third and fourth forms are simplify shorthands for defining a function.

Evaluating a reference to id before its definition is evaluated triggers an “undefined identifier” error.

Examples:
> (define a 1)
> a

- number

1

> (define b : number (+ 1 2))
> b

- number

3

> (define (c x)
    (+ x b))
> (c 3)

- number

6

> (define (d [y : number]) : number
    (c y))
> (d 4)

- number

7

syntax

(define-values (id/type ...) expr)

 
id/type = id
  | [id : type]
Defines each id/type (with an optional type declaration) to be the values within the tuple produced by expr, which must have as many values as declared id/types.

Examples:
> (define t (values 1 'one "One"))
> (define-values (a b c) t)
> a

- number

1

> (define-values ([x : number] [b : symbol] [c : string]) t)
> c

- string

"One"

syntax

(define-type tyid/abs
  [variant-id (field-id : type)]
  ...)
 
tyid/abs = id
  | (id 'arg-id ...)
Defines a type (when tyid/abs is id) or type constructor (when tyid/abs has the form (id 'id ...)).

A constructor variant-id is defined for each variant. Each constructor takes an argument for each field of its variant, where the type of each field is declared by the type after each field-id. The result type of each constructor is id.

Instances of a type declared with define-type are normally used through type-case.

In addition to the type and constructors, a define-type expression also defines:

Examples:
> (define-type Shape
    [circle (radius : number)]
    [rectangle (width : number)
               (height : number)])
> (define c (circle 10))
> c

- Shape

(circle 10)

> (circle? c)

- boolean

#t

> (circle-radius c)

- number

10

> (define r (rectangle 2 3))
> (+ (rectangle-width r) (rectangle-height r))

- number

5

syntax

(define-type-alias tyid/abs type)

 
tyid/abs = id
  | (id 'arg-id ...)
Defines a type alias id. When tyid/abs is id, then using id is the same as using type. When tyid/abs is (id 'arg-id ...), then using (id arg-type ...) is the same as using type with each 'arg-id replaced by the corresponding arg-type.

Examples:
> (define-type-alias size number)

- number

> (define (square-area [side : size])
    (* side side))
> (square-area 10)

- number

100

syntax

(require spec ...)

 
spec = module-path
  | (typed-in module-path [id : type] ...)
  | (opaque-type-in module-path [type-id predicate-id] ...)
  | (rename-in spec [orig-id new-id] ...)
Imports from each module-path.

When a module-path is not wrapped with typed-in or opaque-type-in, then module-path must refer to a module that is implemented with plai-typed.

When module-path is wrapped with typed-in, then only the specified ids are imported from module-path, and the type system assumes (without static or additional dynamic checks) the given type for each id.

When module-path is wrapped with opaque-type-in, then the corresponding type-ids are bound as opaque datatypes, where predicate-id from module-path is a run-time predicate (used for contracts as needed for cooperation with untyped code) for instances of the datatype.

Examples:
> (require (typed-in racket/base [gensym : (-> symbol)]))
> (gensym)

- symbol

'g10396

syntax

(trace id ...)

Traces subsequent calls—showing arguments and results—for functions bound to the ids. This form can be used only in a module top level, and only for tracing functions defined within the module.

syntax

(module id module-path form ...)

Declares a submodule named id, which can be required in the enclosing module using 'id or (submod "." id):

(module sub plai-typed
  (define n 8))
(require 'sub)
(+ n 1)

syntax

(module+ id form ...)

Declares/extends a submodule named id, which is particularly useful for defining a test submodule to hold tests that precede relevant definitions (since the submodule implicitly imports the bindings of its enclosing module, and DrRacket or raco test runs the test submodule):

(module+ test
  (test 11 (add-one 10)))
 
(define (add-one n)
  (+ 1 n))

syntax

(include path-spec)

Copy the content of path-spec in place of the include form, which can only be used in a top-level position.

syntax

(define-syntax-rule (id pattern ...) template)

syntax

(define-syntax id macro-expr)

(define-syntax (id arg-id) macro-body ...)
 
macro = (syntax-rules ....)
  | (lambda ....)
Defines a macro. In a macro-expr or macro-body, the bindings of racket/base are available.

A macro of the form

(define-syntax-rule (id pattern ...) template)

is equivalent to

(define-syntax id
  (syntax-rules ()
   [(id pattern ...) template]))

syntax

(splice form ...)

Equivalent to the forms sequence in a module or top-level context, which is useful for producing multiple definitions from a macro.